Mercurial > hg > Members > kono > Proof > category
changeset 1034:40c39d3e6a75
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Mar 2021 15:58:02 +0900 |
| parents | a59c51b541a2 |
| children | b6dbec7e535b |
| files | src/CCC.agda src/CCCGraph.agda src/CCCSets.agda src/SetsCompleteness.agda src/ToposEx.agda src/cat-utility.agda src/free-monoid.agda src/freyd2.agda src/maybe-monad.agda src/monoid-monad.agda src/monoidal.agda src/stdalone-kleisli.agda src/system-f.agda src/yoneda.agda |
| diffstat | 14 files changed, 180 insertions(+), 96 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/CCC.agda Wed Mar 31 15:58:02 2021 +0900 @@ -193,6 +193,10 @@ -- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a ) -- ker h h -- +-- if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer. +-- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) +-- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g + open Equalizer open import equalizer
--- a/src/CCCGraph.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/CCCGraph.agda Wed Mar 31 15:58:02 2021 +0900 @@ -17,8 +17,8 @@ open import Category.Sets -import Axiom.Extensionality.Propositional -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- import Axiom.Extensionality.Propositional +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ open import CCCSets @@ -310,7 +310,7 @@ c-map {g} {c} {atom x} {atom b} f y = {!!} where cmpa1 : ((y₁ : vertex g) → C g y₁ x ) → {!!} cmpa1 = {!!} - c-map {g} {c} {⊤} {atom b} f y with y OneObj b + c-map {g} {c} {⊤} {atom b} f y with y ! b ... | id .b = {!!} ... | next x t = (cat c) [ emap f x o c-map f {!!} ] c-map {g} {c} {a ∧ a₁} {atom b} f y = {!!}
--- a/src/CCCSets.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/CCCSets.agda Wed Mar 31 15:58:02 2021 +0900 @@ -117,6 +117,9 @@ case1 : a → a ∨ b case2 : b → a ∨ b +--------------------------------------------- +-- +-- a binary Topos of Sets -- -- m : b → a determins a subset of a as an image -- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x. @@ -134,7 +137,7 @@ ; char = λ m mono → tchar m mono ; isTopos = record { char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x ) - ; ker-m = imequ + ; ker-m = λ m mono → equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) } } where -- @@ -143,10 +146,10 @@ -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g -- m have to be isomorphic to ker (char m). -- --- i ○ b +-- b→s ○ b -- ker (char m) ----→ b -----------→ 1 -- | ←---- | | --- | j |m | ⊤ char m : a → Ω = {true,false} +-- | b←s |m | ⊤ char m : a → Ω = {true,false} -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char ) -- +-------------→ a -----------→ Ω else false -- h @@ -160,7 +163,17 @@ tchar {a} {b} m mono y with lem (image m y ) ... | case1 t = true ... | case2 f = false - + -- imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ]) + -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) + uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → + tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y + uniq {a} {b} h m mono y with h y | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y + ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 + ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) + ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq }) + ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1 + + -- technical detail of equalizer-image isomorphism (isol) below open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) img-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) (t : image m y') → s ≅ t img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) @@ -227,16 +240,6 @@ ... | true | record {eq = eq1} = refl ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 ... | t = ⊥-elim (t (isImage x)) - imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ]) - imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) - uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → - tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y - uniq {a} {b} h m mono y with h y | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y - ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 - ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) - ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq }) - ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1 - open import graph module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where
--- a/src/SetsCompleteness.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/SetsCompleteness.agda Wed Mar 31 15:58:02 2021 +0900 @@ -9,8 +9,8 @@ open import Function import Relation.Binary.PropositionalEquality -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x ) -import Axiom.Extensionality.Propositional -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- import Axiom.Extensionality.Propositional +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ≡cong = Relation.Binary.PropositionalEquality.cong
--- a/src/ToposEx.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/ToposEx.agda Wed Mar 31 15:58:02 2021 +0900 @@ -178,6 +178,7 @@ N : Obj A N = Nat iNat + -- if h : Hom A (N ∧ a) a is π', A is a constant record prop33 {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field @@ -318,3 +319,38 @@ < (nsuc iNat) o π , g' o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ < (nsuc iNat) o π , g o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎ +-- +-- open Functor +-- open import Category.Sets +-- open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) +-- record SubObjectFuntor : Set ( suc (suc c₁ ) ⊔ suc (suc c₂) ⊔ suc ℓ ) where +-- field +-- Sub : Functor A (Sets {c₂}) +-- smonic : Mono A {!!} +-- +-- open SubObjectFuntor +-- postulate ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y +-- sub→topos : (Ω : Obj A) → (S : SubObjectFuntor) → Representable A ≡←≈ (Sub S) Ω → Topos A c +-- sub→topos Ω S R = record { +-- Ω = Ω +-- ; ⊤ = {!!} +-- ; Ker = {!!} +-- ; char = λ m mono → {!!} +-- ; isTopos = record { +-- char-uniqueness = {!!} +-- ; ker-m = {!!} +-- } } +-- +-- topos→sub : (t : Topos A c ) → SubObjectFuntor +-- topos→sub t = record { +-- Sub = record { +-- FObj = {!!} +-- ; FMap = {!!} +-- ; isFunctor = {!!} +-- } ; smonic = {!!} +-- } +-- +-- topos→rep : (t : Topos A c ) → Representable A ≡←≈ (Sub (topos→sub t)) (Topos.Ω t) +-- topos→rep t = {!!} +-- +--
--- a/src/cat-utility.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/cat-utility.agda Wed Mar 31 15:58:02 2021 +0900 @@ -529,3 +529,43 @@ initialObject : Obj A hasInitialObject : HasInitialObject A initialObject + open import Category.Sets + import Axiom.Extensionality.Propositional + postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ + + Yoneda : { 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 : Obj A) → Functor A (Sets {c₂}) + Yoneda {c₁} {c₂} {ℓ} A ≡←≈ a = record { + FObj = λ b → Hom A a b + ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) + ; isFunctor = record { + identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; + distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; + ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) + } + } where + lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x + lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ idL + lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ + A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ ( sym assoc ) + lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ ( resp refl-hom eq ) + + -- Representable U ≈ Hom(A,-) + + record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + ( ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y ) + ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + field + -- FObj U x : A → Set + -- FMap U f = Set → Set (locally small) + -- λ b → Hom (a,b) : A → Set + -- λ f → Hom (a,-) = λ b → Hom a b + + repr→ : NTrans A (Sets {c₂}) U (Yoneda A ≡←≈ a ) + repr← : NTrans A (Sets {c₂}) (Yoneda A ≡←≈ a) U + reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A ≡←≈ a) x )] + reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] + +
--- a/src/free-monoid.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/free-monoid.agda Wed Mar 31 15:58:02 2021 +0900 @@ -11,17 +11,17 @@ open import Category.Cat open import HomReasoning open import cat-utility -open import Relation.Binary.Core +open import Relation.Binary.Structures open import universal-mapping open import Relation.Binary.PropositionalEquality -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda -open import Algebra.FunctionProperties using (Op₁; Op₂) +open import Algebra.Definitions -- using (Op₁; Op₂) +open import Algebra.Core open import Algebra.Structures open import Data.Product - record ≡-Monoid : Set (suc c) where infixr 9 _∙_ field @@ -112,7 +112,7 @@ -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) -postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c +-- postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id) isMonoids = record { isEquivalence = isEquivalence1 @@ -132,7 +132,7 @@ f == g → h == i → (h + f) == (i + g) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ≡-Reasoning in begin morph ( h + f ) - ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality {Carrier a} lemma11) ⟩ + ≡⟨ ≡-cong ( λ g → ( ( λ (x : Carrier a ) → g x ) )) (extensionality (Sets ) {Carrier a} lemma11) ⟩ morph ( i + g ) ∎ where @@ -184,15 +184,12 @@ Carrier = List a ; _∙_ = _++_ ; ε = [] - ; isMonoid = record { - identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) ; - isSemigroup = record { - assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) - ; isEquivalence = list-isEquivalence - ; ∙-cong = λ x → λ y → list-o-resp-≈ y x - } - } - } + ; isMonoid = record { isSemigroup = record { isMagma = record { + isEquivalence = list-isEquivalence + ; ∙-cong = λ x → λ y → list-o-resp-≈ y x } + ; assoc = λ x → λ y → λ z → sym ( list-assoc {a} {x} {y} {z} ) } + ; identity = ( ( λ x → list-id-l {a} ) , ( λ x → list-id-r {a} ) ) + } } Generator : Obj A → Obj B Generator s = list s @@ -257,7 +254,7 @@ ( λ (x : a ) → b < ( f x ) ∙ (Φ {a} {b} f [] ) > ) ≡⟨⟩ ( λ (x : a ) → b < ( f x ) ∙ ( ε b ) > ) - ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality {a} lemma-ext1) ⟩ + ≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality A {a} lemma-ext1) ⟩ ( λ (x : a ) → f x ) ≡⟨⟩ f @@ -267,7 +264,7 @@ uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → { g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] uniquness {a} {b} {f} {g} eq = - extensionality lemma-ext2 where + extensionality A lemma-ext2 where lemma-ext2 : ( ∀( x : List a ) → (morph ( solution a b f)) x ≡ (morph g) x ) -- (morph ( solution a b f)) [] ≡ (morph g) [] ) lemma-ext2 [] = let open ≡-Reasoning in @@ -288,7 +285,7 @@ ≡⟨ ≡-cong ( λ k → ( b < ( k x ) ∙ ((morph g) ( xs )) > )) ( begin ( λ x → (morph ( solution a b f)) ( x :: [] ) ) - ≡⟨ extensionality {a} lemma-ext3 ⟩ + ≡⟨ extensionality A {a} lemma-ext3 ⟩ ( λ x → (morph g) ( x :: [] ) ) ∎ ) ⟩
--- a/src/freyd2.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/freyd2.agda Wed Mar 31 15:58:02 2021 +0900 @@ -6,7 +6,7 @@ where open import HomReasoning -open import cat-utility +open import cat-utility hiding (Yoneda) open import Relation.Binary.Core open import Function @@ -24,9 +24,13 @@ -- 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 +Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) +Yoneda {c₁} {c₂} {ℓ} A a = cat-utility.Yoneda A (≡←≈ A) a + + import Axiom.Extensionality.Propositional -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ ---- -- @@ -40,47 +44,47 @@ open IsLimit open import Category.Cat -Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) -Yoneda {c₁} {c₂} {ℓ} A a = record { - FObj = λ b → Hom A a b - ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) - ; isFunctor = record { - identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) - } - } where - lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL - lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ - A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin - A [ A [ g o f ] o x ] - ≈↑⟨ assoc ⟩ - A [ g o A [ f o x ] ] - ≈⟨⟩ - ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) - ∎ ) - lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin - A [ f o x ] - ≈⟨ resp refl-hom eq ⟩ - A [ g o x ] - ∎ ) +-- Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) +-- Yoneda {c₁} {c₂} {ℓ} A a = record { +-- FObj = λ b → Hom A a b +-- ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) +-- ; isFunctor = record { +-- identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; +-- distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; +-- ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) +-- } +-- } where +-- lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x +-- lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL +-- lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ +-- A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x +-- lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin +-- A [ A [ g o f ] o x ] +-- ≈↑⟨ assoc ⟩ +-- A [ g o A [ f o x ] ] +-- ≈⟨⟩ +-- ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) +-- ∎ ) +-- lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] +-- lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin +-- A [ f o x ] +-- ≈⟨ resp refl-hom eq ⟩ +-- A [ g o x ] +-- ∎ ) --- Representable U ≈ Hom(A,-) +-- -- Representable U ≈ Hom(A,-) -record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where - field - -- FObj U x : A → Set - -- FMap U f = Set → Set (locally small) - -- λ b → Hom (a,b) : A → Set - -- λ f → Hom (a,-) = λ b → Hom a b +-- record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where +-- field +-- -- FObj U x : A → Set +-- -- FMap U f = Set → Set (locally small) +-- -- λ b → Hom (a,b) : A → Set +-- -- λ f → Hom (a,-) = λ b → Hom a b - repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) - repr← : NTrans A (Sets {c₂}) (Yoneda A a) U - reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] - reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] +-- repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) +-- repr← : NTrans A (Sets {c₂}) (Yoneda A a) U +-- reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] +-- reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] open Representable @@ -104,7 +108,7 @@ YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) (Γ : Functor I A) (limita : Limit I A Γ) → - IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) + IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i @@ -281,7 +285,7 @@ (U : Functor A (Sets {c₂}) ) ( i : Obj ( K A Sets * ↓ U) ) (In : HasInitialObject ( K A Sets * ↓ U) i ) - → Representable A U (obj i) + → Representable A (≡←≈ A) U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
--- a/src/maybe-monad.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/maybe-monad.agda Wed Mar 31 15:58:02 2021 +0900 @@ -8,9 +8,9 @@ open import Relation.Binary.Core open import Category.Cat -import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ([_]) -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ data maybe (A : Set c) : Set c where just : A → maybe A @@ -87,9 +87,12 @@ A [ A [ FMap Maybe f o tmap a ] ≈ A [ tmap b o FMap (Maybe ○ Maybe) f ] ] comm {a} {b} {f} = extensionality A ( λ x → comm1 a b f x ) -MaybeMonad : Monad A Maybe Maybe-η Maybe-μ +MaybeMonad : Monad A MaybeMonad = record { - isMonad = record { + T = Maybe + ; η = Maybe-η + ; μ = Maybe-μ + ; isMonad = record { unity1 = unity1 ; unity2 = unity2 ; assoc = assoc
--- a/src/monoid-monad.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/monoid-monad.agda Wed Mar 31 15:58:02 2021 +0900 @@ -111,11 +111,6 @@ Lemma-MM36 x y z = ( IsMonoid.assoc ( isMonoid M )) x y z import Relation.Binary.PropositionalEquality --- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → Relation.Binary.PropositionalEquality.Extensionality c c --- postulate extensionality : Axiom.Extensionality.Propositional.Extensionality c c - -import Axiom.Extensionality.Propositional -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ -- Multi Arguments Functional Extensionality extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } →
--- a/src/monoidal.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/monoidal.agda Wed Mar 31 15:58:02 2021 +0900 @@ -21,6 +21,14 @@ -- iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] -- Monoidal Category +-- +-- αA□BCD αAB□CD +-- (((a □ b) □ c ) □ d) → ((a □ (b □ c)) □ d) → (a □ ((b □ c ) □ d)) +-- +-- ↓ αA□BCD 1A□BCD ↓ ↓ αAB□CD +-- +-- ((a □ b ) □ (c □ d)) ← (a □ (b □ ( c □ d) )) ← -------+ +-- αABC□D record IsMonoidal {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C ) : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where @@ -267,8 +275,6 @@ open import Category.Sets import Relation.Binary.PropositionalEquality --- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ------ -- Data.Product as a Tensor Product for Monoidal Category
--- a/src/stdalone-kleisli.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/stdalone-kleisli.agda Wed Mar 31 15:58:02 2021 +0900 @@ -115,8 +115,8 @@ ∎ -import Axiom.Extensionality.Propositional -postulate extensionality : { c₂ : Level} ( A : Category {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +-- import Axiom.Extensionality.Propositional +-- postulate extensionality : { c₂ : Level} ( A : Category {c₂} ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ -- -- t a
--- a/src/system-f.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/system-f.agda Wed Mar 31 15:58:02 2021 +0900 @@ -167,7 +167,7 @@ lemma21 : {l : Level} {X : Set l} ( x y : Int X ) → add x Zero ≡ x lemma21 x y = refl -postulate extensionality : {l : Level } → Relation.Binary.PropositionalEquality.Extensionality l l +-- postulate extensionality : {l : Level } → Relation.Binary.PropositionalEquality.Extensionality l l --lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x (S y) ≡ S ( add x y ) --lemma23 x y = extensionality ( λ z → {!!} )
--- a/src/yoneda.agda Tue Mar 30 23:31:10 2021 +0900 +++ b/src/yoneda.agda Wed Mar 31 15:58:02 2021 +0900 @@ -79,10 +79,6 @@ -- A is Locally 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 -import Axiom.Extensionality.Propositional --- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ - ---- -- -- Object mapping in Yoneda Functor