31
|
1 module CatReasoning where
|
|
2
|
|
3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
4
|
|
5 open import Category -- https://github.com/konn/category-agda
|
|
6 open import Level
|
|
7 open Functor
|
|
8
|
|
9
|
|
10 -- F(f)
|
|
11 -- F(a) ---→ F(b)
|
|
12 -- | |
|
|
13 -- |t(a) |t(b) G(f)t(a) = t(b)F(f)
|
|
14 -- | |
|
|
15 -- v v
|
|
16 -- G(a) ---→ G(b)
|
|
17 -- G(f)
|
|
18
|
|
19 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
|
|
20 ( F G : Functor D C )
|
|
21 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
|
|
22 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
23 field
|
|
24 naturality : {a b : Obj D} {f : Hom D a b}
|
|
25 → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ]
|
|
26
|
|
27 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
|
|
28 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
|
|
29 field
|
|
30 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
|
|
31 isNTrans : IsNTrans domain codomain F G TMap
|
|
32
|
|
33
|
|
34
|
|
35 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
|
|
36 open import Relation.Binary.Core
|
|
37
|
|
38 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
|
|
39 x o y = A [ x o y ]
|
|
40
|
|
41 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ
|
|
42 x ≈ y = A [ x ≈ y ]
|
|
43
|
|
44 infixr 9 _o_
|
|
45 infix 4 _≈_
|
|
46
|
|
47 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x
|
|
48 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))
|
|
49
|
|
50 trans-hom : {a b : Obj A } { x y z : Hom A a b } →
|
|
51 x ≈ y → y ≈ z → x ≈ z
|
|
52 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c
|
|
53
|
|
54 -- some short cuts
|
|
55
|
|
56 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
|
|
57 x ≈ y → ( x o f ) ≈ ( y o f )
|
|
58 car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq
|
|
59
|
|
60 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
|
|
61 x ≈ y → f o x ≈ f o y
|
|
62 cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom )
|
|
63
|
|
64 id : (a : Obj A ) → Hom A a a
|
|
65 id a = (Id {_} {_} {_} {A} a)
|
|
66
|
|
67 idL : {a b : Obj A } { f : Hom A b a } → id a o f ≈ f
|
|
68 idL = IsCategory.identityL (Category.isCategory A)
|
|
69
|
|
70 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f
|
|
71 idR = IsCategory.identityR (Category.isCategory A)
|
|
72
|
|
73 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f
|
|
74 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
|
|
75
|
|
76 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b}
|
|
77 → f o ( g o h ) ≈ ( f o g ) o h
|
|
78 assoc = IsCategory.associative (Category.isCategory A)
|
|
79
|
|
80 distr : (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
|
|
81 → FMap T ( g o f ) ≈ FMap T g o FMap T f
|
|
82 distr T = IsFunctor.distr ( isFunctor T )
|
|
83
|
|
84 open NTrans
|
|
85 nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A }
|
|
86 → (η : NTrans D A F G )
|
|
87 → FMap G f o TMap η a ≈ TMap η b o FMap F f
|
|
88 nat _ η = IsNTrans.naturality ( isNTrans η )
|
|
89
|
|
90
|
|
91 infixr 2 _∎
|
|
92 infixr 2 _≈⟨_⟩_ _≈⟨⟩_
|
|
93 infix 1 begin_
|
|
94
|
|
95 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
|
|
96 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y
|
|
97 -- ≈-to-≡ refl-hom = refl
|
|
98
|
|
99 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
|
|
100 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
101 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y
|
|
102
|
|
103 begin_ : { a b : Obj A } { x y : Hom A a b } →
|
|
104 x IsRelatedTo y → x ≈ y
|
|
105 begin relTo x≈y = x≈y
|
|
106
|
|
107 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } →
|
|
108 x ≈ y → y IsRelatedTo z → x IsRelatedTo z
|
|
109 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
|
|
110
|
|
111 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
|
|
112 _ ≈⟨⟩ x∼y = x∼y
|
|
113
|
|
114 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
|
|
115 _∎ _ = relTo refl-hom
|
|
116
|