Mercurial > hg > Members > kono > Proof > category
annotate src/idF.agda @ 1124:f683d96fbc93 default tip
safe fix done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2024 22:28:50 +0900 |
| parents | 45de2b31bf02 |
| children |
| rev | line source |
|---|---|
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
2 |
| 153 | 3 module idF where |
| 4 | |
| 5 open import Category | |
| 6 open import HomReasoning | |
| 7 | |
| 8 identityFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → Functor C C | |
| 9 identityFunctor {C = C} = record { | |
| 10 FObj = λ x → x | |
| 11 ; FMap = λ x → x | |
| 12 ; isFunctor = isFunctor | |
| 13 } | |
| 14 where | |
| 15 isFunctor : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} → IsFunctor C C (λ x → x) (λ x → x) | |
| 16 isFunctor {C = C} = | |
| 17 record { ≈-cong = Lemma1 | |
| 18 ; identity = Lemma2 | |
| 19 ; distr = Lemma3 | |
| 20 } where | |
| 21 FMap : {a b : Obj C} -> Hom C a b -> Hom C a b | |
| 22 FMap = λ x → x | |
| 23 FObj : Obj C -> Obj C | |
| 24 FObj = λ x → x | |
| 25 Lemma1 : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ FMap f ≈ FMap g ] | |
| 26 Lemma1 {a} {b} {f} {g} f≈g = let open ≈-Reasoning C in | |
| 27 begin | |
| 28 FMap f | |
| 29 ≈⟨⟩ | |
| 30 f | |
| 31 ≈⟨ f≈g ⟩ | |
| 32 g | |
| 33 ≈⟨⟩ | |
| 34 FMap g | |
| 35 ∎ | |
| 36 Lemma2 : {A : Obj C} → C [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {C} (FObj A)) ] | |
| 37 Lemma2 {A} = let open ≈-Reasoning C in | |
| 38 begin | |
| 39 (FMap {A} {A} (Id {_} {_} {_} {C} A)) | |
| 40 ≈⟨⟩ | |
| 41 (Id {_} {_} {_} {C} (FObj A)) | |
| 42 ∎ | |
| 43 Lemma3 : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c} | |
| 44 → C [ FMap (C [ g o f ]) ≈ (C [ FMap g o FMap f ] )] | |
| 45 Lemma3 {a} {b} {c} {f} {g} = let open ≈-Reasoning C in | |
| 46 begin | |
| 47 FMap ( g o f ) | |
| 48 ≈⟨⟩ | |
| 49 g o f | |
| 50 ≈⟨⟩ | |
| 51 FMap g o FMap f | |
| 52 ∎ | |
| 53 | |
| 54 | |
| 55 | |
| 56 | |
| 57 |