Mercurial > hg > Members > kono > Proof > category
changeset 781:340708e8d54f
fix for 2.5.4.2
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 08 Mar 2019 17:46:59 +0900 |
| parents | b44c1c6ce646 |
| children | db59b8f954aa |
| files | CCC.agda HomReasoning.agda SetsCompleteness.agda discrete.agda freyd2.agda monoid-monad.agda monoidal.agda yoneda.agda |
| diffstat | 8 files changed, 28 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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 : {!!} +
--- 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
--- 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
--- 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
--- 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
--- 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 _∙_
--- 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
--- 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} )