Mercurial > hg > Members > kono > Proof > category

comparison CatReasoning.agda @ 31:17b8bafebad7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add universal mapping
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 14:30:27 +0900
parents
children
comparison
equal deleted inserted replaced
30:98b8431a419b 31:17b8bafebad7
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