---

Step * of Lemma context-subset-map-equal

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}]. ∀[X:j⊢]. ∀[f,g:X j⟶ H.𝕀].  ((f = g ∈ X j⟶ H.𝕀) ⇒ (f = g ∈ X, ((phi)p)f j⟶ H, phi.𝕀))
BY
{ ((Intro THEN (Assert H.𝕀 j⊢ BY Auto) THEN Intros)
   THEN StrengthenEquation (-1)
   THEN SubsumeC ⌜{z:X j⟶ H.𝕀| (z = f ∈ X j⟶ H.𝕀) ∧ (z = g ∈ X j⟶ H.𝕀)} ⌝⋅
   THEN Try (Trivial)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (InstLemma `context-subset-map` [⌜H.𝕀⌝;⌜(phi)p⌝;⌜X⌝;⌜x⌝]⋅ THENA Auto)) }

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.𝕀

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[X:j\mvdash{}].  \mforall{}[f,g:X  j{}\mrightarrow{}  H.\mBbbI{}].    ((f  =  g)  {}\mRightarrow{}  (f  =  g))


By

---

Latex:
((Intro  THEN  (Assert  H.\mBbbI{}  j\mvdash{}  BY  Auto)  THEN  Intros)
  THEN  StrengthenEquation  (-1)
  THEN  SubsumeC  \mkleeneopen{}\{z:X  j{}\mrightarrow{}  H.\mBbbI{}|  (z  =  f)  \mwedge{}  (z  =  g)\}  \mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `context-subset-map`  [\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(phi)p\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index