annotate CatReasoning.agda @ 31:17b8bafebad7

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