# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555684939 -32400
# Node ID 1e7319868d77c53c62c691fa6c4ea6c62ff6577c
# Parent  4e1e2f7199c813050238b1ac97b6b387d6b10f99
Sets is CCC

diff -r 4e1e2f7199c8 -r 1e7319868d77 CCChom.agda
--- a/CCChom.agda	Fri Apr 19 19:20:04 2019 +0900
+++ b/CCChom.agda	Fri Apr 19 23:42:19 2019 +0900
@@ -6,7 +6,7 @@
 open import cat-utility
 open import Data.Product renaming (_×_ to _∧_)
 open import Category.Constructions.Product
-open  import  Relation.Binary.PropositionalEquality
+open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 open Functor
 
@@ -314,5 +314,81 @@
                *-cong  : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
                *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
 
+open import Category.Sets
+
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+data One' {l : Level}  : Set l where
+  OneObj' : One'   -- () in Haskell ( or any one object set )
+
+sets : {l : Level } → CCC (Sets {l})
+sets {l} = record {
+         １  = One'
+       ; ○ = λ _ → λ _ → OneObj'
+       ; _∧_ = _/\_
+       ; <_,_> = <,>
+       ; π = π
+       ; π' = π'
+       ; _<=_ = _<=_
+       ; _* = _*
+       ; ε = ε
+       ; isCCC = isCCC
+  } where
+         １ : Obj Sets 
+         １ = One' 
+         ○ : (a : Obj Sets ) → Hom Sets a １
+         ○ a = λ _ → OneObj'
+         _/\_ : Obj Sets → Obj Sets → Obj Sets
+         _/\_ a b = a ∧ b
+         <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b)
+         <,> f g = λ x → ( f x , g x )
+         π : {a b : Obj Sets } → Hom Sets (a /\ b) a
+         π {a} {b} =  proj₁ 
+         π' : {a b : Obj Sets } → Hom Sets (a /\ b) b
+         π' {a} {b} =  proj₂ 
+         _<=_ : (a b : Obj Sets ) → Obj Sets
+         a <= b  = b → a
+         _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b)
+         f * =  λ x → λ y → f ( x , y )
+         ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a
+         ε {a} {b} =  λ x → ( proj₁ x ) ( proj₂ x )
+         isCCC : CCC.IsCCC Sets １ ○ _/\_ <,> π π' _<=_ _* ε
+         isCCC = record {
+               e2  = e2
+             ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
+             ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
+             ; e3c = e3c
+             ; π-cong = π-cong
+             ; e4a = e4a
+             ; e4b = e4b
+             ; *-cong = *-cong
+           } where
+                e2 : {a : Obj Sets} (f : Hom Sets a １) → Sets [ f ≈ ○ a ]
+                e2 {a} f = extensionality Sets ( λ x → e20 x )
+                  where
+                        e20 : (x : a ) → f x ≡ ○ a x
+                        e20 x with f x
+                        e20 x | OneObj' = refl
+                e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
+                    Sets [ ( Sets [  π  o ( <,> f g)  ] ) ≈ f ]
+                e3a = refl
+                e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
+                    Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
+                e3b = refl
+                e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} →
+                    Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
+                e3c = refl
+                π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
+                    Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
+                π-cong refl refl = refl
+                e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} →
+                    Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
+                e4a = refl
+                e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
+                    Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
+                e4b = refl
+                *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} →
+                    Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
+                *-cong refl = refl