---

Step * of Lemma context-subset-map

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[Z:j⊢]. ∀[s:Z j⟶ Gamma].  (s ∈ Z, (phi)s j⟶ Gamma, phi)
BY
{ (Intros
   THEN Unhide
   THEN (Assert s ∈ Z j⟶ Gamma BY
               Trivial)
   THEN (Assert (phi)s ∈ {Z ⊢ _:𝔽} BY
               Auto)
   THEN RepUR ``cube_set_map psc_map`` 0
   THEN OnVar `s' (RepUR ``cube_set_map psc_map``) 
   THEN All (RepUR ``nat-trans op-cat cube-cat type-cat cat-ob``)
   THEN All (RepUR ``cat-arrow cat-comp functor-arrow functor-ob``)
   THEN RepUR ``context-subset compose`` 0
   THEN DSetVars
   THEN MemTypeCD) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. Z : CubicalSet{j}
4. s : A:fset(ℕ) ⟶ ((fst(Z)) A) ⟶ ((fst(Gamma)) A)
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.
     ((((snd(Gamma)) A B g) o (s A)) = ((s B) o ((snd(Z)) A B g)) ∈ (((fst(Z)) A) ⟶ ((fst(Gamma)) B)))
6. s ∈ Z j⟶ Gamma
7. (phi)s ∈ {Z ⊢ _:𝔽}
⊢ s ∈ A:fset(ℕ)
  ⟶ {rho:Z(A)| (phi)s(rho) = 1 ∈ Point(face_lattice(A))} 
  ⟶ {rho:Gamma(A)| phi(rho) = 1 ∈ Point(face_lattice(A))} 

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. Z : CubicalSet{j}
4. s : A:fset(ℕ) ⟶ ((fst(Z)) A) ⟶ ((fst(Gamma)) A)
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.
     ((((snd(Gamma)) A B g) o (s A)) = ((s B) o ((snd(Z)) A B g)) ∈ (((fst(Z)) A) ⟶ ((fst(Gamma)) B)))
6. s ∈ Z j⟶ Gamma
7. (phi)s ∈ {Z ⊢ _:𝔽}
⊢ ∀A,B:fset(ℕ). ∀g:B ⟶ A.
    ((λx.g(s A x))
    = (λx.(s B g(x)))
    ∈ ({rho:Z(A)| (phi)s(rho) = 1 ∈ Point(face_lattice(A))}  ⟶ {rho:Gamma(B)| phi(rho) = 1 ∈ Point(face_lattice(B))} ))

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. Z : CubicalSet{j}
4. s : A:fset(ℕ) ⟶ ((fst(Z)) A) ⟶ ((fst(Gamma)) A)
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.
     ((((snd(Gamma)) A B g) o (s A)) = ((s B) o ((snd(Z)) A B g)) ∈ (((fst(Z)) A) ⟶ ((fst(Gamma)) B)))
6. s ∈ Z j⟶ Gamma
7. (phi)s ∈ {Z ⊢ _:𝔽}
8. trans : A:fset(ℕ)
⟶ {rho:Z(A)| (phi)s(rho) = 1 ∈ Point(face_lattice(A))} 
⟶ {rho:Gamma(A)| phi(rho) = 1 ∈ Point(face_lattice(A))} 
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.
           ((λx.g(trans A x))
           = (λx.(trans B g(x)))
           ∈ ({rho:Z(A)| (phi)s(rho) = 1 ∈ Point(face_lattice(A))}  ⟶ {rho:Gamma(B)| 
                                                                      phi(rho) = 1 ∈ Point(face_lattice(B))} )))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[Z:j\mvdash{}].  \mforall{}[s:Z  j{}\mrightarrow{}  Gamma].    (s  \mmember{}  Z,  (phi)s  j{}\mrightarrow{}  Gamma,  phi)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  s  \mmember{}  Z  j{}\mrightarrow{}  Gamma  BY
                          Trivial)
  THEN  (Assert  (phi)s  \mmember{}  \{Z  \mvdash{}  \_:\mBbbF{}\}  BY
                          Auto)
  THEN  RepUR  ``cube\_set\_map  psc\_map``  0
  THEN  OnVar  `s'  (RepUR  ``cube\_set\_map  psc\_map``) 
  THEN  All  (RepUR  ``nat-trans  op-cat  cube-cat  type-cat  cat-ob``)
  THEN  All  (RepUR  ``cat-arrow  cat-comp  functor-arrow  functor-ob``)
  THEN  RepUR  ``context-subset  compose``  0
  THEN  DSetVars
  THEN  MemTypeCD)

---

Home Index