---

Step * of Lemma csm-subtype-cubical-subset

No Annotations
∀[Gamma:j⊢]. ∀[I:fset(ℕ)]. ∀[psi:𝔽(I)].  (formal-cube(I) j⟶ Gamma ⊆r I,psi j⟶ Gamma)
BY
{ ... }

1
1. Gamma : CubicalSet{j}
2. I : fset(ℕ)
3. psi : 𝔽(I)
4. x : A:fset(ℕ) ⟶ A ⟶ I ⟶ Gamma(A)
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.
     ((λx@0.((snd(Gamma)) A B g (x A x@0))) = (λx@0.(x B x@0 ⋅ g)) ∈ (A ⟶ I ⟶ ((fst(Gamma)) B)))
6. A : fset(ℕ)
7. B : fset(ℕ)
8. g : B ⟶ A
⊢ (λx@0.((snd(Gamma)) A B g (x A x@0))) = (λx@0.(x B x@0 ⋅ g)) ∈ ({f:A ⟶ I| (psi f) = 1}  ⟶ Gamma(B))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].    (formal-cube(I)  j{}\mrightarrow{}  Gamma  \msubseteq{}r  I,psi  j{}\mrightarrow{}  Gamma)


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  DVar  `x'
  THEN  (MemTypeCD  THENL  [Id;  Id;  Auto])
  THEN  All  (RepUR  ``cube-cat  type-cat  cubical-subset  rep-sub-sheaf  formal-cube``)
  THEN  All  (RepUR  ``cat-arrow  op-cat  cat-ob  functor-ob  functor-arrow  cat-comp  compose``)
  THEN  Try  (((Fold  `functor-ob`  0  THEN  Fold  `I\_cube`  0)
                        THEN  Fold  `functor-ob`  (-2)
                        THEN  Fold  `I\_cube`  (-2)
                        THEN  Auto)))

---

Home Index