---

Step * 2 of Lemma ps-discrete-map-is-constant


1. C : SmallCategory
2. T : 𝕌{j}
3. I : cat-ob(C)
4. s : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(C) A I) ⟶ T
5. ∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
     ((λx.(s A x)) = (λx.(s B (cat-comp(C) B A I g x))) ∈ ((cat-arrow(C) A I) ⟶ T))
6. trans : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{[i | j]':l}) (Yoneda(I) A) (discrete-set(T) A))
⊢ istype(∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
           ((λx.(trans A x)) = (λx.(trans B (cat-comp(C) B A I g x))) ∈ ((cat-arrow(C) A I) ⟶ T)))
BY
{ (RepUR ``type-cat discrete-set compose Yoneda`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  T  :  \mBbbU{}\{j\}
3.  I  :  cat-ob(C)
4.  s  :  A:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(C)  A  I)  {}\mrightarrow{}  T
5.  \mforall{}A,B:cat-ob(op-cat(C)).  \mforall{}g:cat-arrow(op-cat(C))  A  B.
          ((\mlambda{}x.(s  A  x))  =  (\mlambda{}x.(s  B  (cat-comp(C)  B  A  I  g  x))))
6.  trans  :  A:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(type-cat\{[i  |  j]':l\})  (Yoneda(I)  A) 
                                                                      (discrete-set(T)  A))
\mvdash{}  istype(\mforall{}A,B:cat-ob(op-cat(C)).  \mforall{}g:cat-arrow(op-cat(C))  A  B.
                      ((\mlambda{}x.(trans  A  x))  =  (\mlambda{}x.(trans  B  (cat-comp(C)  B  A  I  g  x)))))


By

---

Latex:
(RepUR  ``type-cat  discrete-set  compose  Yoneda``  -1  THEN  Auto)

---

Home Index