Mercurial > hg > Members > kono > Proof > category
diff CCC.agda @ 783:bded2347efa4
CCC by equation
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 17 Apr 2019 12:03:45 +0900 |
| parents | 340708e8d54f |
| children | f27d966939f8 |
line wrap: on
line diff
--- a/CCC.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/CCC.agda Wed Apr 17 12:03:45 2019 +0900 @@ -4,8 +4,8 @@ open import HomReasoning open import cat-utility -open import Data.Product renaming (_×_ to _∧_) -open import Category.Constructions.Product +-- open import Data.Product renaming (_×_ to _∧_) +-- open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality open Functor @@ -14,14 +14,6 @@ -- 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 -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 ] - data One {c : Level} : Set c where OneObj : One -- () in Haskell ( or any one object set ) @@ -44,14 +36,22 @@ 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₂ ℓ) (one : Obj A) + +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 one ≅ {*} - IsoS A OneCat a one OneObj OneObj + 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) + 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 @@ -61,11 +61,77 @@ one : Obj A _*_ : Obj A → Obj A → Obj A _^_ : Obj A → Obj A → Obj A - isCCC : IsCCC A one _*_ _^_ + _×_ : Obj A → Obj A → Obj A + isCCC : IsCCC A one _×_ _*_ _^_ + +open import HomReasoning + +record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( １ : Obj A ) + ( ○ : (a : Obj A ) → Hom A a １ ) + ( _∧_ : Obj A → Obj A → Obj A ) + ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) ) + ( π : {a b : Obj A } → Hom A (a ∧ b) a ) + ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) + ( _<=_ : (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 ) + : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where + field + -- cartesian + e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ] + e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ] + e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ] + e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ] + π-congl : {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ] → A [ < f , g > ≈ < f' , g > ] + π-congr : {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ] → A [ < f , g > ≈ < f , g' > ] + -- closed + e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] + e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] -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 + e'2 : A [ ○ １ ≈ id1 A １ ] + e'2 = let open ≈-Reasoning A in begin + ○ １ + ≈↑⟨ e2 (id1 A １ ) ⟩ + id1 A １ + ∎ + e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ] + e''2 {a} {b} {f} = let open ≈-Reasoning A in begin + ○ b o f + ≈⟨ e2 (○ b o f) ⟩ + ○ a + ∎ + distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ] + distr {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin + < f , g > o h + ≈↑⟨ e3c ⟩ + < π o < f , g > o h , π' o < f , g > o h > + ≈⟨ π-congl assoc ⟩ + < ( π o < f , g > ) o h , π' o < f , g > o h > + ≈⟨ π-congl (car e3a ) ⟩ + < f o h , π' o < f , g > o h > + ≈⟨ π-congr assoc ⟩ + < f o h , (π' o < f , g > ) o h > + ≈⟨ π-congr (car e3b ) ⟩ + < f o h , g o h > + ∎ + _×_ : { 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 field - e2 : {a : Obj A} { f : Hom A a one } → A [ f ≈ oneT a ] - e3a : {!!} + １ : Obj A + ○ : (a : Obj A ) → Hom A a １ + _∧_ : Obj A → Obj A → Obj A + <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) + π : {a b : Obj A } → Hom A (a ∧ b) a + π' : {a b : Obj A } → Hom A (a ∧ b) b + _<=_ : (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 １ ○ _∧_ <_,_> π π' _<=_ _* ε + + + +