---

Step * 3 of Lemma ps_context-ext


1. C : SmallCategory
⊢ {FM:F:cat-ob(C) ⟶ 𝕌{j'} × (I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ (cat-arrow(C) J I) ⟶ (F I) ⟶ (F J))| 
   let F,M = FM 
   in (∀I:cat-ob(C). ∀s:FM(I).  (cat-id(C) I(s) = s ∈ FM(I)))
      ∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀s:FM(I).
           (cat-comp(C) K J I g f(s) = g(f(s)) ∈ FM(K)))}  ≡ ps_context{j:l}(C)
BY
{ (DCat 1
   THEN RepUR ``ps_context cat-functor op-cat names-cat type-cat cat-ob cat-arrow`` 0
   THEN RepUR ``cat-id cat-comp I_set psc-restriction compose`` 0
   THEN RepUR ``functor-ob`` 0) }

1
1. Cob : Type
2. Carrow : Cob ⟶ Cob ⟶ Type
3. Cid : x:Cob ⟶ (Carrow x x)
4. Ccomp : x:Cob ⟶ y:Cob ⟶ z:Cob ⟶ (Carrow x y) ⟶ (Carrow y z) ⟶ (Carrow x z)
5. [%1] : (∀x,y:Cob. ∀f:Carrow x y.
             (((Ccomp x x y (Cid x) f) = f ∈ (Carrow x y)) ∧ ((Ccomp x y y f (Cid y)) = f ∈ (Carrow x y))))
∧ (∀x,y,z,w:Cob. ∀f:Carrow x y. ∀g:Carrow y z. ∀h:Carrow z w.
     ((Ccomp x z w (Ccomp x y z f g) h) = (Ccomp x y w f (Ccomp y z w g h)) ∈ (Carrow x w)))
⊢ {FM:F:Cob ⟶ 𝕌{j'} × (I:Cob ⟶ J:Cob ⟶ (Carrow J I) ⟶ (F I) ⟶ (F J))| 
   let F,M = FM 
   in (∀I:Cob. ∀s:(fst(FM)) I.  (((snd(FM)) I I (Cid I) s) = s ∈ ((fst(FM)) I)))
      ∧ (∀I,J,K:Cob. ∀f:Carrow J I. ∀g:Carrow K J. ∀s:(fst(FM)) I.
           (((snd(FM)) I K (Ccomp K J I g f) s) = ((snd(FM)) J K g ((snd(FM)) I J f s)) ∈ ((fst(FM)) K)))}  ≡
  {FM:F:Cob ⟶ 𝕌{j'} × (x:Cob ⟶ y:Cob ⟶ (Carrow y x) ⟶ (F x) ⟶ (F y))| 
   let F,M = FM 
   in (∀x:Cob. ((M x x (Cid x)) = (λx.x) ∈ ((F x) ⟶ (F x))))
      ∧ (∀x,y,z:Cob. ∀f:Carrow y x. ∀g:Carrow z y.
           ((M x z (Ccomp z y x g f)) = (λx@0.(M y z g (M x y f x@0))) ∈ ((F x) ⟶ (F z))))} 

---

Latex:

---

Latex:

1.  C  :  SmallCategory
\mvdash{}  \{FM:F:cat-ob(C)  {}\mrightarrow{}  \mBbbU{}\{j'\}  \mtimes{}  (I:cat-ob(C)  {}\mrightarrow{}  J:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  J  I)  {}\mrightarrow{}  (F  I)  {}\mrightarrow{}  (F  J))| 
      let  F,M  =  FM 
      in  (\mforall{}I:cat-ob(C).  \mforall{}s:FM(I).    (cat-id(C)  I(s)  =  s))
            \mwedge{}  (\mforall{}I,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}s:FM(I).
                      (cat-comp(C)  K  J  I  g  f(s)  =  g(f(s))))\}    \mequiv{}  ps\_context\{j:l\}(C)


By

---

Latex:
(DCat  1
  THEN  RepUR  ``ps\_context  cat-functor  op-cat  names-cat  type-cat  cat-ob  cat-arrow``  0
  THEN  RepUR  ``cat-id  cat-comp  I\_set  psc-restriction  compose``  0
  THEN  RepUR  ``functor-ob``  0)

---

Home Index