---

Step * 1 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))
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
BY
{ ((ApFunToHypEquands `Z' ⌜Z (cat-id(C) I)⌝ ⌜T⌝ (-1)⋅ THENA Auto)
   THEN Reduce -1
   THEN NthHypEqTrans (-1)
   THEN EqCD
   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.  A  :  cat-ob(op-cat(C))
7.  x  :  cat-arrow(C)  A  I
8.  (\mlambda{}x.(s  I  x))  =  (\mlambda{}x@0.(s  A  (cat-comp(C)  A  I  I  x  x@0)))
\mvdash{}  (s  A  x)  =  (s  I  (cat-id(C)  I))


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  (cat-id(C)  I)\mkleeneclose{}  \mkleeneopen{}T\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  NthHypEqTrans  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index