Nuprl Lemma : psc-restriction-comp2
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀I,J1,J2,K:cat-ob(C). ∀f:cat-arrow(C) J1 I. ∀g:cat-arrow(C) K J1. ∀a:X(I).
  g(f(a)) = cat-comp(C) K J1 I g f(a) ∈ X(K) supposing J1 = J2 ∈ cat-ob(C)
Proof
Definitions occuring in Statement : 
psc-restriction: f(s)
, 
I_set: A(I)
, 
ps_context: __⊢
, 
uimplies: b supposing a
, 
all: ∀x:A. B[x]
, 
apply: f a
, 
equal: s = t ∈ T
, 
cat-comp: cat-comp(C)
, 
cat-arrow: cat-arrow(C)
, 
cat-ob: cat-ob(C)
, 
small-category: SmallCategory
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
uimplies: b supposing a
, 
member: t ∈ T
, 
squash: ↓T
, 
uall: ∀[x:A]. B[x]
, 
subtype_rel: A ⊆r B
, 
and: P ∧ Q
, 
true: True
, 
guard: {T}
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ Q
, 
implies: P 
⇒ Q
Lemmas referenced : 
equal_wf, 
I_set_wf, 
psc-restriction_wf, 
small-category-cumulativity-2, 
ps_context_cumulativity2, 
subtype_rel-equal, 
cat-arrow_wf, 
cat-comp_wf, 
iff_weakening_equal, 
psc-restriction-comp
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation_alt, 
isect_memberFormation_alt, 
cut, 
applyEquality, 
thin, 
instantiate, 
lambdaEquality_alt, 
sqequalHypSubstitution, 
imageElimination, 
introduction, 
extract_by_obid, 
isectElimination, 
because_Cache, 
hypothesis, 
hypothesisEquality, 
sqequalRule, 
independent_isectElimination, 
equalitySymmetry, 
dependent_set_memberEquality_alt, 
independent_pairFormation, 
equalityTransitivity, 
productIsType, 
equalityIstype, 
inhabitedIsType, 
applyLambdaEquality, 
setElimination, 
rename, 
productElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
independent_functionElimination, 
dependent_functionElimination, 
universeIsType
Latex:
\mforall{}C:SmallCategory.  \mforall{}X:ps\_context\{j:l\}(C).  \mforall{}I,J1,J2,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J1  I.
\mforall{}g:cat-arrow(C)  K  J1.  \mforall{}a:X(I).
    g(f(a))  =  cat-comp(C)  K  J1  I  g  f(a)  supposing  J1  =  J2
Date html generated:
2020_05_20-PM-01_24_33
Last ObjectModification:
2020_04_01-AM-11_00_38
Theory : presheaf!models!of!type!theory
Home
Index