|
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
|
|
|
9 module CatExponetial {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') where
|
|
|
10
|
|
|
11 open import HomReasoning
|
|
|
12 open import cat-utility
|
|
|
13
|
|
|
14
|
|
|
15 -- Object is a Functor : A → B
|
|
|
16 -- Hom is a natural transformation
|
|
|
17
|
|
|
18 open Functor
|
|
|
19
|
|
|
20 CObj = Functor A B
|
|
|
21 CHom = λ (f : CObj ) → λ (g : CObj ) → NTrans A B f g
|
|
|
22
|
|
|
23 open NTrans
|
|
|
24 Cid : {a : CObj} → CHom a a
|
|
|
25 Cid {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} →
|
|
|
27 B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈
|
|
|
28 B [ id1 B (FObj a b) o FMap a f ] ]
|
|
|
29 commute {a} {a₁} {b} {f} = let open ≈-Reasoning B in begin
|
|
|
30 FMap a f o id1 B (FObj a a₁)
|
|
|
31 ≈⟨ idR ⟩
|
|
|
32 FMap a f
|
|
|
33 ≈↑⟨ idL ⟩
|
|
|
34 id1 B (FObj a b) o FMap a f
|
|
|
35 ∎
|
|
|
36 isNTrans1 : {a : CObj } → IsNTrans A B a a (\x -> id1 B (FObj a x))
|
|
|
37 isNTrans1 {a} = record { commute = \{a₁ b f} -> commute {a} {a₁} {b} {f} }
|
|
|
38
|
|
|
39 _+_ : {a b c : CObj} → CHom b c → CHom a b → CHom a c
|
|
|
40 _+_{a} {b} {c} f g = record { TMap = λ x → B [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where
|
|
|
41 commute1 : (a b c : CObj ) (f : CHom b c) (g : CHom a b )
|
|
|
42 (a₁ b₁ : Obj A) (h : Hom A a₁ b₁) →
|
|
|
43 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 ] ]
|
|
|
45 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₁ ] ]
|
|
|
47 ≈⟨ assoc ⟩
|
|
|
48 B [ B [ FMap c h o TMap f a₁ ] o TMap g a₁ ]
|
|
|
49 ≈⟨ car (nat f) ⟩
|
|
|
50 B [ B [ TMap f b₁ o FMap b h ] o TMap g a₁ ]
|
|
|
51 ≈↑⟨ assoc ⟩
|
|
|
52 B [ TMap f b₁ o B [ FMap b h o TMap g a₁ ] ]
|
|
|
53 ≈⟨ cdr (nat g) ⟩
|
|
|
54 B [ TMap f b₁ o B [ TMap g b₁ o FMap a h ] ]
|
|
|
55 ≈⟨ assoc ⟩
|
|
|
56 B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ]
|
|
|
57 ∎
|
|
|
58 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 }
|
|
|
60
|
|
|
61 _==_ : {a b : CObj} → CHom a b → CHom a b → Set (ℓ' ⊔ c₁)
|
|
|
62 _==_ {a} {b} f g = ∀{x} → B [ TMap f x ≈ TMap g x ]
|
|
|
63
|
|
|
64 infix 4 _==_
|
|
|
65
|
|
|
66 import Relation.Binary.PropositionalEquality
|
|
|
67 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
|
|
|
68 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₁ c₁
|
|
|
69
|
|
|
70 open import Relation.Binary.Core
|
|
|
71 isB^A : IsCategory CObj CHom _==_ _+_ Cid
|
|
|
72 isB^A =
|
|
|
73 record { isEquivalence = record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B ));
|
|
|
74 sym = \{i j} → sym1 {_} {_} {i} {j} ;
|
|
|
75 trans = \{i j k} → trans1 {_} {_} {i} {j} {k} }
|
|
|
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
|
|
|
81 sym1 : {a b : CObj } {i j : CHom a b } → i == j → j == i
|
|
|
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 ∎
|
|
|
87 trans1 : {a b : CObj } {i j k : CHom a b} → i == j → j == k → i == k
|
|
|
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 ∎
|
|
|
95 o-resp-≈1 : {a b c : CObj} {f g : CHom a b} {h i : CHom b c } →
|
|
|
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
|
|
|
103 B^A : Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) (ℓ' ⊔ c₁)
|
|
|
104 B^A =
|
|
|
105 record { Obj = CObj
|
|
|
106 ; Hom = CHom
|
|
|
107 ; _o_ = _+_
|
|
|
108 ; _≈_ = _==_
|
|
|
109 ; Id = Cid
|
|
|
110 ; isCategory = isB^A
|
|
|
111 }
|
|
|
112
|
