---

Step * of Lemma unit-functor-is-const

∀[A:SmallCategory]. ∀f:Functor(1;A). ∃a:cat-ob(A). (f = const-functor(A;a) ∈ Functor(1;A))
BY
{ (Auto
   THEN (D 0 With ⌜ob(f) ⋅⌝  THEN Auto)
   THEN BLemma `equal-functors`
   THEN Auto
   THEN OnVar `f' DFunctor
   THEN All (RepUR ``const-functor unit-cat discrete-cat mk-cat``)) }

1
1. A : SmallCategory
2. fob : Unit ⟶ cat-ob(A)
3. farrow : x:Unit ⟶ y:Unit ⟶ (x = y ∈ Unit) ⟶ (cat-arrow(A) (fob x) (fob y))
4. ∀x:Unit. ((farrow x x ⋅) = (cat-id(A) (fob x)) ∈ (cat-arrow(A) (fob x) (fob x)))
5. ∀x,y,z:Unit. ∀f:x = y ∈ Unit. ∀g:y = z ∈ Unit.
     ((farrow x z ⋅)
     = (cat-comp(A) (fob x) (fob y) (fob z) (farrow x y f) (farrow y z g))
     ∈ (cat-arrow(A) (fob x) (fob z)))
6. x : Unit
⊢ (fob x) = (fob ⋅) ∈ cat-ob(A)

2
1. A : SmallCategory
2. fob : Unit ⟶ cat-ob(A)
3. farrow : x:Unit ⟶ y:Unit ⟶ (x = y ∈ Unit) ⟶ (cat-arrow(A) (fob x) (fob y))
4. ∀x:Unit. ((farrow x x ⋅) = (cat-id(A) (fob x)) ∈ (cat-arrow(A) (fob x) (fob x)))
5. ∀x,y,z:Unit. ∀f:x = y ∈ Unit. ∀g:y = z ∈ Unit.
     ((farrow x z ⋅)
     = (cat-comp(A) (fob x) (fob y) (fob z) (farrow x y f) (farrow y z g))
     ∈ (cat-arrow(A) (fob x) (fob z)))
6. x : Unit
7. y : Unit
8. f1 : x = y ∈ Unit
⊢ (farrow x y f1) = (cat-id(A) (fob ⋅)) ∈ (cat-arrow(A) (fob x) (fob y))

---

Latex:

---

Latex:
\mforall{}[A:SmallCategory].  \mforall{}f:Functor(1;A).  \mexists{}a:cat-ob(A).  (f  =  const-functor(A;a))


By

---

Latex:
(Auto
  THEN  (D  0  With  \mkleeneopen{}ob(f)  \mcdot{}\mkleeneclose{}    THEN  Auto)
  THEN  BLemma  `equal-functors`
  THEN  Auto
  THEN  OnVar  `f'  DFunctor
  THEN  All  (RepUR  ``const-functor  unit-cat  discrete-cat  mk-cat``))

---

Home Index