|
153
|
1 module idF where
|
|
|
2
|
|
|
3 open import Category
|
|
|
4 open import HomReasoning
|
|
|
5
|
|
|
6 identityFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → Functor C C
|
|
|
7 identityFunctor {C = C} = record {
|
|
|
8 FObj = λ x → x
|
|
|
9 ; FMap = λ x → x
|
|
|
10 ; isFunctor = isFunctor
|
|
|
11 }
|
|
|
12 where
|
|
|
13 isFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → IsFunctor C C (λ x → x) (λ x → x)
|
|
|
14 isFunctor {C = C} =
|
|
|
15 record { ≈-cong = Lemma1
|
|
|
16 ; identity = Lemma2
|
|
|
17 ; distr = Lemma3
|
|
|
18 } where
|
|
|
19 FMap : {a b : Obj C} -> Hom C a b -> Hom C a b
|
|
|
20 FMap = λ x → x
|
|
|
21 FObj : Obj C -> Obj C
|
|
|
22 FObj = λ x → x
|
|
|
23 Lemma1 : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ FMap f ≈ FMap g ]
|
|
|
24 Lemma1 {a} {b} {f} {g} f≈g = let open ≈-Reasoning C in
|
|
|
25 begin
|
|
|
26 FMap f
|
|
|
27 ≈⟨⟩
|
|
|
28 f
|
|
|
29 ≈⟨ f≈g ⟩
|
|
|
30 g
|
|
|
31 ≈⟨⟩
|
|
|
32 FMap g
|
|
|
33 ∎
|
|
|
34 Lemma2 : {A : Obj C} → C [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {C} (FObj A)) ]
|
|
|
35 Lemma2 {A} = let open ≈-Reasoning C in
|
|
|
36 begin
|
|
|
37 (FMap {A} {A} (Id {_} {_} {_} {C} A))
|
|
|
38 ≈⟨⟩
|
|
|
39 (Id {_} {_} {_} {C} (FObj A))
|
|
|
40 ∎
|
|
|
41 Lemma3 : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
|
|
|
42 → C [ FMap (C [ g o f ]) ≈ (C [ FMap g o FMap f ] )]
|
|
|
43 Lemma3 {a} {b} {c} {f} {g} = let open ≈-Reasoning C in
|
|
|
44 begin
|
|
|
45 FMap ( g o f )
|
|
|
46 ≈⟨⟩
|
|
|
47 g o f
|
|
|
48 ≈⟨⟩
|
|
|
49 FMap g o FMap f
|
|
|
50 ∎
|
|
|
51
|
|
|
52
|
|
|
53
|
|
|
54
|
|
|
55
|
