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