|
779
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module CCC where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
780
|
7 open import Data.Product renaming (_×_ to _∧_)
|
|
|
8 open import Category.Constructions.Product
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
779
|
10
|
|
|
11 open Functor
|
|
|
12
|
|
|
13 -- ccc-1 : Hom A a 1 ≅ {*}
|
|
|
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
|
|
|
15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
|
|
|
16
|
|
780
|
17 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
|
|
|
18 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where
|
|
779
|
19 field
|
|
780
|
20 ≅→ : Hom A a b → Hom B a' b'
|
|
|
21 ≅← : Hom B a' b' → Hom A a b
|
|
|
22 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ]
|
|
|
23 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ]
|
|
779
|
24
|
|
|
25 data One {c : Level} : Set c where
|
|
|
26 OneObj : One -- () in Haskell ( or any one object set )
|
|
|
27
|
|
780
|
28 OneCat : Category Level.zero Level.zero Level.zero
|
|
|
29 OneCat = record {
|
|
|
30 Obj = One ;
|
|
|
31 Hom = λ a b → One ;
|
|
|
32 _o_ = λ{a} {b} {c} x y → OneObj ;
|
|
|
33 _≈_ = λ x y → x ≡ y ;
|
|
|
34 Id = λ{a} → OneObj ;
|
|
|
35 isCategory = record {
|
|
|
36 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
|
|
|
37 identityL = λ{a b f} → lemma {a} {b} {f} ;
|
|
|
38 identityR = λ{a b f} → lemma {a} {b} {f} ;
|
|
|
39 o-resp-≈ = λ{a b c f g h i} _ _ → refl ;
|
|
|
40 associative = λ{a b c d f g h } → refl
|
|
|
41 }
|
|
|
42 } where
|
|
|
43 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f
|
|
|
44 lemma {a} {b} {f} with f
|
|
|
45 ... | OneObj = refl
|
|
|
46
|
|
779
|
47
|
|
|
48 record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
|
|
780
|
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
779
|
50 field
|
|
780
|
51 ccc-1 : {a : Obj A} → -- Hom A a one ≅ {*}
|
|
|
52 IsoS A OneCat a one OneObj OneObj
|
|
|
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
|
|
|
54 IsoS A (A × A) c (a * b) (c , c) (a , b)
|
|
|
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
|
|
|
56 IsoS A A a (c ^ b) (a * b) c
|
|
779
|
57
|
|
|
58
|
|
|
59
|
