---

Step * 1 of Lemma subset-iota-is-id


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ v = (v)iota ∈ {H, phi ⊢ _}
BY
{ BLemma `cubical-type-equal` }

1
.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ H, phi j⊢

2
.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ H, phi ⊢ v

3
.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ (v)iota ∈ A:I:fset(ℕ) ⟶ H, phi(I) ⟶ Type × (I:fset(ℕ)
                                               ⟶ J:fset(ℕ)
                                               ⟶ f:J ⟶ I
                                               ⟶ a:H, phi(I)
                                               ⟶ (A I a)
                                               ⟶ (A J f(a)))

4
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ v
= (v)iota
∈ (A:I:fset(ℕ) ⟶ H, phi(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:H, phi(I) ⟶ (A I a) ⟶ (A J f(a))))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  v  :  \{H,  phi  \mvdash{}  \_\}
\mvdash{}  v  =  (v)iota


By

---

Latex:
BLemma  `cubical-type-equal`

---

Home Index