---

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

No Annotations
∀[C:SmallCategory]. ∀[T:𝕌{j}]. ∀[I:cat-ob(C)]. ∀[s:psc_map{[i | j]:l}(C; Yoneda(I); discrete-set(T))].
  (s = (λJ,g. (s I (cat-id(C) I))) ∈ psc_map{[i | j]:l}(C; Yoneda(I); discrete-set(T)))
BY
{ (Intros
   THEN D -1
   THEN RepUR ``type-cat discrete-set compose Yoneda`` -1
   THEN RepUR ``type-cat discrete-set compose Yoneda`` -2
   THEN EqTypeCD
   THEN RepUR ``type-cat discrete-set compose Yoneda`` 0
   THEN Try (Trivial)) }

1
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))
⊢ s = (λJ,g. (s I (cat-id(C) I))) ∈ (A:cat-ob(op-cat(C)) ⟶ (cat-arrow(C) A I) ⟶ T)

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[T:\mBbbU{}\{j\}].  \mforall{}[I:cat-ob(C)].
\mforall{}[s:psc\_map\{[i  |  j]:l\}(C;  Yoneda(I);  discrete-set(T))].
    (s  =  (\mlambda{}J,g.  (s  I  (cat-id(C)  I))))


By

---

Latex:
(Intros
  THEN  D  -1
  THEN  RepUR  ``type-cat  discrete-set  compose  Yoneda``  -1
  THEN  RepUR  ``type-cat  discrete-set  compose  Yoneda``  -2
  THEN  EqTypeCD
  THEN  RepUR  ``type-cat  discrete-set  compose  Yoneda``  0
  THEN  Try  (Trivial))

---

Home Index