# HG changeset patch # User Shinji KONO # Date 1555480059 -32400 # Node ID f27d966939f8eb767a1bce769c128f1a3f6e216a # Parent bded2347efa46ae86a98d351877f01f704c7118b add CCC hom diff -r bded2347efa4 -r f27d966939f8 CCC.agda --- a/CCC.agda Wed Apr 17 12:03:45 2019 +0900 +++ b/CCC.agda Wed Apr 17 14:47:39 2019 +0900 @@ -4,69 +4,12 @@ open import HomReasoning open import cat-utility --- open import Data.Product renaming (_×_ to _∧_) --- open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality -open Functor - --- ccc-1 : Hom A a 1 ≅ {*} --- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) --- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c - -data One {c : Level} : Set c where - OneObj : One -- () in Haskell ( or any one object set ) - -OneCat : Category Level.zero Level.zero Level.zero -OneCat = record { - Obj = One ; - Hom = λ a b → One ; - _o_ = λ{a} {b} {c} x y → OneObj ; - _≈_ = λ x y → x ≡ y ; - Id = λ{a} → OneObj ; - isCategory = record { - isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; - identityL = λ{a b f} → lemma {a} {b} {f} ; - identityR = λ{a b f} → lemma {a} {b} {f} ; - o-resp-≈ = λ{a b c f g h i} _ _ → refl ; - associative = λ{a b c d f g h } → refl - } - } where - lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f - lemma {a} {b} {f} with f - ... | OneObj = refl - -record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) - : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where - field - ≅→ : Hom A a b → Hom B a' b' - ≅← : Hom B a' b' → Hom A a b - iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] - iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] - - -record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _×_ : {a b c : Obj A ) → Hom A c a → Hom A c b → Hom A (a * b) ) - ( _*_ : 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 １ ≅ {*} - IsoS A OneCat a １ OneObj OneObj - ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) - IsoS A A c (a * b) {!!} {!!} - ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c - 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 - _×_ : Obj A → Obj A → Obj A - isCCC : IsCCC A one _×_ _*_ _^_ open import HomReasoning -record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) +record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A ) ( ○ : (a : Obj A ) → Hom A a １ ) ( _∧_ : Obj A → Obj A → Obj A ) @@ -118,7 +61,7 @@ _×_ : { a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e ) f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] > -record EqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where +record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field １ : Obj A ○ : (a : Obj A ) → Hom A a １ @@ -129,7 +72,7 @@ _<=_ : (a b : Obj A ) → Obj A _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a - isEqCCC : IsEqCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε + isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε diff -r bded2347efa4 -r f27d966939f8 CCChom.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CCChom.agda Wed Apr 17 14:47:39 2019 +0900 @@ -0,0 +1,80 @@ +open import Level +open import Category +module CCChom where + +open import HomReasoning +open import cat-utility +open import Data.Product renaming (_×_ to _∧_) +open import Category.Constructions.Product +open import Relation.Binary.PropositionalEquality + +open Functor + +-- ccc-1 : Hom A a 1 ≅ {*} +-- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) +-- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c + +data One {c : Level} : Set c where + OneObj : One -- () in Haskell ( or any one object set ) + +OneCat : Category Level.zero Level.zero Level.zero +OneCat = record { + Obj = One ; + Hom = λ a b → One ; + _o_ = λ{a} {b} {c} x y → OneObj ; + _≈_ = λ x y → x ≡ y ; + Id = λ{a} → OneObj ; + isCategory = record { + isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; + identityL = λ{a b f} → lemma {a} {b} {f} ; + identityR = λ{a b f} → lemma {a} {b} {f} ; + o-resp-≈ = λ{a b c f g h i} _ _ → refl ; + associative = λ{a b c d f g h } → refl + } + } where + lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f + lemma {a} {b} {f} with f + ... | OneObj = refl + +record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) + : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where + field + ≅→ : Hom A a b → Hom B a' b' + ≅← : Hom B a' b' → Hom A a b + iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] + iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] + + +record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : 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 １ ≅ {*} + IsoS A OneCat a １ OneObj OneObj + ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) + IsoS A (A × A) c (a * b) (c , c ) (a , b ) + ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c + IsoS A A a (c ^ b) (a * b) c + + +record CCChom {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 + isCCChom : IsCCChom A one _*_ _^_ + +open import HomReasoning + +open import CCC + +CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A +CCC→hom A c = record { + one = CCC.１ c + ; _*_ = CCC._∧_ c + ; _^_ = CCC._<=_ c + ; isCCChom = record { + ccc-1 = {!!} + ; ccc-2 = {!!} + ; ccc-3 = {!!} + } + }