|
779
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module CCC where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
|
7 open import Data.Product renaming (_×_ to _*_)
|
|
|
8
|
|
|
9 open Functor
|
|
|
10
|
|
|
11 -- ccc-1 : Hom A a 1 ≅ {*}
|
|
|
12 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
|
|
|
13 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
|
|
|
14
|
|
|
15 record _≅_ {c₁ c₂ ℓ ℓ' : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A} (f : Hom A a b) (S : Set ℓ') : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ ℓ' ) where
|
|
|
16 field
|
|
|
17 ≅→ : {!!}
|
|
|
18 ≅← : {!!}
|
|
|
19 iso→ : {!!}
|
|
|
20 iso← : {!!}
|
|
|
21
|
|
|
22 data One {c : Level} : Set c where
|
|
|
23 OneObj : One -- () in Haskell ( or any one object set )
|
|
|
24
|
|
|
25
|
|
|
26 record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
|
|
|
27 ( _×_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
28 field
|
|
|
29 ccc-1 : {a : Obj A} → Hom A a one ≅ One {ℓ}
|
|
|
30 ccc-2 : {a b c : Obj A} → Hom A c ( a × b ) ≅ ( Hom A c a ) * ( Hom A c b )
|
|
|
31 ccc-3 : {a b c : Obj A} → Hom A a ( c ^ b ) ≅ Hom A ( a × b ) c
|
|
|
32
|
|
|
33
|
|
|
34
|
