---

Step * 1 of Lemma context-subset-map-equal


1. H : CubicalSet{j}
2. H.𝕀 j⊢
3. phi : {H ⊢ _:𝔽}
4. X : CubicalSet{j}
5. f : X j⟶ H.𝕀
6. g : X j⟶ H.𝕀
7. f = g ∈ X j⟶ H.𝕀
8. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
9. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
10. x : X j⟶ H.𝕀
11. (x = f ∈ X j⟶ H.𝕀) ∧ (x = g ∈ X j⟶ H.𝕀)
12. x ∈ X, ((phi)p)x j⟶ H.𝕀, (phi)p
⊢ x ∈ X, ((phi)p)f j⟶ H, phi.𝕀
BY
{ SubsumeC ⌜X, ((phi)p)f j⟶ H.𝕀, (phi)p⌝⋅ }

1
1. H : CubicalSet{j}
2. H.𝕀 j⊢
3. phi : {H ⊢ _:𝔽}
4. X : CubicalSet{j}
5. f : X j⟶ H.𝕀
6. g : X j⟶ H.𝕀
7. f = g ∈ X j⟶ H.𝕀
8. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
9. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
10. x : X j⟶ H.𝕀
11. (x = f ∈ X j⟶ H.𝕀) ∧ (x = g ∈ X j⟶ H.𝕀)
12. x ∈ X, ((phi)p)x j⟶ H.𝕀, (phi)p
⊢ x ∈ X, ((phi)p)f j⟶ H.𝕀, (phi)p

2
1. H : CubicalSet{j}
2. H.𝕀 j⊢
3. phi : {H ⊢ _:𝔽}
4. X : CubicalSet{j}
5. f : X j⟶ H.𝕀
6. g : X j⟶ H.𝕀
7. f = g ∈ X j⟶ H.𝕀
8. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
9. f = g ∈ {z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} 
10. x : X j⟶ H.𝕀
11. (x = f ∈ X j⟶ H.𝕀) ∧ (x = g ∈ X j⟶ H.𝕀)
12. x ∈ X, ((phi)p)x j⟶ H.𝕀, (phi)p
13. x = x ∈ X, ((phi)p)f j⟶ H.𝕀, (phi)p
⊢ X, ((phi)p)f j⟶ H.𝕀, (phi)p ⊆r X, ((phi)p)f j⟶ H, phi.𝕀

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  H.\mBbbI{}  j\mvdash{}
3.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
4.  X  :  CubicalSet\{j\}
5.  f  :  X  j{}\mrightarrow{}  H.\mBbbI{}
6.  g  :  X  j{}\mrightarrow{}  H.\mBbbI{}
7.  f  =  g
8.  f  =  g
9.  f  =  g
10.  x  :  X  j{}\mrightarrow{}  H.\mBbbI{}
11.  (x  =  f)  \mwedge{}  (x  =  g)
12.  x  \mmember{}  X,  ((phi)p)x  j{}\mrightarrow{}  H.\mBbbI{},  (phi)p
\mvdash{}  x  \mmember{}  X,  ((phi)p)f  j{}\mrightarrow{}  H,  phi.\mBbbI{}


By

---

Latex:
SubsumeC  \mkleeneopen{}X,  ((phi)p)f  j{}\mrightarrow{}  H.\mBbbI{},  (phi)p\mkleeneclose{}\mcdot{}

---

Home Index