view idF.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 3249aaddc405
line wrap: on
line source
```
module idF where

open import Category
open import HomReasoning

identityFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → Functor C C
identityFunctor {C = C} = record {
FObj      = λ x → x
; FMap      = λ x → x
; isFunctor = isFunctor
}
where
isFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → IsFunctor C C (λ x → x) (λ x → x)
isFunctor {C = C} =
record { ≈-cong   = Lemma1
; identity = Lemma2
; distr    = Lemma3
} where
FMap : {a b : Obj C} -> Hom C a b -> Hom C a b
FMap = λ x → x
FObj : Obj C -> Obj C
FObj = λ x → x
Lemma1 : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ FMap f ≈ FMap g ]
Lemma1 {a} {b} {f} {g}  f≈g = let open ≈-Reasoning C in
begin
FMap f
≈⟨⟩
f
≈⟨ f≈g  ⟩
g
≈⟨⟩
FMap g
∎
Lemma2 : {A : Obj C} →  C [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {C} (FObj A)) ]
Lemma2 {A} = let open ≈-Reasoning C in
begin
(FMap {A} {A} (Id {_} {_} {_} {C} A))
≈⟨⟩
(Id {_} {_} {_} {C} (FObj A))
∎
Lemma3 : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
→ C [ FMap (C [ g o f ]) ≈ (C [ FMap g o FMap f ] )]
Lemma3 {a} {b} {c} {f} {g}  = let open ≈-Reasoning C in
begin
FMap ( g o f )
≈⟨⟩
g o f
≈⟨⟩
FMap g o FMap f
∎

```