Step * of Lemma cubical-eta

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠB}].  ((λapp((w)p; q)) w ∈ {X ⊢ _:ΠB})
BY
xxx((Auto THEN Symmetry) THEN Assert ⌜app((w)p; q)) ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst(ΠB)) a))⌝⋅)xxx }

1
.....assertion..... 
1. CubicalSet
2. {X ⊢ _}
3. {X.A ⊢ _}
4. {X ⊢ _:ΠB}
⊢ app((w)p; q)) ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst(ΠB)) a))

2
1. CubicalSet
2. {X ⊢ _}
3. {X.A ⊢ _}
4. {X ⊢ _:ΠB}
5. app((w)p; q)) ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst(ΠB)) a))
⊢ app((w)p; q)) ∈ {X ⊢ _:ΠB}


Latex:


Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:\mPi{}A  B\}].    ((\mlambda{}app((w)p;  q))  =  w)


By


Latex:
xxx((Auto  THEN  Symmetry)  THEN  Assert  \mkleeneopen{}w  =  (\mlambda{}app((w)p;  q))\mkleeneclose{}\mcdot{})xxx




Home Index