`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[L:I-face(X;I) List].  (adjacent-compatible(X;I;L) ∈ ℙ)`

Proof

Definitions occuring in Statement :  adjacent-compatible: `adjacent-compatible(X;I;L)` I-face: `I-face(X;I)` cubical-set: `CubicalSet` coordinate_name: `Cname` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` adjacent-compatible: `adjacent-compatible(X;I;L)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  pairwise_wf2 I-face_wf face-compatible_wf list_wf coordinate_name_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].  \mforall{}[L:I-face(X;I)  List].    (adjacent-compatible(X;I;L)  \mmember{}  \mBbbP{})

Date html generated: 2016_06_16-PM-05_50_11
Last ObjectModification: 2015_12_28-PM-04_30_18

Theory : cubical!sets

Home Index