---

Step * 1 of Lemma cubical-equiv-by-cases_wf

.....subterm..... T:t
3:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
6. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
⊢ IdEquiv(G.𝕀, (q=1);(B)p) ∈ {G.𝕀, (q=1) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)}
BY
{ ((GenConcl ⌜q = i ∈ {G.𝕀 ⊢ _:𝕀}⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(A)p = AA ∈ {G.𝕀 ⊢ _}⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(B)p = BB ∈ {G.𝕀 ⊢ _}⌝⋅ THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
6. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
7. i : {G.𝕀 ⊢ _:𝕀}
8. q = i ∈ {G.𝕀 ⊢ _:𝕀}
9. AA : {G.𝕀 ⊢ _}
10. (A)p = AA ∈ {G.𝕀 ⊢ _}
11. BB : {G.𝕀 ⊢ _}
12. (B)p = BB ∈ {G.𝕀 ⊢ _}
⊢ IdEquiv(G.𝕀, (i=1);BB) ∈ {G.𝕀, (i=1) ⊢ _:Equiv((if (i=0) then AA else BB);BB)}

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (A)p
6.  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (B)p
\mvdash{}  IdEquiv(G.\mBbbI{},  (q=1);(B)p)  \mmember{}  \{G.\mBbbI{},  (q=1)  \mvdash{}  \_:Equiv((if  (q=0)  then  (A)p  else  (B)p);(B)p)\}


By

---

Latex:
((GenConcl  \mkleeneopen{}q  =  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(A)p  =  AA\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(B)p  =  BB\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index