Mercurial > hg > Members > kono > Proof > category

comparison CatExponetial.agda @ 267:b1b728559d89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constancy Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 17:26:47 +0900
parents eb935f04bf39
children d6a6dd305da2
comparison
equal deleted inserted replaced
266:9e9f1e27e89f 267:b1b728559d89
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> 4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
5 ---- 5 ----
6 6
7 open import Category -- https://github.com/konn/category-agda 7 open import Category -- https://github.com/konn/category-agda
8 open import Level 8 open import Level
9 module CatExponetial {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') where 9 module CatExponetial where
10
11 -- {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' }
10 12
11 open import HomReasoning 13 open import HomReasoning
12 open import cat-utility 14 open import cat-utility
13 15
14 16
15 -- Object is a Functor : A → B 17 -- Object is a Functor : A → B
16 -- Hom is a natural transformation 18 -- Hom is a natural transformation
17 19
18 open Functor 20 open Functor
19 21
20 CObj = Functor A B 22 CObj = λ {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') → Functor A B
21 CHom = λ (f : CObj ) → λ (g : CObj ) → NTrans A B f g 23 CHom = λ {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (f g : CObj A B ) → NTrans A B f g
22 24
23 open NTrans 25 open NTrans
24 Cid : {a : CObj} → CHom a a 26 Cid : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) {a : CObj A B } → CHom A B a a
25 Cid {a} = record { TMap = \x -> id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where 27 Cid {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B {a} = record { TMap = \x -> id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
26 commute : {a : CObj} {a₁ b : Obj A} {f : Hom A a₁ b} → 28 commute : {a : CObj A B } {a₁ b : Obj A} {f : Hom A a₁ b} →
27 B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈ 29 B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈
28 B [ id1 B (FObj a b) o FMap a f ] ] 30 B [ id1 B (FObj a b) o FMap a f ] ]
29 commute {a} {a₁} {b} {f} = let open ≈-Reasoning B in begin 31 commute {a} {a₁} {b} {f} = let open ≈-Reasoning B in begin
30 FMap a f o id1 B (FObj a a₁) 32 FMap a f o id1 B (FObj a a₁)
31 ≈⟨ idR ⟩ 33 ≈⟨ idR ⟩
32 FMap a f 34 FMap a f
33 ≈↑⟨ idL ⟩ 35 ≈↑⟨ idL ⟩
34 id1 B (FObj a b) o FMap a f 36 id1 B (FObj a b) o FMap a f
35 ∎ 37 ∎
36 isNTrans1 : {a : CObj } → IsNTrans A B a a (\x -> id1 B (FObj a x)) 38 isNTrans1 : {a : CObj A B } → IsNTrans A B a a (\x -> id1 B (FObj a x))
37 isNTrans1 {a} = record { commute = \{a₁ b f} -> commute {a} {a₁} {b} {f} } 39 isNTrans1 {a} = record { commute = \{a₁ b f} -> commute {a} {a₁} {b} {f} }
38 40
39 _+_ : {a b c : CObj} → CHom b c → CHom a b → CHom a c 41 _+_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } {a b c : CObj A B }
40 _+_{a} {b} {c} f g = record { TMap = λ x → B [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where 42 → CHom A B b c → CHom A B a b → CHom A B a c
41 commute1 : (a b c : CObj ) (f : CHom b c) (g : CHom a b ) 43 _+_ {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {A} {B} {a} {b} {c} f g = record { TMap = λ x → B [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where
44 commute1 : (a b c : CObj A B ) (f : CHom A B b c) (g : CHom A B a b )
42 (a₁ b₁ : Obj A) (h : Hom A a₁ b₁) → 45 (a₁ b₁ : Obj A) (h : Hom A a₁ b₁) →
43 B [ B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ] ≈ 46 B [ B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ] ≈
44 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] 47 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
45 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning B in begin 48 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning B in begin
46 B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ] 49 B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ]
56 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ] 59 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ]
57 ∎ 60 ∎
58 isNTrans1 : IsNTrans A B a c (λ x → B [ TMap f x o TMap g x ]) 61 isNTrans1 : IsNTrans A B a c (λ x → B [ TMap f x o TMap g x ])
59 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } 62 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
60 63
61 _==_ : {a b : CObj} → CHom a b → CHom a b → Set (ℓ' ⊔ c₁) 64 _==_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } {a b : CObj A B } →
62 _==_ {a} {b} f g = ∀{x} → B [ TMap f x ≈ TMap g x ] 65 CHom A B a b → CHom A B a b → Set (ℓ' ⊔ c₁)
66 _==_ {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {A} {B} {a} {b} f g = ∀{x} → B [ TMap f x ≈ TMap g x ]
63 67
64 infix 4 _==_ 68 infix 4 _==_
65 69
66 open import Relation.Binary.Core 70 open import Relation.Binary.Core
67 isB^A : IsCategory CObj CHom _==_ _+_ Cid 71 isB^A : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) → IsCategory (CObj A B) (CHom A B) _==_ _+_ (Cid A B)
68 isB^A = 72 isB^A {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B =
69 record { isEquivalence = record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B )); 73 record { isEquivalence = record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B ));
70 sym = \{i j} → sym1 {_} {_} {i} {j} ; 74 sym = \{i j} → sym1 {_} {_} {i} {j} ;
71 trans = \{i j k} → trans1 {_} {_} {i} {j} {k} } 75 trans = \{i j k} → trans1 {_} {_} {i} {j} {k} }
72 ; identityL = IsCategory.identityL ( Category.isCategory B ) 76 ; identityL = IsCategory.identityL ( Category.isCategory B )
73 ; identityR = IsCategory.identityR ( Category.isCategory B ) 77 ; identityR = IsCategory.identityR ( Category.isCategory B )
74 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} 78 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈1 {a} {b} {c} {f} {g} {h} {i}
75 ; associative = IsCategory.associative ( Category.isCategory B ) 79 ; associative = IsCategory.associative ( Category.isCategory B )
76 } where 80 } where
77 sym1 : {a b : CObj } {i j : CHom a b } → i == j → j == i 81 sym1 : {a b : CObj A B } {i j : CHom A B a b } → i == j → j == i
78 sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin 82 sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin
79 TMap j x 83 TMap j x
80 ≈⟨ sym eq ⟩ 84 ≈⟨ sym eq ⟩
81 TMap i x 85 TMap i x
82 ∎ 86 ∎
83 trans1 : {a b : CObj } {i j k : CHom a b} → i == j → j == k → i == k 87 trans1 : {a b : CObj A B } {i j k : CHom A B a b} → i == j → j == k → i == k
84 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning B in begin 88 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning B in begin
85 TMap i x 89 TMap i x
86 ≈⟨ i=j ⟩ 90 ≈⟨ i=j ⟩
87 TMap j x 91 TMap j x
88 ≈⟨ j=k ⟩ 92 ≈⟨ j=k ⟩
89 TMap k x 93 TMap k x
90 ∎ 94 ∎
91 o-resp-≈1 : {a b c : CObj} {f g : CHom a b} {h i : CHom b c } → 95 o-resp-≈1 : {a b c : CObj A B } {f g : CHom A B a b} {h i : CHom A B b c } →
92 f == g → h == i → h + f == i + g 96 f == g → h == i → h + f == i + g
93 o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning B in begin 97 o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning B in begin
94 TMap h x o TMap f x 98 TMap h x o TMap f x
95 ≈⟨ resp f=g h=i ⟩ 99 ≈⟨ resp f=g h=i ⟩
96 TMap i x o TMap g x 100 TMap i x o TMap g x
97 ∎ 101 ∎
98 102
99 B^A : Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) (ℓ' ⊔ c₁) 103 _^_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ' ) (B : Category c₁ c₂ ℓ) →
100 B^A = 104 Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))
101 record { Obj = CObj 105 (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))
102 ; Hom = CHom 106 (ℓ' ⊔ c₁)
107 _^_ {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} B A =
108 record { Obj = CObj A B
109 ; Hom = CHom A B
103 ; _o_ = _+_ 110 ; _o_ = _+_
104 ; _≈_ = _==_ 111 ; _≈_ = _==_
105 ; Id = Cid 112 ; Id = Cid A B
106 ; isCategory = isB^A 113 ; isCategory = isB^A A B
107 } 114 }
108 115