---

Step * 1 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)p
BY
{ (InferEqualTypeUp THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
2:n
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
⊢ ((phi)p)x = ((phi)p)f ∈ {X ⊢ _:𝔽}

---

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.\mBbbI{},  (phi)p


By

---

Latex:
(InferEqualTypeUp  THEN  RepeatFor  2  (EqCDA))

---

Home Index