Step
*
of Lemma
unit-functor-is-const
No Annotations
∀[A:SmallCategory]. ∀f:Functor(1;A). ∃a:cat-ob(A). (f = const-functor(A;a) ∈ Functor(1;A))
BY
{ (Auto
THEN (D 0 With ⌜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)@i
3. farrow : x:Unit ⟶ y:Unit ⟶ (x = y ∈ Unit) ⟶ (cat-arrow(A) (fob x) (fob y))@i
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@i
⊢ (fob x) = (fob ⋅) ∈ cat-ob(A)
2
1. A : SmallCategory
2. fob : Unit ⟶ cat-ob(A)@i
3. farrow : x:Unit ⟶ y:Unit ⟶ (x = y ∈ Unit) ⟶ (cat-arrow(A) (fob x) (fob y))@i
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@i
7. y : Unit@i
8. f1 : x = y ∈ Unit@i
⊢ (farrow x y f1) = (cat-id(A) (fob ⋅)) ∈ (cat-arrow(A) (fob x) (fob y))
Latex:
Latex:
No Annotations
\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{}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