---

Step * 1 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))
⊢ s = (λJ,g. (s I (cat-id(C) I))) ∈ (A:cat-ob(op-cat(C)) ⟶ (cat-arrow(C) A I) ⟶ T)
BY
{ ((RepeatFor 2 ((FunExt THENA Auto)) THEN Reduce 0) THEN (InstHyp [⌜I⌝;⌜A⌝;⌜x⌝] (-3)⋅ THENA Auto)) }

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))
6. A : cat-ob(op-cat(C))
7. x : cat-arrow(C) A I
8. (λx.(s I x)) = (λx@0.(s A (cat-comp(C) A I I x x@0))) ∈ ((cat-arrow(C) I I) ⟶ T)
⊢ (s A x) = (s I (cat-id(C) I)) ∈ T

---

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))))
\mvdash{}  s  =  (\mlambda{}J,g.  (s  I  (cat-id(C)  I)))


By

---

Latex:
((RepeatFor  2  ((FunExt  THENA  Auto))  THEN  Reduce  0)  THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))

---

Home Index