---

Step * of Lemma ps_context-ext

No Annotations
∀[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
{ (Intro THEN Unhide) }

1
.....wf..... 
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)))}  ∈ 𝕌{[j 2 | i]}

2
.....wf..... 
1. C : SmallCategory
⊢ ps_context{j:l}(C) ∈ 𝕌{[j 2 | i]}

3
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory]
    \{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:
(Intro  THEN  Unhide)

---

Home Index