Nuprl Lemma : csm-ap-comp-type-sq

[Gamma:CubicalSet]. ∀[Delta,Z,s1,s2:Top].  ∀A:{Gamma ⊢ _}. ((A)s2 s1 ((A)s2)s1)


Proof




Definitions occuring in Statement :  csm-ap-type: (AF)s cubical-type: {X ⊢ _} csm-comp: F cubical-set: CubicalSet uall: [x:A]. B[x] top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] cubical-type: {X ⊢ _} csm-ap-type: (AF)s csm-comp: F csm-ap: (s)x type-cat: TypeCat trans-comp: trans-comp(C;D;F;G;H;t1;t2) cat-comp: cat-comp(C) pi2: snd(t) compose: g member: t ∈ T
Lemmas referenced :  cubical-set_wf top_wf cubical-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution setElimination thin rename cut productElimination sqequalRule hypothesis lemma_by_obid isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}[Gamma:CubicalSet].  \mforall{}[Delta,Z,s1,s2:Top].    \mforall{}A:\{Gamma  \mvdash{}  \_\}.  ((A)s2  o  s1  \msim{}  ((A)s2)s1)



Date html generated: 2016_06_16-PM-05_39_47
Last ObjectModification: 2016_03_28-PM-09_46_48

Theory : cubical!sets


Home Index