# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1552034819 -32400
# Node ID 340708e8d54f51754d3f13dcf52c04a8113cd9e4
# Parent  b44c1c6ce6461969757672b835507093d11d8e88
fix for 2.5.4.2

diff -r b44c1c6ce646 -r 340708e8d54f CCC.agda
--- a/CCC.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/CCC.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -45,7 +45,7 @@
          ... | OneObj = refl
 
 
-record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
+record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
           ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
        ccc-1 : {a : Obj A}     →  --   Hom A a one ≅ {*}
@@ -56,4 +56,16 @@
                           IsoS A A  a (c ^ b) (a * b) c
         
         
+record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+       one : Obj A
+       _*_ : Obj A → Obj A → Obj A
+       _^_ : Obj A → Obj A → Obj A  
+       isCCC : IsCCC A one _*_ _^_
 
+record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) ( oneT : ( a : Obj A ) → Hom A a one )
+          ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+       e2  : {a : Obj A} { f : Hom A a one } →  A [ f ≈ oneT a ]
+       e3a : {!!}
+
diff -r b44c1c6ce646 -r 340708e8d54f HomReasoning.agda
--- a/HomReasoning.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/HomReasoning.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -6,7 +6,6 @@
 open import Level
 open Functor
 
-
 --        F(f)
 --   F(a) ---→ F(b)
 --    |          |
@@ -82,8 +81,9 @@
   idR1 :  { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } →  A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f  ]
   idR1 A =  IsCategory.identityR (Category.isCategory A)
 
+  open import Relation.Binary.PropositionalEquality using ( _≡_ )
   ≈←≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
-  ≈←≡  refl = refl-hom
+  ≈←≡  _≡_.refl = refl-hom
 
 -- Ho← to prove this?
 --  ≡←≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
@@ -91,7 +91,7 @@
 
   ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
              (f : Hom B x y → Hom A x' y' ) →  a ≡ b  → f a  ≈  f b
-  ≡-cong f refl =  ≈←≡ refl
+  ≡-cong f _≡_.refl =  ≈←≡ _≡_.refl
 
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
diff -r b44c1c6ce646 -r 340708e8d54f SetsCompleteness.agda
--- a/SetsCompleteness.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/SetsCompleteness.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -13,6 +13,8 @@
 
 ≡cong = Relation.Binary.PropositionalEquality.cong
 
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+
 lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
    Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
 lemma1 refl  x  = refl
diff -r b44c1c6ce646 -r 340708e8d54f discrete.agda
--- a/discrete.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/discrete.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -4,6 +4,8 @@
 module discrete where
 
 open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
 
 data  TwoObject {c₁ : Level}  : Set c₁ where
    t0 : TwoObject
diff -r b44c1c6ce646 -r 340708e8d54f freyd2.agda
--- a/freyd2.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/freyd2.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -19,6 +19,8 @@
 --    U ⋍ Hom (a,-)
 --
 
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
 -- A is localy small
 postulate ≡←≈ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
diff -r b44c1c6ce646 -r 340708e8d54f monoid-monad.agda
--- a/monoid-monad.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/monoid-monad.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -15,6 +15,8 @@
 -- open Monoid
 open import Algebra.FunctionProperties using (Op₁; Op₂)
 
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
 
 record ≡-Monoid c : Set (suc c) where
   infixl 7 _∙_
diff -r b44c1c6ce646 -r 340708e8d54f monoidal.agda
--- a/monoidal.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/monoidal.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -274,6 +274,8 @@
 -- Data.Product as a Tensor Product for Monoidal Category
 --
 
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+
 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} )  (Sets {c})
 SetsTensorProduct =   record {
        FObj = λ x  →  proj₁ x  *  proj₂ x
diff -r b44c1c6ce646 -r 340708e8d54f yoneda.agda
--- a/yoneda.agda	Mon Oct 08 16:48:27 2018 +0900
+++ b/yoneda.agda	Fri Mar 08 17:46:59 2019 +0900
@@ -16,6 +16,8 @@
 open import cat-utility
 open import Relation.Binary.Core
 open import Relation.Binary
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
 
 
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )