---

Step * of Lemma cube-set-map-subtype

∀[A,B:CubicalSet].  (A ⟶ B ⊆r (I:(Cname List) ⟶ A(I) ⟶ B(I)))
BY
{ xxx(Intros THEN (D 0 THENA Auto) THEN D -1 THEN Thin (-1))xxx }

1
1. A : CubicalSet
2. B : CubicalSet
3. x : A@0:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (A A@0) (B A@0))
⊢ x ∈ I:(Cname List) ⟶ A(I) ⟶ B(I)

---

Latex:

---

Latex:
\mforall{}[A,B:CubicalSet].    (A  {}\mrightarrow{}  B  \msubseteq{}r  (I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)))


By

---

Latex:
xxx(Intros  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Thin  (-1))xxx

---

Home Index