Step * 2 1 of Lemma equiv-path2-0


1. CubicalSet{j}
2. {G ⊢ _}
3. {G ⊢ _}
4. {G ⊢ _:Equiv(A;B)}
5. cA +⊢ Compositon(A)
6. cB +⊢ Compositon(B)
7. G.𝕀((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
8. case-type-comp(G.𝕀(q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p)
   ∈ G.𝕀((q=0) ∨ (q=1)) +⊢ Compositon((if (q=0) then (A)p else (B)p))
⊢ G ⊢ (1(𝔽 ((0(𝕀)=0) ∨ (0(𝕀)=1)))
BY
((InstLemma `face-zero-interval-0` [⌜G⌝]⋅ THENA Auto) THEN RWO "-1" THEN Auto) }


Latex:


Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  cA  :  G  +\mvdash{}  Compositon(A)
6.  cB  :  G  +\mvdash{}  Compositon(B)
7.  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)
8.  case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p)
      \mmember{}  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  +\mvdash{}  Compositon((if  (q=0)  then  (A)p  else  (B)p))
\mvdash{}  G  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  ((0(\mBbbI{})=0)  \mvee{}  (0(\mBbbI{})=1)))


By


Latex:
((InstLemma  `face-zero-interval-0`  [\mkleeneopen{}G\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto)




Home Index