---

Step * of Lemma subtype-context-subset-0

No Annotations
∀[X,Y:j⊢].  ({X ⊢ _} ⊆r {Y, 0(𝔽) ⊢ _})
BY
{ ((UnivCD THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (DVar `x')
   THEN Thin (-1)
   THEN RepUR ``cubical-type context-subset cubical-term-at face-0`` 0) }

1
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. A : I:fset(ℕ) ⟶ X(I) ⟶ Type
4. x1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a))
⊢ <A, x1> ∈ {AF:A:I:fset(ℕ) ⟶ {rho:Y(I)| 0 = 1 ∈ Point(face_lattice(I))}  ⟶ Type
             × (I:fset(ℕ)
               ⟶ J:fset(ℕ)
               ⟶ f:J ⟶ I
               ⟶ a:{rho:Y(I)| 0 = 1 ∈ Point(face_lattice(I))} 
               ⟶ (A I a)
               ⟶ (A J f(a)))| 
             let A,F = AF 
             in (∀I:fset(ℕ). ∀a:{rho:Y(I)| 0 = 1 ∈ Point(face_lattice(I))} . ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
                ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:{rho:Y(I)| 0 = 1 ∈ Point(face_lattice(I))} . ∀u:A I a.
                     ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].    (\{X  \mvdash{}  \_\}  \msubseteq{}r  \{Y,  0(\mBbbF{})  \mvdash{}  \_\})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `x')
  THEN  Thin  (-1)
  THEN  RepUR  ``cubical-type  context-subset  cubical-term-at  face-0``  0)

---

Home Index