`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[J,K,g,v,u:Top].  (g((v;u)) ~ (g(v);(u v g)))`

Proof

Definitions occuring in Statement :  cc-adjoin-cube: `(v;u)` cube-context-adjoin: `X.A` cubical-type-ap-morph: `(u a f)` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` cubical-set: `CubicalSet` uall: `∀[x:A]. B[x]` top: `Top` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` cubical-type: `{X ⊢ _}` cubical-type-ap-morph: `(u a f)` cc-adjoin-cube: `(v;u)` cube-context-adjoin: `X.A` pi2: `snd(t)` cube-set-restriction: `f(s)` pi1: `fst(t)`
Lemmas referenced :  top_wf cubical-type_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule hypothesis sqequalAxiom lemma_by_obid isect_memberEquality isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[J,K,g,v,u:Top].    (g((v;u))  \msim{}  (g(v);(u  v  g)))

Date html generated: 2016_06_16-PM-05_40_56
Last ObjectModification: 2015_12_28-PM-04_35_06

Theory : cubical!sets

Home Index