Mercurial > hg > Members > kono > Proof > category

comparison src/idF.agda @ 949:ac53803b3b2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganization for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 16:40:15 +0900
parents idF.agda@3249aaddc405
children 45de2b31bf02
comparison
equal deleted inserted replaced
948:dca4b29553cb 949:ac53803b3b2a
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