---

Step * of Lemma context-adjoin-subset0

No Annotations
∀[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].  ∀T:{H ⊢ _}. sub_cubical_set{k:l}(H.T, (phi)p; H, phi.T)
BY
{ ((Intros THEN Unfold `sub_cubical_set` 0)
   THEN (Assert ∀A:fset(ℕ). ∀rho:alpha:H(A) × T(alpha).  ((phi)p(rho) ∈ Point(face_lattice(A))) BY
               (Auto
                THEN DVar `phi'
                THEN RepUR ``csm-ap-term cc-fst csm-ap cubical-term-at`` 0
                THEN InferEqualType
                THEN Auto))
   THEN MemTypeCD
   THEN RepUR ``csm-id cube_set_map nat-trans cat-ob op-cat cat-arrow functor-ob`` 0
   THEN RepUR ``functor-arrow cat-comp type-cat names-cat cube-context-adjoin`` 0
   THEN RepUR ``context-subset compose`` 0) }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. T : {H ⊢ _}
4. ∀A:fset(ℕ). ∀rho:alpha:H(A) × T(alpha).  ((phi)p(rho) ∈ Point(face_lattice(A)))
⊢ λA,x. x ∈ A:fset(ℕ)
  ⟶ {rho:alpha:H(A) × T(alpha)| (phi)p(rho) = 1 ∈ Point(face_lattice(A))} 
  ⟶ (alpha:{rho:H(A)| phi(rho) = 1 ∈ Point(face_lattice(A))}  × T(alpha))

2
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. T : {H ⊢ _}
4. ∀A:fset(ℕ). ∀rho:alpha:H(A) × T(alpha).  ((phi)p(rho) ∈ Point(face_lattice(A)))
⊢ ∀A,B:fset(ℕ). ∀g:B ⟶ A.
    ((λx.<g(fst(x)), (snd(x) fst(x) g)>)
    = (λx.<g(fst(x)), (snd(x) fst(x) g)>)
    ∈ ({rho:alpha:H(A) × T(alpha)| (phi)p(rho) = 1 ∈ Point(face_lattice(A))}  ⟶ (alpha:{rho:H(B)| 
                                                                                       phi(rho)
                                                                                       = 1
                                                                                       ∈ Point(face_lattice(B))}  × T(al\000Cpha))))

3
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. T : {H ⊢ _}
4. ∀A:fset(ℕ). ∀rho:alpha:H(A) × T(alpha).  ((phi)p(rho) ∈ Point(face_lattice(A)))
5. trans : A:cat-ob(op-cat(CubeCat)) ⟶ (cat-arrow(type-cat{k':l}) (H.T, (phi)p A) (H, phi.T A))
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.
           ((λx.<g(fst((trans A x))), (snd((trans A x)) fst((trans A x)) g)>)
           = (λx.(trans B <g(fst(x)), (snd(x) fst(x) g)>))
           ∈ ({rho:alpha:H(A) × T(alpha)| (phi)p(rho) = 1 ∈ Point(face_lattice(A))}  ⟶ (alpha:{rho:H(B)| 
                                                                                              phi(rho)
                                                                                              = 1
                                                                                              ∈ Point(face_lattice(B))} 
                                                                                      × T(alpha)))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    \mforall{}T:\{H  \mvdash{}  \_\}.  sub\_cubical\_set\{k:l\}(H.T,  (phi)p;  H,  phi.T)


By

---

Latex:
((Intros  THEN  Unfold  `sub\_cubical\_set`  0)
  THEN  (Assert  \mforall{}A:fset(\mBbbN{}).  \mforall{}rho:alpha:H(A)  \mtimes{}  T(alpha).    ((phi)p(rho)  \mmember{}  Point(face\_lattice(A)))  BY
                          (Auto
                            THEN  DVar  `phi'
                            THEN  RepUR  ``csm-ap-term  cc-fst  csm-ap  cubical-term-at``  0
                            THEN  InferEqualType
                            THEN  Auto))
  THEN  MemTypeCD
  THEN  RepUR  ``csm-id  cube\_set\_map  nat-trans  cat-ob  op-cat  cat-arrow  functor-ob``  0
  THEN  RepUR  ``functor-arrow  cat-comp  type-cat  names-cat  cube-context-adjoin``  0
  THEN  RepUR  ``context-subset  compose``  0)

---

Home Index