---

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

.....subterm..... T:t
2: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
⊢ (f)p ∈ {G.𝕀, (q=0) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)[(q=1) |⟶ IdEquiv(G.𝕀, (q=1);(B)p)]}
BY
{ MemTypeCD }

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
⊢ (f)p ∈ {G.𝕀, (q=0) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)}

2
.....set predicate..... 
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) = (f)p ∈ {G.𝕀, (q=0), (q=1) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)}

3
.....wf..... 
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. a : {G.𝕀, (q=0) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)}
⊢ istype(IdEquiv(G.𝕀, (q=1);(B)p) = a ∈ {G.𝕀, (q=0), (q=1) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)})

---

Latex:

---

Latex:
.....subterm.....  T:t
2: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{}  (f)p  \mmember{}  \{G.\mBbbI{},  (q=0)  \mvdash{}  \_:Equiv((if  (q=0)  then  (A)p  else  (B)p);(B)p)[(q=1) 
                                                  |{}\mrightarrow{}  IdEquiv(G.\mBbbI{},  (q=1);(B)p)]\}


By

---

Latex:
MemTypeCD

---

Home Index