|
200
|
1 ----
|
|
|
2 --
|
|
|
3 -- B^A
|
|
|
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
|
5 ----
|
|
|
6
|
|
|
7 open import Category -- https://github.com/konn/category-agda
|
|
|
8 open import Level
|
|
267
|
9 module CatExponetial where
|
|
|
10
|
|
|
11 -- {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' }
|
|
200
|
12
|
|
|
13 open import HomReasoning
|
|
|
14 open import cat-utility
|
|
|
15
|
|
|
16
|
|
|
17 -- Object is a Functor : A → B
|
|
|
18 -- Hom is a natural transformation
|
|
|
19
|
|
|
20 open Functor
|
|
|
21
|
|
267
|
22 CObj = λ {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') → Functor A B
|
|
|
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
|
|
200
|
24
|
|
|
25 open NTrans
|
|
267
|
26 Cid : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) {a : CObj A B } → CHom A B a a
|
|
300
|
27 Cid {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B {a} = record { TMap = λ x → id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
|
|
267
|
28 commute : {a : CObj A B } {a₁ b : Obj A} {f : Hom A a₁ b} →
|
|
200
|
29 B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈
|
|
|
30 B [ id1 B (FObj a b) o FMap a f ] ]
|
|
|
31 commute {a} {a₁} {b} {f} = let open ≈-Reasoning B in begin
|
|
|
32 FMap a f o id1 B (FObj a a₁)
|
|
|
33 ≈⟨ idR ⟩
|
|
|
34 FMap a f
|
|
|
35 ≈↑⟨ idL ⟩
|
|
|
36 id1 B (FObj a b) o FMap a f
|
|
|
37 ∎
|
|
300
|
38 isNTrans1 : {a : CObj A B } → IsNTrans A B a a (λ x → id1 B (FObj a x))
|
|
|
39 isNTrans1 {a} = record { commute = λ {a₁ b f} → commute {a} {a₁} {b} {f} }
|
|
200
|
40
|
|
267
|
41 _+_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } {a b c : CObj A B }
|
|
|
42 → CHom A B b c → CHom A B a b → CHom A B a c
|
|
|
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 )
|
|
200
|
45 (a₁ b₁ : Obj A) (h : Hom A a₁ b₁) →
|
|
|
46 B [ B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ] ≈
|
|
|
47 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
|
|
|
48 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning B in begin
|
|
|
49 B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ]
|
|
|
50 ≈⟨ assoc ⟩
|
|
|
51 B [ B [ FMap c h o TMap f a₁ ] o TMap g a₁ ]
|
|
|
52 ≈⟨ car (nat f) ⟩
|
|
|
53 B [ B [ TMap f b₁ o FMap b h ] o TMap g a₁ ]
|
|
|
54 ≈↑⟨ assoc ⟩
|
|
|
55 B [ TMap f b₁ o B [ FMap b h o TMap g a₁ ] ]
|
|
|
56 ≈⟨ cdr (nat g) ⟩
|
|
|
57 B [ TMap f b₁ o B [ TMap g b₁ o FMap a h ] ]
|
|
|
58 ≈⟨ assoc ⟩
|
|
|
59 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ]
|
|
|
60 ∎
|
|
|
61 isNTrans1 : IsNTrans A B a c (λ x → B [ TMap f x o TMap g x ])
|
|
|
62 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
|
|
|
63
|
|
267
|
64 _==_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } {a b : CObj A B } →
|
|
|
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 ]
|
|
200
|
67
|
|
|
68 infix 4 _==_
|
|
|
69
|
|
|
70 open import Relation.Binary.Core
|
|
267
|
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)
|
|
|
72 isB^A {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B =
|
|
200
|
73 record { isEquivalence = record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B ));
|
|
300
|
74 sym = λ {i j} → sym1 {_} {_} {i} {j} ;
|
|
|
75 trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} }
|
|
200
|
76 ; identityL = IsCategory.identityL ( Category.isCategory B )
|
|
|
77 ; identityR = IsCategory.identityR ( Category.isCategory B )
|
|
|
78 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈1 {a} {b} {c} {f} {g} {h} {i}
|
|
|
79 ; associative = IsCategory.associative ( Category.isCategory B )
|
|
|
80 } where
|
|
267
|
81 sym1 : {a b : CObj A B } {i j : CHom A B a b } → i == j → j == i
|
|
200
|
82 sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin
|
|
|
83 TMap j x
|
|
|
84 ≈⟨ sym eq ⟩
|
|
|
85 TMap i x
|
|
|
86 ∎
|
|
267
|
87 trans1 : {a b : CObj A B } {i j k : CHom A B a b} → i == j → j == k → i == k
|
|
200
|
88 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning B in begin
|
|
|
89 TMap i x
|
|
|
90 ≈⟨ i=j ⟩
|
|
|
91 TMap j x
|
|
|
92 ≈⟨ j=k ⟩
|
|
|
93 TMap k x
|
|
|
94 ∎
|
|
267
|
95 o-resp-≈1 : {a b c : CObj A B } {f g : CHom A B a b} {h i : CHom A B b c } →
|
|
200
|
96 f == g → h == i → h + f == i + g
|
|
|
97 o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning B in begin
|
|
|
98 TMap h x o TMap f x
|
|
|
99 ≈⟨ resp f=g h=i ⟩
|
|
|
100 TMap i x o TMap g x
|
|
|
101 ∎
|
|
|
102
|
|
267
|
103 _^_ : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ' ) (B : Category c₁ c₂ ℓ) →
|
|
|
104 Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))
|
|
|
105 (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))
|
|
|
106 (ℓ' ⊔ c₁)
|
|
|
107 _^_ {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} B A =
|
|
|
108 record { Obj = CObj A B
|
|
|
109 ; Hom = CHom A B
|
|
200
|
110 ; _o_ = _+_
|
|
|
111 ; _≈_ = _==_
|
|
267
|
112 ; Id = Cid A B
|
|
|
113 ; isCategory = isB^A A B
|
|
200
|
114 }
|
|
|
115
|
