Mercurial > hg > Members > kono > Proof > category
changeset 1115:5620d4a85069
safe rewriting nearly finished
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jul 2024 11:44:58 +0900 |
| parents | ce23d2b47c5e |
| children | 5b80413de9b1 |
| files | src/CCCGraph.agda src/CCCSets.agda src/CCChom.agda src/Category/Cone.agda src/Category/Constructions/Coslice.agda src/Category/Group.agda src/Category/Isomorphism.agda src/Category/Monoid.agda src/Category/Object/Terminal.agda src/Category/One.agda src/Category/Poset.agda src/Category/Ring.agda src/Definitions.agda src/Polynominal.agda src/SetsCompleteness.agda src/SetsCompleteness1.agda src/ToposEx.agda src/applicative.agda src/freyd.agda src/freyd1.agda src/freyd2.agda src/group.agda src/limit-to.agda src/list-monoid-cat.agda src/maybe-monad.agda src/monad→monoidal.agda src/monoid-monad.agda src/monoidal.agda src/stdalone-kleisli.agda src/yoneda.agda |
| diffstat | 30 files changed, 672 insertions(+), 621 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCCGraph.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/CCCGraph.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,9 +1,10 @@ +{-# OPTIONS --cubical-compatible --safe #-} module CCCgraph where open import Level open import Category open import HomReasoning -open import cat-utility +open import Definitions open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality hiding ( [_] )
--- a/src/CCCSets.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/CCCSets.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,13 +1,14 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --with-K --cubical-compatible --allow-unsolved-metas #-} +--- {-# OPTIONS --allow-unsolved-metas #-} module CCCSets where open import Level open import Category open import HomReasoning -open import cat-utility +open import Definitions open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product -open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import CCC open Functor @@ -71,32 +72,32 @@ ; *-cong = *-cong } where e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] - e2 {a} {f} = extensionality Sets ( λ x → e20 x ) + e2 {a} {f} = ? -- extensionality Sets ( λ x → e20 x ) where e20 : (x : a ) → f x ≡ ○ a x e20 x with f x e20 x | ! = refl e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] - e3a = refl + e3a _ = refl e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] - e3b = refl + e3b _ = refl e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] - e3c = refl + e3c _ = refl π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] - π-cong refl refl = refl + π-cong = ? e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] - e4a = refl + e4a _ = refl e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] - e4b = refl + e4b _ = refl *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] - *-cong refl = refl + *-cong = ? open import Relation.Nullary open import Data.Empty @@ -136,7 +137,7 @@ ; Ker = tker ; char = λ m mono → tchar m mono ; isTopos = record { - char-uniqueness = λ {a} {b} {h} → extensionality Sets ( λ x → uniq h x ) + char-uniqueness = λ {a} {b} {h} → ? -- extensionality Sets ( λ x → uniq h x ) ; char-iso = iso-m ; ker-m = ker-iso } @@ -159,7 +160,7 @@ tker {a} h = record { equalizer-c = sequ a Bool h (λ _ → true ) ; equalizer = λ e → equ e - ; isEqualizer = SetsIsEqualizer _ _ _ _ } + ; isEqualizer = SetsIsEqualizer _ _ _ _ ? } tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} tchar {a} {b} m mono y with lem (image m y ) ... | case1 t = true @@ -168,18 +169,19 @@ -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) uniq : {a : Obj (Sets {c})} (h : Hom Sets a Bool) (y : a) → tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y - uniq {a} h 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 + uniq = ? +-- uniq {a} h 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₁) - with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) ) - ... | refl = HE.refl + img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) = ? + -- with cong (λ k → k ! ) ? -- ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ? ) -- ( extensionality Sets ( λ _ → eq )) ) + -- ... | refl = HE.refl image-uniq : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m ) (y : a) → (i0 i1 : image m y ) → i0 ≡ i1 image-uniq {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1) tchar¬Img : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) (y : a) → tchar m mono y ≡ false → ¬ image m y @@ -202,7 +204,7 @@ s2i {a} {b} m mono (elem y eq) with lem (image m y) ... | case1 im = im ker-iso : {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 ]) - ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m isol (extensionality Sets ( λ x → iso4 x)) where + ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m isol ? where -- (extensionality Sets ( λ x → iso4 x)) where b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) b→s x = b2s m mono x b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b @@ -227,8 +229,8 @@ iso2 (elem y eq) = begin b→s ( b←s (elem y eq)) ≡⟨⟩ b2s m mono ( i2b m (s2i m mono (elem y eq))) ≡⟨⟩ - b2s m mono x ≡⟨ elm-cong _ _ (iso21 x ) ⟩ - elem (m x) eq1 ≡⟨ elm-cong _ _ mx=y ⟩ + b2s m mono x ≡⟨ equ-inject ? _ _ (iso21 x ) ⟩ + elem (m x) eq1 ≡⟨ equ-inject ? _ _ mx=y ⟩ elem y eq ∎ where open ≡-Reasoning x : b @@ -246,12 +248,13 @@ ... | t = ⊥-elim (t (isImage x)) isol : Iso Sets b (Equalizer.equalizer-c (tker (tchar m mono))) isol = record { ≅→ = b→s ; ≅← = b←s ; - iso→ = extensionality Sets ( λ x → iso1 x ) - ; iso← = extensionality Sets ( λ x → iso2 x) } + iso→ = ? -- extensionality Sets ( λ x → iso1 x ) + ; iso← = ? } -- extensionality Sets ( λ x → iso2 x) } iso-m : {a a' b : Obj Sets} (p : Hom Sets a b) (q : Hom Sets a' b) (mp : Mono Sets p) (mq : Mono Sets q) → (i : Iso Sets a a' ) → Sets [ p ≈ Sets [ q o Iso.≅→ i ] ] → Sets [ tchar p mp ≈ tchar q mq ] - iso-m {a} {a'} {b} p q mp mq i ei = extensionality Sets (λ y → iso-m1 y ) where + iso-m {a} {a'} {b} p q mp mq i ei = ? -- extensionality Sets (λ y → iso-m1 y ) where + where -- -- Iso.≅← i x ○ a mq : q ( f x ) ≡ q ( g x ) → f x ≡ g x -- a'------------→ a -----------→ 1 @@ -286,21 +289,21 @@ ⊤ = λ _ → true ○ = λ _ → λ _ → ! _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set (suc c ) - _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p o h ≈ ⊤ o ○ c ] - → A [ Poly.f q ∙ h ≈ ⊤ o ○ c ] + _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ A [ Poly.f p o h ] ≈ A [ ⊤ o ○ c ] ] + → A [ Poly.f q ∙ h ≈ A [ ⊤ o ○ c ] ] tl01 : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] - tl01 {a} {b} p q p<q q<p = extensionality Sets t1011 where + tl01 {a} {b} p q p<q q<p = ? where -- extensionality Sets t1011 where open ≡-Reasoning t1011 : (s : b ) → Poly.f p s ≡ Poly.f q s t1011 x with Poly.f p x | inspect ( Poly.f p) x ... | true | record { eq = eq1 } = sym tt1 where tt1 : Poly.f q _ ≡ true - tt1 = cong (λ k → k !) (p<q _ ( extensionality Sets (λ x → eq1) )) + tt1 = cong (λ k → k !) (p<q _ ? ) -- ( extensionality Sets (λ x → eq1) )) ... | false | record { eq = eq1 } with Poly.f q x | inspect (Poly.f q) x ... | true | record { eq = eq2 } = ⊥-elim ( ¬x≡t∧x≡f record { fst = eq1 ; snd = tt1 } ) where tt1 : Poly.f p _ ≡ true - tt1 = cong (λ k → k !) (q<p _ ( extensionality Sets (λ x → eq2) )) + tt1 = cong (λ k → k !) (q<p _ ? ) -- ( extensionality Sets (λ x → eq2) )) ... | false | eq2 = refl @@ -428,8 +431,8 @@ ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) adistr eq x = cong ( λ k → amap x k ) eq isf : IsFunctor PL Sets fobj fmap - IsFunctor.identity isf = extensionality Sets ( λ x → refl ) + IsFunctor.identity isf = ? -- extensionality Sets ( λ x → refl ) IsFunctor.≈-cong isf refl = refl - IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) + IsFunctor.distr isf {a} {b} {c} {g} {f} = ? -- extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
--- a/src/CCChom.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/CCChom.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,9 +1,10 @@ +{-# OPTIONS --cubical-compatible --safe #-} open import Level open import Category module CCChom where open import HomReasoning -open import cat-utility +open import Definitions open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality hiding ( [_] )
--- a/src/Category/Cone.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Cone.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --cubical-compatible --irrelevant-projections #-} +{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --cubical-compatible --irrelevant-projections #-} import Category @@ -24,7 +25,7 @@ field apex : Obj proj : ∀ i → Hom apex (FObj i) - .isCone : ∀{i j : index D} {α : edge D i j } → proj j ≈ FMap α o proj i + isCone : ∀{i j : index D} {α : edge D i j } → proj j ≈ FMap α o proj i record _-Cone⟶_ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} (C₁ : Cone D) (C₂ : Cone D) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where @@ -32,7 +33,7 @@ open Cone field morphism : Hom (apex C₁) (apex C₂) - .isConeMorphism : ∀ {j} → proj C₁ j ≈ proj C₂ j o morphism + isConeMorphism : ∀ {j} → proj C₁ j ≈ proj C₂ j o morphism open Cone open _-Cone⟶_ @@ -41,7 +42,7 @@ ConeId {C₁ = C₁} = record { morphism = Id { apex C₁ } ; isConeMorphism = proof } where - .proof : ∀ {j} → proj C₁ j ≈ proj C₁ j o Id + proof : ∀ {j} → proj C₁ j ≈ proj C₁ j o Id proof = ≈-sym identityR where open Category.IsCategory isCategory open IsEquivalence isEquivalence renaming (sym to ≈-sym) @@ -54,7 +55,7 @@ record { morphism = morph ; isConeMorphism = proof } where morph = morphism C₂toC₃ o morphism C₁toC₂ - .proof : {j : index D} → proj C₁ j ≈ proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) + proof : {j : index D} → proj C₁ j ≈ proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) proof {j} = begin proj C₁ j ≈⟨ isConeMorphism C₁toC₂ ⟩ proj C₂ j o morphism C₁toC₂ ≈⟨ car (isConeMorphism C₂toC₃) ⟩
--- a/src/Category/Constructions/Coslice.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Constructions/Coslice.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,11 +1,13 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --cubical-compatible --safe --universe-polymorphism #-} module Category.Constructions.Coslice where open import Category open import Level open import Relation.Binary open import Relation.Binary.Core -import Relation.Binary.EqReasoning as EqR +-- import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR record CosliceObj {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) (O : Obj C) : Set (c₁ ⊔ c₂) where constructor ⟦_⟧
--- a/src/Category/Group.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Group.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,11 +1,11 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} module Category.Group where open import Category open import Algebra open import Algebra.Structures open import Algebra.Morphism -import Algebra.Props.Group as GroupP -import Relation.Binary.EqReasoning as EqR +import Algebra.Properties.Group as GroupP +import Relation.Binary.Reasoning.Setoid as EqR open import Relation.Binary.Core open import Relation.Binary open import Level @@ -25,7 +25,7 @@ ∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_ ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε - ε-homo = left-identity-unique ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin + ε-homo = identityʳ-unique ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo F.ε F.ε) ⟩ ⟦ F._∙_ F.ε F.ε ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsMonoid.identity (Monoid.isMonoid F.monoid)) F.ε) ⟩ ⟦ F.ε ⟧ ∎) @@ -33,7 +33,7 @@ open GroupP To open EqR T.setoid ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹ - ⁻¹-homo x = left-inverse-unique ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ (begin + ⁻¹-homo x = inverseˡ-unique ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ (begin T._∙_ ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (F._⁻¹ x) x) ⟩ ⟦ F._∙_ (F._⁻¹ x) x ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsGroup.inverse F.isGroup) x) ⟩ ⟦ F.ε ⟧ ≈⟨ ε-homo ⟩
--- a/src/Category/Isomorphism.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Isomorphism.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,10 +1,11 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} import Category module Category.Isomorphism {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where open Category.Category C open import Level -import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR + open import Relation.Binary open import Relation.Binary.Core
--- a/src/Category/Monoid.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Monoid.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} module Category.Monoid where open import Category open import Relation.Binary @@ -8,16 +8,16 @@ open import Level open import Data.Product -data MonoidObj : Set1 where +data MonoidObj {c : Level} : Set c where * : MonoidObj -data MonoidMor {c ℓ : Level} {M : Monoid c ℓ} : MonoidObj → MonoidObj → Set c where +data MonoidMor {c ℓ : Level} {M : Monoid c ℓ} : MonoidObj {c} → MonoidObj {c} → Set (suc c) where Mor : Monoid.Carrier M → MonoidMor * * MonoidId : {c ℓ : Level} {M : Monoid c ℓ} {A : MonoidObj} → MonoidMor {c} {ℓ} {M} A A MonoidId {_} {_} {M} {*} = Mor (Monoid.ε M) -comp : ∀{c ℓ} {M : Monoid c ℓ} {A B C : MonoidObj} +comp : ∀{c ℓ} {M : Monoid c ℓ} {A B C : MonoidObj {c}} → MonoidMor {c} {ℓ} {M} B C → MonoidMor {c} {ℓ} {M} A B → MonoidMor {c} {ℓ} {M} A C @@ -56,8 +56,8 @@ ; associative = assoc } where - isEquivalence : {A B : MonoidObj} - → IsEquivalence {c} {suc (c ⊔ ℓ)} {MonoidMor A B} (_~_ {c} {ℓ} {M} {A} {B}) + isEquivalence : {A B : MonoidObj {c}} + → IsEquivalence {suc c} {suc (c ⊔ ℓ)} {MonoidMor A B} (_~_ {c} {ℓ} {M} {A} {B}) isEquivalence {*} {*} = record { refl = reflexive; sym = symmetric; trans = transitive } o-resp-≃ : {f g h i : MonoidMor {c} {ℓ} {M} * *} → f ≃ g → h ≃ i → comp h f ≃ comp i g o-resp-≃ {Mor f} {Mor g} {Mor h} {Mor i} (Eq eq₁) (Eq eq₂) = @@ -83,9 +83,9 @@ -MONOID : ∀{c ℓ} → (M : Monoid c ℓ) → Category (suc zero) c (suc (ℓ ⊔ c)) -MONOID M = record { Obj = MonoidObj - ; Hom = MonoidMor {_} {_} {M} +MONOID : ∀{c ℓ} → (M : Monoid c ℓ) → Category (c) (suc c) (suc c ⊔ suc ℓ) +MONOID {c} {ℓ} M = record { Obj = MonoidObj {c} + ; Hom = MonoidMor {c} {ℓ} {M} ; _o_ = comp ; _≈_ = _~_ ; Id = MonoidId
--- a/src/Category/Object/Terminal.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Object/Terminal.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,11 +1,13 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} + import Category module Category.Object.Terminal {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where open Category.Category C open import Category.Isomorphism C open import Level -import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR + open import Relation.Binary open import Relation.Binary.Core
--- a/src/Category/One.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/One.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module Category.One where open import Category open import Level
--- a/src/Category/Poset.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Poset.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} module Category.Poset where open import Category open import Relation.Binary
--- a/src/Category/Ring.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Category/Ring.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,10 +1,10 @@ -{-# OPTIONS --universe-polymorphism #-} +{-# OPTIONS --cubical-compatible --safe #-} module Category.Ring where open import Category open import Algebra open import Algebra.Structures -open import Algebra.Morphism -import Relation.Binary.EqReasoning as EqR +open import Algebra.Morphism +import Relation.Binary.Reasoning.Setoid as EqR open import Relation.Binary.Core open import Relation.Binary open import Level @@ -13,17 +13,33 @@ RingObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ)) RingObj {c} {ℓ} = Ring c ℓ + +-- open import Algebra.Morphism.Definitions + +record _-Ring⟶_ {c ℓ c' ℓ' : Level } (From : RingObj {c} {ℓ}) (To : RingObj {c'} {ℓ'}) : Set ((c ⊔ ℓ ⊔ c' ⊔ ℓ')) where + module F = Ring From + module T = Ring To + open Definitions (F.Carrier) (T.Carrier) T._≈_ + field + ⟦_⟧ : Ring.Carrier From → Ring.Carrier To + ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_ + +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_ + *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_ + 1-homo : Homomorphic₀ ⟦_⟧ F.1# T.1# + +infixr 5 _-Ring⟶_ + RingHom : ∀{c ℓ} → Set (suc (c ⊔ ℓ)) RingHom {c} {ℓ} = {R₁ R₂ : Ring c ℓ} → R₁ -Ring⟶ R₂ RingId : ∀{c ℓ} {R : Ring c ℓ} → R -Ring⟶ R RingId {R = R} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo - ; *-homo = *-homo ; 1-homo = 1-homo - } + ; *-homo = *-homo ; 1-homo = 1-homo + } where open Algebra.Ring R open Definitions Carrier Carrier _≈_ - ⟦_⟧ : Morphism + ⟦_⟧ : Carrier → Carrier ⟦_⟧ = λ x → x ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_ ⟦⟧-cong = λ x → x
--- a/src/Definitions.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Definitions.agda Wed Jul 03 11:44:58 2024 +0900 @@ -255,7 +255,7 @@ ; Id = λ {a} → id1 A (SObj.s a) ; isCategory = record { isEquivalence = IsCategory.isEquivalence (Category.isCategory A ) - ; identityL = idL + ; identityL = idL ; identityR = idR ; o-resp-≈ = resp ; associative = assoc @@ -601,11 +601,11 @@ } where open ≈-Reasoning (Category.op A) - -- - -- better than ≡←≈ + -- + -- better than ≡←≈ -- Cong≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Set (c₁ ⊔ c₂ ⊔ ℓ) - Cong≈ A a = {c b : Obj A} (f : Hom A a c → Hom A a b ) + Cong≈ A a = {c b : Obj A} (f : Hom A a c → Hom A a b ) {x y : Hom A a c} → A [ x ≈ y ] → A [ f x ≈ f y ] where open ≈-Reasoning A @@ -623,15 +623,15 @@ } where open ≈-Reasoning A - Yoneda≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + Yoneda≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → (≈-cong : Cong≈ (Category.op A) a ) → Functor (Category.op A) (Sets≈ (Category.op A) a ≈-cong) Yoneda≈ {c₁} {c₂} {ℓ} A a ≈-cong = record { - FObj = λ b → b + FObj = λ b → b ; FMap = λ {x} {y} (f : Hom A y x ) ( g : Hom A x a ) → A [ g o f ] ; isFunctor = record { identity = λ {b} x → idR - ; distr = λ {a} {b} {c} {f} {g} x → assoc - ; ≈-cong = λ eq x → resp eq refl-hom + ; distr = λ {a} {b} {c} {f} {g} x → assoc + ; ≈-cong = λ eq x → resp eq refl-hom } } where open ≈-Reasoning A @@ -656,15 +656,27 @@ record Representable≈ { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( ≡←≈ : {a b : Obj A } { x y : Hom A b a } → (x≈y : (Category.op A) [ x ≈ y ]) → x ≡ y ) - (≈-cong : (a : Obj A) → Cong≈ (Category.op A) a ) - (a : Obj A) + (≈-cong : (a : Obj A) → Cong≈ (Category.op A) a ) + (a : Obj A) ( U : Functor (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) ) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where field repr→ : NTrans (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) U (Yoneda≈ A a (≈-cong a)) repr← : NTrans (Category.op A) (Sets≈ (Category.op A) a (≈-cong a)) (Yoneda≈ A a (≈-cong a)) U - reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] + reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets≈ (Category.op A) a (≈-cong a)) (FObj (Yoneda≈ A a (≈-cong a)) x )] - reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] + reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets≈ (Category.op A) a (≈-cong a)) (FObj U x)] + -- they say it is not possible to prove FreeTheorem in Agda nor Coq + -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities + -- so we postulate this + FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } + → Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) + FreeTheorem C D {a} {b} {c } = + (F : Functor C D ) + → (fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) + → {h f : Hom C a b } → {g k : Hom C b c } + → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ] + +
--- a/src/Polynominal.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/Polynominal.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,4 +1,5 @@ --- {-# OPTIONS --cubical-compatible #-} +{-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible --safe #-} open import Category @@ -36,11 +37,11 @@ -- open Functor - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ; resp ) renaming ( sym to ≡sym ) - data _H≈_ {a b c d : Obj A } ( x : Hom A a b ) (y : Hom A c d ) : Set ( c₁ ⊔ c₂ ⊔ ℓ) where - feq : a ≡ c → b ≡ d → (z : Hom A a b) → z ≅ y → A [ x ≈ z ] → x H≈ y + -- data _H≈_ {a b c d : Obj A } ( x : Hom A a b ) (y : Hom A c d ) : Set ( c₁ ⊔ c₂ ⊔ ℓ) where + -- feq : a ≡ c → b ≡ d → (z : Hom A a b) → z ≅ y → A [ x ≈ z ] → x H≈ y data φ {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁ ⊔ c₂ ⊔ ℓ) where i : {b c : Obj A} (k : Hom A b c ) → φ x k @@ -154,8 +155,8 @@ -- an assuption needed in k x phi ≈ k x phi' -- k x (i x) ≈ k x ii - postulate - xf : {a b c : Obj A } → ( x : Hom A １ a ) → {f : Hom A b c } → ( fp : φ {a} x f ) → A [ k x (i f) ≈ k x fp ] + xf : {a b c : Obj A } → ( x : Hom A １ a ) → {f : Hom A b c } → ( fp : φ {a} x f ) → A [ k x (i f) ≈ k x fp ] + xf = ? -- ( x ∙ π' ) ≈ π -- -- this is justified equality f ≈ g in A[x] is used in f ∙ < x , id1 A _> ≈ f ∙ < x , id1 A _>
--- a/src/SetsCompleteness.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/SetsCompleteness.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,8 +1,8 @@ -{-# OPTIONS #-} +{-# OPTIONS --cubical-compatible --safe #-} open import Category -- https://github.com/konn/category-agda open import Level -open import Category.Sets renaming ( _o_ to _*_ ) +open import Category.Sets module SetsCompleteness where @@ -10,20 +10,12 @@ open import Relation.Binary.Core 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₂ - --- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - -≡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 eq x = ? +lemma1 eq x = eq x record Σ {a} (A : Set a) (B : Set a) : Set a where constructor _,_ @@ -41,16 +33,16 @@ ; π2 = λ ab → (proj₂ ab) ; isProduct = record { _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) - ; π1fxg=f = ? - ; π2fxg=g = ? - ; uniqueness = ? + ; π1fxg=f = λ {c} {f} {g} x → refl + ; π2fxg=g = λ {c} {f} {g} x → refl + ; uniqueness = λ {c} {h} x → refl ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g } } where prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b } → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ] - prod-cong a b {c} {f} {f1} {g} {g1} eq eq1 = ? + prod-cong a b {c} {f} {f1} {g} {g1} eq eq1 x = cong₂ (λ j k → j , k) (eq x) (eq1 x) record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where @@ -61,9 +53,12 @@ open Small +open import Axiom.Extensionality.Propositional + SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) + → Extensionality c₂ c₂ → IProduct I ( Sets { c₂} ) ai -SetsIProduct I fi = record { +SetsIProduct {c₂} I fi ext = record { iprod = iproduct I fi ; pi = λ i prod → pi1 prod i ; isIProduct = record { @@ -76,20 +71,20 @@ iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi) iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x } pif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets q (fi i)} → {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ] - pif=q {q} {qi} {i} = ? + pif=q {q} {qi} {i} x = refl ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ] - ip-uniqueness = ? + ip-uniqueness {q} {h} x = refl ipcx : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x ipcx {q} {qi} {qi'} qi=qi x = begin record { pi1 = λ i → (qi i) x } - ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ? ⟩ -- ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ + ≡⟨ cong (λ k → record { pi1 = k} ) (ext (λ i → qi=qi i x) ) ⟩ record { pi1 = λ i → (qi' i) x } ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning ip-cong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1 qi' ] - ip-cong {q} {qi} {qi'} qi=qi = ? -- extensionality Sets ( ipcx qi=qi ) + ip-cong {q} {qi} {qi'} qi=qi = ipcx qi=qi data coproduct {c} (a b : Set c) : Set c where k1 : ( i : a ) → coproduct a b @@ -102,10 +97,10 @@ ; κ2 = λ i → k2 i ; isProduct = record { _+_ = sum - ; κ1f+g=f = ? -- extensionality Sets (λ x → refl ) - ; κ2f+g=g = ? -- extensionality Sets (λ x → refl ) - ; uniqueness = λ {c} {h} → ? -- extensionality Sets (λ x → uniq {c} {h} x ) - ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → ? -- extensionality Sets (pccong feq geq) + ; κ1f+g=f = λ {c} {f} {g} x → fk1 {c} {f} {g} x + ; κ2f+g=g = λ {c} {f} {g} x → fk2 {c} {f} {g} x + ; uniqueness = λ {c} {h} x → uniq {c} {h} x + ; +-cong = pccong } } where sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c @@ -114,9 +109,13 @@ uniq : {c : Obj Sets} {h : Hom Sets (coproduct a b) c} → (x : coproduct a b ) → sum (Sets [ h o (λ i → k1 i) ]) (Sets [ h o (λ i → k2 i) ]) x ≡ h x uniq {c} {h} (k1 i) = refl uniq {c} {h} (k2 i) = refl - pccong : {c : Obj Sets} {f f' : Hom Sets a c} {g g' : Hom Sets b c} → f ≡ f' → g ≡ g' → (x : coproduct a b ) → sum f g x ≡ sum f' g' x - pccong refl refl (k1 i) = refl - pccong refl refl (k2 i) = refl + pccong : {c : Obj Sets} {f f' : Hom Sets a c} {g g' : Hom Sets b c} → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ sum f g ≈ sum f' g' ] + pccong {c} {f} {f'} {g} {g'} eq eq1 (k1 i) = eq i + pccong {c} {f} {f'} {g} {g'} eq eq1 (k2 i) = eq1 i + fk1 : {c : Obj Sets} {f : Hom Sets a c} {g : Hom Sets b c} → Sets [ Sets [ sum f g o (λ i → k1 i) ] ≈ f ] + fk1 {c} {f} {g} x = refl + fk2 : {c : Obj Sets} {f : Hom Sets a c} {g : Hom Sets b c} → Sets [ Sets [ sum f g o (λ i → k2 i) ] ≈ g ] + fk2 {c} {f} {g} x = refl data icoproduct {a} (I : Set a) (ki : I → Set a) : Set a where @@ -137,15 +136,15 @@ isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q isum {q} fi (ki1 i x) = fi i x kif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets (fi i) q} {i : I} → Sets [ Sets [ isum qi o (λ x → ki1 i x) ] ≈ qi i ] - kif=q {q} {qi} {i} = ? -- extensionality Sets (λ x → refl ) + kif=q {q} {qi} {i} x = refl uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ] - uniq {q} {h} = ? where -- extensionality Sets u1 where + uniq {q} {h} = u1 where u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x u1 (ki1 i x) = refl iccong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets (fi i) q} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ isum qi ≈ isum qi' ] - iccong {q} {qi} {qi'} ieq = ? where -- extensionality Sets u2 where + iccong {q} {qi} {qi'} ieq = u2 where u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x - u2 (ki1 i x) = cong (λ k → k x ) ? -- (ieq i) + u2 (ki1 i x) = ieq i x -- -- e f @@ -168,44 +167,44 @@ (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x fe=ge0 (elem x eq ) = eq -irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' -irr refl refl = refl -elm-cong : { c₂ : Level} {a b : Set c₂} {f g : Hom (Sets {c₂}) a b} (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y -elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) +-- we need -with-K to prove this +--- ≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' + +equ-inject : { c₂ : Level} {a b : Set c₂} + (≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq') + {f g : Hom (Sets {c₂}) a b} (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y +equ-inject ≡-irr ( elem x eq ) (elem .x eq' ) refl = cong (λ k → elem x k ) (≡-irr eq eq' ) open sequ -- equalizer-c = sequ a b f g -- ; equalizer = λ e → equ e -SetsIsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g -SetsIsEqualizer {c₂} a b f g = record { +open import Relation.Binary.PropositionalEquality + +SetsIsEqualizer : { c₂ : Level} + (≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq') + → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g +SetsIsEqualizer {c₂} ≡-irr a b f g = record { fe=ge = fe=ge ; k = k ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq} ; uniqueness = uniqueness } where fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] - fe=ge = ? -- extensionality Sets (fe=ge0 ) + fe=ge (elem x eq) = eq k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g) - k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) ? ) + k {d} h eq x = elem (h x) (eq x) ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e ) o k h eq ] ≈ h ] - ek=h {d} {h} {eq} = ? + ek=h {d} {h} {eq} x = refl injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ injection f = ∀ x y → f x ≡ f y → x ≡ y - lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → - Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) - lemma5 eq x = ? -- somehow this is not equal to lemma1 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] - uniqueness {d} {h} {fh=gh} {k'} ek'=h = ? -- extensionality Sets ( λ ( x : d ) → begin - -- k h fh=gh x - -- ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ - -- k' x - -- ∎ ) where - -- open import Relation.Binary.PropositionalEquality - -- open ≡-Reasoning - + uniqueness {d} {h} {fh=gh} {k'} ek'=h x = equ-inject ≡-irr _ _ ( begin + equ ( k h fh=gh x) ≡⟨⟩ + h x ≡⟨ sym ( ek'=h x) ⟩ + equ (k' x) ∎ ) where open ≡-Reasoning -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c -- record cequ {c : Level} (A B : Set c) : Set (suc c) where @@ -219,9 +218,9 @@ -- open import HomReasoning --- etsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) +-- SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) -- → IsCoEqualizer Sets (λ x → {!!} ) f g --- etsIsCoEqualizer {c₂} a b f g = record { +-- SetsIsCoEqualizer {c₂} a b f g = record { -- ef=eg = extensionality Sets (λ x → {!!} ) -- ; k = {!!} -- ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} @@ -260,145 +259,3 @@ -- open ≡-Reasoning -open Functor - ----- --- C is locally small i.e. Hom C i j is a set c₁ --- --- record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) --- : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where --- field --- hom→ : {i j : Obj C } → Hom C i j → I --- hom← : {i j : Obj C } → ( f : I ) → Hom C i j --- hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] --- hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f --- ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g - -ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - (i : Obj C ) → Set c₁ -ΓObj s Γ i = FObj Γ i - -ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - {i j : Obj C } → ( f : I ) → ΓObj s Γ i → ΓObj s Γ j -ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) - -record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) - ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where - field - snmap : ( i : OC ) → sobj i - sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j - -open snat - -open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' ) - using (_≅_;refl; ≡-to-≅) --- why we cannot use Extensionality' ? -postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → - {a : Level } {A : Set a} {B B' : A → Set a} - {f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y )) - -snat-cong : {c : Level} - {I OC : Set c} - {sobj : OC → Set c} - {smap : {i j : OC} → (f : I) → sobj i → sobj j} - → (s t : snat sobj smap) - → (snmap-≡ : snmap s ≡ snmap t) - → (sncommute-≅ : sncommute s ≅ sncommute t) - → s ≡ t -snat-cong _ _ refl refl = refl - -open import HomReasoning -open NTrans - -Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → NTrans C Sets (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ -Cone C I s Γ = record { - TMap = λ i → λ sn → snmap sn i - ; isNTrans = record { commute = comm1 } - } where - comm1 : {a b : Obj C} {f : Hom C a b} → - Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ - Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] - comm1 {a} {b} {f} = ? --- comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin --- FMap Γ f (snmap sn a ) --- ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩ --- FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) --- ≡⟨⟩ --- ΓMap s Γ (hom→ s f) (snmap sn a ) --- ≡⟨ sncommute sn a b (hom→ s f) ⟩ --- snmap sn b --- ∎ ) where --- open import Relation.Binary.PropositionalEquality --- open ≡-Reasoning --- - -SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → Limit C Sets Γ -SetsLimit {c₁} I C s Γ = record { - a0 = snat (ΓObj s Γ) (ΓMap s Γ) - ; t0 = Cone C I s Γ - ; isLimit = record { - limit = limit1 - ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} - ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} - } - } where - comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I) - → ΓMap s Γ f (TMap t i x) ≡ TMap t j x - comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) ) - limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) - limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; - sncommute = λ i j f → comm2 t f } - t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] - t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin - ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x - ≡⟨⟩ - TMap t i x - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → - ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] - limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin - limit1 a t x - ≡⟨⟩ - record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } - ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets ( λ i → eq1 x i )) (eq5 x ) ⟩ - record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j g → sncommute (f x ) i j g } - ≡⟨⟩ - f x - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i - eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t ) - eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x - eq2 x i j f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) - eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j - eq3 x i j k = sncommute (f x ) i j k - irr≅ : { c₂ : Level} {d e : Set c₂ } { x1 y1 : d } { x2 y2 : e } - ( ee : x1 ≅ x2 ) ( ee' : y1 ≅ y2 ) ( eq : x1 ≡ y1 ) ( eq' : x2 ≡ y2 ) → eq ≅ eq' - irr≅ refl refl refl refl = refl - eq4 : ( x : a) ( i j : Obj C ) ( g : I ) - → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ) ≅ sncommute (f x) i j g - eq4 x i j g = irr≅ (≡-to-≅ (≡cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g ) - eq5 : ( x : a) - → ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } )) - ≅ ( λ i j g → sncommute (f x) i j g ) - eq5 x = ≅extensionality (Sets {c₁} ) ( λ i → - ≅extensionality (Sets {c₁} ) ( λ j → - ≅extensionality (Sets {c₁} ) ( λ g → eq4 x i j g ) ) ) - -open Limit -open IsLimit -open IProduct - -SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C -SetsCompleteness {c₁} {c₂} C I s = record { - climit = λ Γ → SetsLimit {c₁} I C s Γ - ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; - equalizer = ( λ e → equ e ) ; - isEqualizer = SetsIsEqualizer a b f g } - ; cproduct = λ J fi → SetsIProduct J fi - } where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/SetsCompleteness1.agda Wed Jul 03 11:44:58 2024 +0900 @@ -0,0 +1,152 @@ +{-# OPTIONS --safe --with-K #-} + +open import Category -- https://github.com/konn/category-agda +open import Level +open import Category.Sets + +module SetsCompleteness1 where + +open import Definitions +open import Relation.Binary.Core +open import Function +import Relation.Binary.PropositionalEquality + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open Small + +open import Axiom.Extensionality.Propositional + +open Functor + + +ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) + (i : Obj C ) → Set c₁ +ΓObj s Γ i = FObj Γ i + +ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) + {i j : Obj C } → ( f : I ) → ΓObj s Γ i → ΓObj s Γ j +ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) + +record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) + ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where + field + snmap : ( i : OC ) → sobj i + sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j + +open snat + +open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ) + using (_≅_;refl; ≡-to-≅) + +open import Axiom.Extensionality.Heterogeneous renaming ( Extensionality to HExtensionality ) + +snat-cong : {c : Level} + {I OC : Set c} + {sobj : OC → Set c} + {smap : {i j : OC} → (f : I) → sobj i → sobj j} + → (s t : snat sobj smap) + → (snmap-≡ : snmap s ≡ snmap t) + → (sncommute-≅ : sncommute s ≅ sncommute t) + → s ≡ t +snat-cong _ _ refl refl = refl + +open import HomReasoning +open NTrans + +Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) + → ( Γ : Functor C (Sets {c₁} ) ) + → NTrans C Sets (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ +Cone C I s Γ = record { + TMap = λ i → λ sn → snmap sn i + ; isNTrans = record { commute = comm1 } + } where + comm1 : {a b : Obj C} {f : Hom C a b} → + Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ + Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] + comm1 {a} {b} {f} sn = begin + FMap Γ f (snmap sn a ) + ≡⟨ cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩ + FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) + ≡⟨⟩ + ΓMap s Γ (hom→ s f) (snmap sn a ) + ≡⟨ sncommute sn a b (hom→ s f) ⟩ + snmap sn b + ∎ where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning + + +SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) + → ( (a b : Level) → HExtensionality a b ) + → ( (a b : Level) → Extensionality a b ) + → Limit C Sets Γ +SetsLimit {c₁} I C s Γ hext ext = record { + a0 = snat (ΓObj s Γ) (ΓMap s Γ) + ; t0 = Cone C I s Γ + ; isLimit = record { + limit = limit1 + ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} + ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} + } + } where + comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I) + → ΓMap s Γ f (TMap t i x) ≡ TMap t j x + comm2 {a} {x} t f = IsNTrans.commute ( isNTrans t ) x + limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) + limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; + sncommute = λ i j f → comm2 t f } + t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] + t0f=t {a} {t} {i} x = begin + ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x + ≡⟨⟩ + TMap t i x + ∎ where + open ≡-Reasoning + limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → + ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] + limit-uniqueness {a} {t} {f} cif=t x = begin + limit1 a t x + ≡⟨⟩ + record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } + ≡⟨ snat-cong (limit1 a t x) (f x ) eq10 (eq5 x ) ⟩ + record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j g → sncommute (f x ) i j g } + ≡⟨⟩ + f x + ∎ where + open ≡-Reasoning + eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i + eq1 x i = sym ( cif=t x ) + eq10 : snmap (limit1 a t x) ≡ snmap (f x) + eq10 = ext _ _ ( λ i → eq1 x i ) + eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x + eq2 x i j y = IsNTrans.commute ( isNTrans t ) x + eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j + eq3 x i j k = sncommute (f x ) i j k + irr≅ : { c₂ : Level} {d e : Set c₂ } { x1 y1 : d } { x2 y2 : e } + ( ee : x1 ≅ x2 ) ( ee' : y1 ≅ y2 ) ( eq : x1 ≡ y1 ) ( eq' : x2 ≡ y2 ) → eq ≅ eq' + irr≅ refl refl refl refl = refl + eq4 : ( x : a) ( i j : Obj C ) ( g : I ) + → ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } x ) ≅ sncommute (f x) i j g + eq4 x i j g = irr≅ (≡-to-≅ (cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g ) + eq5 : ( x : a) + → ( λ i j g → IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } x ) + ≅ ( λ i j g → sncommute (f x) i j g ) + eq5 x = hext _ _ ? ( λ i → + hext _ _ ? ( λ j → + hext _ _ ? ( λ g → eq4 x i j g ) ) ) + +open Limit +open IsLimit +open IProduct + +open import SetsCompleteness + +SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete {c₁} {c₂} {ℓ} (Sets {c₁}) +SetsCompleteness {c₁} {c₂} C I s = record { + climit = λ Γ → ? -- SetsLimit {c₁} I C s ? ? ? + ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; + equalizer = ( λ e → equ e ) ; + isEqualizer = SetsIsEqualizer ? a b f g } + ; cproduct = λ J fi → SetsIProduct J fi ? + }
--- a/src/ToposEx.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/ToposEx.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --allow-unsolved-metas #-} -- {-# OPTIONS --cubical-compatible #-} @@ -382,9 +383,9 @@ pb : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → Pullback A (smc d f dm) (id1 A _) uniq : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → (p : Hom A a b) → Pullback A p (id1 A _) → A [ smc d f dm ≈ p ] - postulate - I : Set c₁ - small : Small A I +-- postulate +-- I : Set c₁ +-- small : Small A I -- open import yoneda A I small --
--- a/src/applicative.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/applicative.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,11 +1,25 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category -module applicative where +open import Definitions +open Functor + +-- +-- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem. +-- +-- they say it is not possible to prove FreeTheorem in Agda nor Coq +-- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities +-- so we postulate this + +module applicative ( + FT : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → FreeTheorem C D {a} {b} {c} ) + where + open import Data.Product renaming (_×_ to _*_) hiding (_<*>_) open import Category.Constructions.Product open import HomReasoning -open import cat-utility open import Relation.Binary.Core open import Relation.Binary open import monoidal @@ -20,22 +34,6 @@ ---- ----- --- --- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem. --- --- they say it is not possible to prove FreeTheorem in Agda nor Coq --- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities --- so we postulate this - -open Functor - -postulate - FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } - → (F : Functor C D ) - → (fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) - → {h f : Hom C a b } → {g k : Hom C b c } - → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ] - UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D) {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] ) @@ -46,7 +44,7 @@ id1 D (FObj F b) o fmap f ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩ FMap F (id1 C b) o fmap f - ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩ + ≈⟨ FT C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩ fmap (id1 C b) o FMap F f ≈⟨ car eq ⟩ id1 D (FObj F b) o FMap F f @@ -60,7 +58,6 @@ _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c _・_ f g = λ x → f ( g x ) - record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) ) ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b ) @@ -125,7 +122,8 @@ pure id <*> x ≡⟨ IsApplicative.identity ismf ⟩ x - ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x + ≡⟨ sym ( IsFunctor.identity (isFunctor F ) x ) ⟩ + FMap F id x ∎ ) where open Relation.Binary.PropositionalEquality @@ -133,7 +131,7 @@ F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x F→pure {a} {b} {f} {x} = sym ( begin pure f <*> x - ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x → IsApplicative.identity ismf ))) ⟩ + ≡⟨ (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) (λ x → IsApplicative.identity ismf )) x ⟩ FMap F f x ∎ ) where @@ -183,7 +181,7 @@ (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩ (FMap F (λ j k → f j , k) x) <*> (FMap F g y) - ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩ + ≡⟨ ≡-cong ( λ k → k <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ) x ) ⟩ (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y) ≡⟨⟩ φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) ) @@ -193,7 +191,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] - φab-comm {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x ) + φab-comm {a} {b} {f} = λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x associativity0 : {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ o Sets [ id1 Sets (FObj F a) □ φ o Iso.≅→ (mα-iso isM) ] ]) x ≡ (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x associativity0 {x} {y} {f} ((a , b) , c ) = begin @@ -253,7 +251,7 @@ associativity : {a b c : Obj Sets} → Sets [ Sets [ φ o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] - associativity {a} {b} {c} = extensionality Sets ( λ x → associativity0 x ) + associativity {a} {b} {c} x = associativity0 x unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x @@ -284,7 +282,7 @@ unitarity-idr : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] - unitarity-idr {a} {b} = extensionality Sets ( λ x → unitarity-idr0 {a} {b} x ) + unitarity-idr {a} {b} x = unitarity-idr0 {a} {b} x unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x @@ -310,7 +308,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] - unitarity-idl {a} {b} = extensionality Sets ( λ x → unitarity-idl0 {a} {b} x ) + unitarity-idl {a} {b} x = unitarity-idl0 {a} {b} x ---- -- @@ -354,10 +352,10 @@ FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } { f : Hom Sets (c * d) e } { x : FObj F a } { y : FObj F b } - → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( f o map g h ) ( φ ( x , y ) ) + → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) ) FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin - FMap F ( f o map g h ) ( φ ( x , y ) ) - ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩ + FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) ) + ≡⟨ IsFunctor.distr (isFunctor F) ( φ ( x , y )) ⟩ FMap F f (( FMap F ( map g h ) ) ( φ ( x , y ))) ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩ FMap F f ( φ ( FMap F g x , FMap F h y ) ) @@ -365,17 +363,17 @@ where open Relation.Binary.PropositionalEquality.≡-Reasoning u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u - u→F {a} {u} = sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) ) + u→F {a} {u} = sym ( IsFunctor.identity ( isFunctor F ) u) φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u φunitr {a} {u} = sym ( begin FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) ) - ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ - (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) ) - ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩ + ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩ + (FMap F ( Sets [ (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)) ] )) ( φ ( unit , u) ) + ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mλ-iso isM)) _ ⟩ FMap F id ( φ ( unit , u) ) - ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ + ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩ id ( φ ( unit , u) ) ≡⟨⟩ φ ( unit , u) @@ -387,11 +385,11 @@ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) ) - ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ - (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) ) - ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩ + ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩ + (FMap F (Sets [ (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)) ] )) ( φ ( u , unit ) ) + ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mρ-iso isM)) _ ⟩ FMap F id ( φ ( u , unit ) ) - ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ + ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩ id ( φ ( u , unit ) ) ≡⟨⟩ φ ( u , unit ) @@ -431,7 +429,7 @@ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ - (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩ + (k , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w)) ≡⟨⟩ @@ -440,26 +438,26 @@ ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩ - FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w)) + FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id ]) (φ (u , v)) , w)) ≡⟨⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w)) ≡⟨ FφF→F ⟩ - FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w)) + FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id ] ) (φ (φ (u , v) , w)) ≡⟨⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w)) - ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩ + ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) (sym (IsFunctor.identity (isFunctor F ) _)) ⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) ) - ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F k (φ (φ (u , v) , w)) ) ) (sym (Iso.iso→ (mα-iso isM))) ⟩ - FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F ( (Iso.≅← (mα-iso isM)) o (Iso.≅→ (mα-iso isM))) (φ (φ (u , v) , w)) ) - ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F )) ⟩ + ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k ) (sym (IsFunctor.≈-cong (isFunctor F) (Iso.iso→ (mα-iso isM)) _)) ⟩ + FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Sets [ (Iso.≅← (mα-iso isM)) o (Iso.≅→ (mα-iso isM)) ] ) (φ (φ (u , v) , w)) ) + ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) ( IsFunctor.distr (isFunctor F ) _ ) ⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) ( FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (u , v) , w)) )) ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w)))) ≡⟨⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w)))) - ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩ + ≡⟨ (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩ FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w))) ≡⟨⟩ FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) @@ -478,14 +476,14 @@ ≡⟨⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit)) ≡⟨ FφF→F ⟩ - FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit)) + FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x) ] ) (φ (unit , unit)) ≡⟨⟩ FMap F (λ y → f x) (φ (unit , unit)) ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩ FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit) ≡⟨⟩ FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit) - ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ + ≡⟨ sym (IsFunctor.distr (isFunctor F) _) ⟩ FMap F (λ y → f x) unit ≡⟨⟩ pure (f x) @@ -500,21 +498,21 @@ ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit)) ≡⟨ FφF→F ⟩ - FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit)) + FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map id (λ y → x) ] ) (φ (u , unit)) ≡⟨⟩ FMap F (λ r → proj₁ r x) (φ (u , unit)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩ FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u ) - ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ - FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u + ≡⟨ ( sym ( IsFunctor.distr (isFunctor F ) _) ) ⟩ + FMap F (Sets [ ( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) )) ] ) u ≡⟨⟩ - FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u - ≡⟨ left ( IsFunctor.distr (isFunctor F )) ⟩ + FMap F (Sets [( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) )) ] ) u + ≡⟨ IsFunctor.distr (isFunctor F ) _ ⟩ FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩ FMap F (λ r → proj₂ r x) (φ (unit , u)) ≡⟨⟩ - FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u)) + FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id ] ) (φ (unit , u)) ≡⟨ sym FφF→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩ @@ -562,7 +560,7 @@ FMap F (map f g) (φ (x , y)) ≡⟨⟩ FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y) - ≡⟨ ≡-cong ( λ h → h (x , y)) ( IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF ))) ⟩ + ≡⟨ IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF )) _ ⟩ <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y) ≡⟨⟩ φ (FMap F f x , FMap F g y) @@ -571,10 +569,10 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c)) - assocφ {x} {y} {z} {a} {b} {c} = ≡-cong ( λ h → h ((a , b) , c ) ) ( IsMonoidalFunctor.associativity isMF ) + assocφ {x} {y} {z} {a} {b} {c} = IsMonoidalFunctor.associativity isMF _ idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x - idrφ {a} {x} = ≡-cong ( λ h → h (x , OneObj ) ) ( IsMonoidalFunctor.unitarity-idr isMF {a} {One} ) + idrφ {a} {x} = IsMonoidalFunctor.unitarity-idr isMF {a} {One} (x , OneObj) idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x - idlφ {a} {x} = ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a} ) + idlφ {a} {x} = IsMonoidalFunctor.unitarity-idl isMF {One} {a} (OneObj , x) -- end
--- a/src/freyd.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/freyd.agda Wed Jul 03 11:44:58 2024 +0900 @@ -23,7 +23,7 @@ preinitialArrow : ∀{a : Obj A } → Hom A ( FObj (InclusiveFunctor A P ) record { s = preinitialObj; p = Pp } ) a -- initial object --- now in cat-utility +-- now in Definitions -- record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where -- field -- initial : ∀( a : Obj A ) → Hom A i a
--- a/src/freyd1.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/freyd1.agda Wed Jul 03 11:44:58 2024 +0900 @@ -67,13 +67,13 @@ -- Limit on A from Γ : I → CommaCategory -- -LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) +LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) → Limit I C (G ○ (FIA Γ)) LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ)) -tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) +tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → NTrans I C (K I C (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) tu {I} comp Γ = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] @@ -107,11 +107,11 @@ ≈⟨ assoc ⟩ ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ∎ -limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) +limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) -commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) +commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) → Obj CommaCategory commaLimit {I} comp Γ glimit = record { @@ -120,7 +120,7 @@ } -commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) +commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) → NTrans I CommaCategory (K I CommaCategory (commaLimit {I} comp Γ glimit)) Γ commaNat {I} comp Γ glimit = record { @@ -186,7 +186,7 @@ ∎ -comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) +comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) comma-a0 {I} comp Γ glimit a t = record { arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) @@ -244,7 +244,7 @@ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ∎ -comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) +comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) (i : Obj I ) → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ] comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin @@ -253,7 +253,7 @@ TMap (NIA {I} Γ a t ) i ∎ -comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) +comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → ( f : Hom CommaCategory a (commaLimit comp Γ glimit)) → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] ) @@ -264,7 +264,7 @@ arrow f ∎ -hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) +hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete {c₁} {c₂} {ℓ} A ) → ( glimit : LimitPreserve I A C G ) → ( Γ : Functor I CommaCategory ) → Limit I CommaCategory Γ
--- a/src/freyd2.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/freyd2.agda Wed Jul 03 11:44:58 2024 +0900 @@ -324,7 +324,7 @@ -- Adjoint Functor Theorem -- -module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) +module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete {c₁} {c₂} {ℓ} A ) (U : Functor A B ) (i : (b : Obj B) → Obj ( K A B b ↓ U) ) (In : (b : Obj B) → HasInitialObject ( K A B b ↓ U) (i b) )
--- a/src/group.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/group.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + -- Free Group and it's Universal Mapping ---- using Sets and forgetful functor @@ -10,7 +12,7 @@ open import Category.Sets open import Category.Cat open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Structures open import universal-mapping open import Relation.Binary.PropositionalEquality hiding ( [_] ) @@ -216,8 +218,8 @@ Homomorph : ? Homomorph = ? -_==_ : ? -_==_ = ? +-- _==_ : ? +-- _==_ = ? _*_ : ? _*_ = ? @@ -230,7 +232,7 @@ ; identityL = refl ; identityR = refl ; associative = refl - ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} + ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} → ? -- o-resp-≈ {a} {b} {c} {f} {g} {h} {i} } where isEquivalence1 : { a b : (Group c c) } → ? @@ -262,7 +264,7 @@ ; _o_ = _*_ ; _≈_ = _==_ ; Id = ? - ; isCategory = isGroups + ; isCategory = ? -- isGroups } open import Data.Unit
--- a/src/limit-to.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/limit-to.agda Wed Jul 03 11:44:58 2024 +0900 @@ -36,7 +36,7 @@ --- --- -open Complete +-- open Complete open Limit open IsLimit open NTrans
--- a/src/list-monoid-cat.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/list-monoid-cat.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,7 +1,9 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Level open import HomReasoning -open import cat-utility +open import Definitions module list-monoid-cat (c : Level ) where @@ -45,12 +47,12 @@ o-resp-≈ : {A : Set} → {f g : List A } → {h i : List A } → f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) o-resp-≈ {A} refl refl = refl - isEquivalence1 : {A : Set} → IsEquivalence {_} {_} {List A } _≡_ - isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types - record { refl = refl - ; sym = sym - ; trans = trans - } + isEquivalence1 : {A : Set} → ? -- IsEquivalence {_} {_} {List A } _≡_ + isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types + -- record { refl = refl + -- ; sym = sym + -- ; trans = trans + -- } ListCategory : (A : Set) → Category _ _ _ ListCategory A = record { Obj = ListObj @@ -62,7 +64,7 @@ } open import Algebra.Structures -open import Algebra.FunctionProperties using (Op₁; Op₂) +-- open import Algebra.FunctionProperties using (Op₁; Op₂) data MonoidObj : Set c where ! : MonoidObj @@ -71,7 +73,7 @@ infixl 7 _∙_ field Carrier : Set c - _∙_ : Op₂ Carrier + _∙_ : Carrier → Carrier → Carrier ε : Carrier isMonoid : IsMonoid _≡_ _∙_ ε @@ -89,12 +91,12 @@ o-resp-≈ : {M : ≡-Monoid c} → {f g : Carrier M } → {h i : Carrier M } → f ≡ g → h ≡ i → (_∙_ M h f) ≡ (_∙_ M i g) o-resp-≈ {A} refl refl = refl - isEquivalence1 : {M : ≡-Monoid c} → IsEquivalence {_} {_} {Carrier M } _≡_ - isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types - record { refl = refl - ; sym = sym - ; trans = trans - } + isEquivalence1 : {M : ≡-Monoid c} → ? -- IsEquivalence {_} {_} {Carrier M } _≡_ + isEquivalence1 {A} = ? -- this is the same function as A's equivalence but has different types + -- record { refl = refl + -- ; sym = sym + -- ; trans = trans + -- } MonoidCategory : (M : ≡-Monoid c) → Category _ _ _ MonoidCategory M = record { Obj = MonoidObj
--- a/src/maybe-monad.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/maybe-monad.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category open import Category.Sets module maybe-monad {c : Level} where open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Core open import Category.Cat @@ -25,9 +27,9 @@ FObj = λ a → maybe a ; FMap = λ {a} {b} f → fmap f ; isFunctor = record { - identity = λ {x} → extensionality A ( λ y → identity1 x y ) - ; distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ w → distr2 a b c f g w ) - ; ≈-cong = λ {a} {b} {c} {f} f≡g → extensionality A ( λ z → ≈-cong1 a b c f z f≡g ) + identity = λ {x} y → identity1 x y + ; distr = λ {a} {b} {c} {f} {g} w → distr2 a b c f g w + ; ≈-cong = λ {a} {b} {f} {g} f≈g z → ≈-cong1 a b f g z f≈g } } where fmap : {a b : Obj A} → (f : Hom A a b ) → Hom A (maybe a) (maybe b) @@ -39,9 +41,9 @@ distr2 : (x y z : Obj A) (f : Hom A x y ) ( g : Hom A y z ) → (w : maybe x) → fmap (λ w → g (f w)) w ≡ fmap g ( fmap f w) distr2 x y z f g nothing = refl distr2 x y z f g (just w) = refl - ≈-cong1 : (x y : Obj A) ( f g : Hom A x y ) → ( z : maybe x ) → f ≡ g → fmap f z ≡ fmap g z - ≈-cong1 x y f g nothing refl = refl - ≈-cong1 x y f g (just z) refl = refl + ≈-cong1 : (x y : Obj A) ( f g : Hom A x y ) → ( z : maybe x ) → Sets [ f ≈ g ] → fmap f z ≡ fmap g z + ≈-cong1 x y f g nothing eq = refl + ≈-cong1 x y f g (just z) eq = cong just ( eq z ) -- Maybe-η : 1 → M @@ -61,7 +63,7 @@ comm : (a b : Obj A) (f : Hom A a b) → A [ A [ Functor.FMap Maybe f o (λ x → just x) ] ≈ A [ (λ x → just x) o FMap (identityFunctor {_} {_} {_} {A} ) f ] ] - comm a b f = extensionality A ( λ x → comm1 a b f x ) + comm a b f x = comm1 a b f x @@ -85,7 +87,7 @@ comm1 a b f (just (just x)) = refl comm : {a b : Obj A} {f : Hom A a b} → 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 ) + comm {a} {b} {f} x = comm1 a b f x MaybeMonad : Monad A MaybeMonad = record { @@ -112,13 +114,13 @@ assoc-1 a (just (just (just x) )) = refl unity1 : {a : Obj A} → A [ A [ TMap Maybe-μ a o TMap Maybe-η (FObj Maybe a) ] ≈ id1 A (FObj Maybe a) ] - unity1 {a} = extensionality A ( λ x → unity1-1 a x ) + unity1 {a} x = unity1-1 a x unity2 : {a : Obj A} → A [ A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-η a) ] ≈ id1 A (FObj Maybe a) ] - unity2 {a} = extensionality A ( λ x → unity2-1 a x ) + unity2 {a} x = unity2-1 a x assoc : {a : Obj A} → A [ A [ TMap Maybe-μ a o TMap Maybe-μ (FObj Maybe a) ] ≈ A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-μ a) ] ] - assoc {a} = extensionality A ( λ x → assoc-1 a x ) + assoc {a} x = assoc-1 a x
--- a/src/monad→monoidal.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/monad→monoidal.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category module monad→monoidal where @@ -5,7 +7,7 @@ open import Data.Product renaming (_×_ to _*_) hiding (_<*>_) open import Category.Constructions.Product open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Core open import Relation.Binary @@ -49,8 +51,8 @@ natφ' : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) natφ' {a} {b} {c} {d} {x} {y} {f} {g} = monoidal.≡-cong ( λ h → h x ) ( begin - ( λ x → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (μ (Σ a (λ k → b)))) ( FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x )) - ≈⟨⟩ + -- ( λ x → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (μ (Σ a (λ k → b)))) ( FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x )) + -- ≈⟨⟩ (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (μ (Σ a (λ k → b)))) o FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) ≈⟨ car {_} {_} {_} {_} {_} {FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)} ( nat (Monad.μ monad) ) ⟩ ( μ ( c * d) o FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)))) o FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) @@ -60,22 +62,22 @@ FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) ) ≈⟨⟩ FMap F (λ x₁ → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)) x₁) - ≈⟨ fcong F ( extensionality Sets ( λ x₁ → monoidal.≡-cong ( λ h → h x₁ ) ( begin + ≈⟨ fcong F ( λ x₁ → monoidal.≡-cong ( λ h → h x₁ ) ( begin FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y ) ≈⟨⟩ ( λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y) ) ≈⟨⟩ ( λ x₁ → ( FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o FMap F (λ g₁ → x₁ , g₁) ) y ) - ≈↑⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( extensionality Sets ( λ x₁ → distr F )) ⟩ + ≈↑⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( ( λ x₁ → distr F )) ⟩ ( λ x₁ → FMap F (λ g₁ → ( λ xy → f (proj₁ xy) , g (proj₂ xy)) (x₁ , g₁)) y ) ≈⟨⟩ ( λ x₁ → FMap F (λ g₁ → f x₁ , g g₁) y ) - ≈⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( extensionality Sets ( λ x₁ → distr F )) ⟩ + ≈⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( ( λ x₁ → distr F )) ⟩ ( λ x₁ → ( FMap F (λ g₁ → f x₁ , g₁) o FMap F g ) y ) ≈⟨⟩ ( λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y) ) ∎ - ) ) ) ⟩ + ) ) ⟩ FMap F (λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y)) ≈⟨⟩ FMap F ( (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o f ) @@ -87,7 +89,7 @@ ≈⟨⟩ ( λ x → μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x))) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin @@ -104,7 +106,7 @@ μ (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)) x) ≡⟨⟩ (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)))) x - ≡⟨ sym ( ≡-cong ( λ h → (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → ( h x₁ y )))) x ) ( extensionality Sets ( λ x → IsFunctor.distr ( Functor.isFunctor F ) ))) ⟩ + ≡⟨ sym ( ≡-cong ( λ h → (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → ( h x₁ y )))) x ) ( λ x → IsFunctor.distr ( Functor.isFunctor F ) )) ⟩ (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F ((λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (λ g₁ → x₁ , g₁) ) y))) x ≡⟨⟩ μ (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ x₂ → f x₁ , g x₂) y) x) @@ -120,7 +122,7 @@ μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → f₁ , g k) y) (FMap F f x)) ≡⟨⟩ μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → ((λ g₁ → f₁ , g₁) (g k))) y) (FMap F f x)) - ≡⟨ ≡-cong ( λ h → μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → h f₁ y ) (FMap F f x ))) ( extensionality Sets ( λ x → (IsFunctor.distr ( Functor.isFunctor F ) ) )) ⟩ + ≡⟨ ≡-cong ( λ h → μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → h f₁ y ) (FMap F f x ))) ( λ x → (IsFunctor.distr ( Functor.isFunctor F ) ) ) ⟩ μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x)) ≡⟨⟩ φ (FMap F f x , FMap F g y) @@ -131,7 +133,7 @@ ≡←≈ refl = refl -- fcongλ : { a b c : Obj (Sets {l} ) } { x y : a → Hom (Sets {l}) a b } → Sets [ x ≈ y ] → ( g : ? ) -- → Sets [ FMap F ( λ (f : a) → ( x f )) ≈ FMap F ( λ (f : a ) → ( y f )) ] - -- fcongλ {a} {b} {c} {x} {y} g eq = let open ≈-Reasoning (Sets {l}) hiding ( _o_ ) in fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → g h f ) eq + -- fcongλ {a} {b} {c} {x} {y} g eq = let open ≈-Reasoning (Sets {l}) hiding ( _o_ ) in fcong F ( λ f → monoidal.≡-cong ( λ h → g h f ) eq ) assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) assocφ {x} {y} {z} {a} {b} {c} = monoidal.≡-cong ( λ h → h a ) ( begin @@ -142,21 +144,21 @@ μ ( x * ( y * z ) ) o (FMap F (λ f → ( FMap F (λ g → f , g) o ( μ (y * z ) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) )) b )) ≈⟨⟩ -- assoc μ ( x * ( y * z ) ) o (FMap F (λ f → ( (FMap F (λ g → f , g) o ( μ (y * z ))) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) ) b )) - ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) - ( car {_} {_} {_} {_} {_} { FMap F (λ f₁ → FMap F (λ g → f₁ , g) c )} (nat (Monad.μ monad ))) ) )) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (λ f → monoidal.≡-cong ( λ h → h b ) + ( car {_} {_} {_} {_} {_} { FMap F (λ f₁ → FMap F (λ g → f₁ , g) c )} (nat (Monad.μ monad ))) )) ⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( ( μ ( x * ( y * z ) ) o FMap F (FMap F (λ g → f , g)) ) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) ) b )) ≈⟨⟩ -- assoc μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (FMap F (λ g → f , g)) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c )) ) b )) - ≈↑⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) - ( cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) )} (distr F)) ) )) ⟩ + ≈↑⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (λ f → monoidal.≡-cong ( λ h → h b ) + ( cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) )} (distr F)) )) ⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (FMap F (λ g → f , g) o (λ f₁ → FMap F (λ g → f₁ , g) c)))) b )) ≈⟨⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F ((λ f₁ → (FMap F (λ g → f , g) o FMap F (λ g → f₁ , g)) c)))) b )) - ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) ( begin + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (λ f → monoidal.≡-cong ( λ h → h b ) ( begin μ (x * y * z) o FMap F (λ f₁ → (FMap F (λ g → f , g) o FMap F (λ g → f₁ , g)) c) - ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ (x * y * z)} ( fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h c ) ( distr F) ))) ⟩ + ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ (x * y * z)} ( fcong F ( (λ f → monoidal.≡-cong ( λ h → h c ) ( distr F) ))) ⟩ μ (x * y * z) o FMap F (λ f₁ → FMap F ((λ g → f , g) o (λ g → f₁ , g)) c) ∎ - ) ))) ⟩ + ) )) ⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ f₁ → (FMap F ((λ g → f , g) o (λ g → f₁ , g))) c))) b )) ≈⟨⟩ μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c))) b )) @@ -172,13 +174,13 @@ FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b ) ≈⟨⟩ FMap F ( λ h → ( FMap F (( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ g → h , g))) b ) - ≈⟨ fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) (distr F) )) ⟩ + ≈⟨ fcong F ( λ f → monoidal.≡-cong ( λ h → h b ) (distr F) ) ⟩ FMap F ( λ h → ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (FMap F (λ g → h , g))) b ) ≈⟨⟩ FMap F ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ h → FMap F (λ g → h , g) b) ) ≈⟨⟩ FMap F ( FMap F ( λ f → ( FMap F ((λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ g → f , g))) c) o (λ f → FMap F (λ g → f , g) b)) - ≈⟨ fcong F ( car ( fcong F ( extensionality Sets (λ f → monoidal.≡-cong ( λ h → h c ) ( distr F ) )))) ⟩ + ≈⟨ fcong F ( car ( fcong F ( λ f → monoidal.≡-cong ( λ h → h c ) ( distr F ) ))) ⟩ FMap F ( FMap F ( λ f → ( FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o FMap F (λ g → f , g)) c) o (λ f → FMap F (λ g → f , g) b) ) ≈⟨⟩ FMap F ( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ f → FMap F (λ g → f , g) c)) o (λ f → FMap F (λ g → f , g) b) ) @@ -221,7 +223,7 @@ ≈⟨⟩ ( λ a → FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) ) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets proj1 : {a : Obj Sets} → _*_ {l} {l} a One → a proj1 = proj₁ proj2 : {a : Obj Sets} → _*_ {l} {l} One a → a @@ -237,7 +239,7 @@ FMap F proj₁ o (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) o η One ) OneObj )) ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( cdr {_} {_} {_} {_} {_} {μ (a * One ) } ( fcong F ( begin (λ f → ( FMap F (λ g → f , g) o η One ) OneObj ) - ≈⟨ monoidal.≡-cong ( λ h → λ f → (h f) OneObj ) (extensionality Sets (λ f → ( + ≈⟨ monoidal.≡-cong ( λ h → λ f → (h f) OneObj ) (λ f → ( begin FMap F (λ g → f , g) o η One ≈⟨ nat ( Monad.η monad ) ⟩ @@ -245,7 +247,7 @@ ≈⟨⟩ η (a * One) o ( λ g → ( f , g ) ) ∎ - ))) ⟩ + )) ⟩ (λ f → ( η (a * One) o ( λ g → ( f , g ) ) ) OneObj ) ≈⟨⟩ η (a * One ) o ( λ f → ( f , OneObj ) ) @@ -267,7 +269,7 @@ ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ id1 Sets (FObj F a) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x idlφ {a} {x} = monoidal.≡-cong ( λ h → h x ) ( begin ( λ x → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ) @@ -275,7 +277,7 @@ ( λ x → FMap F proj₂ (μ (One * a ) (FMap F (λ f → FMap F (λ g → f , g) x) (η One OneObj)))) ≈⟨⟩ ( λ x → ( FMap F proj₂ o (μ (One * a ) o (FMap F (λ f → FMap F (λ g → f , g) x) o η One) )) OneObj ) - ≈⟨ monoidal.≡-cong ( λ h → λ x → ( FMap F proj₂ o (μ (One * a ) o h x )) OneObj ) ( extensionality (Sets {l}) ( λ x → nat (Monad.η monad ) )) ⟩ + ≈⟨ monoidal.≡-cong ( λ h → λ x → ( FMap F proj₂ o (μ (One * a ) o h x )) OneObj ) ( λ x → nat (Monad.η monad ) ) ⟩ (λ x → (FMap F proj2 o (μ (One * a) o (η (FObj F (One * a)) o FMap (identityFunctor {_} {_} {_} {Sets {l}} ) (λ f → FMap F (λ g → f , g) x) ))) OneObj) ≈⟨⟩ FMap F proj2 o (μ (One * a ) o (η (FObj F (One * a)) o ( FMap F (λ g → (OneObj , g )) ))) @@ -292,7 +294,7 @@ ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ id1 Sets (FObj F a) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m ) Monad→Applicative {l} monad = record { @@ -326,7 +328,7 @@ ( λ u → μ a (FMap F (λ k → FMap F k u) (η (a → a) (λ x → x)))) ≈⟨⟩ (λ u → μ a ((FMap F (λ k → FMap F k u) o η (a → a)) (id1 Sets a ))) - ≈⟨ ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans (Monad.η monad ) )))) ⟩ + ≈⟨ ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( λ x → (IsNTrans.commute (NTrans.isNTrans (Monad.η monad ) ))) ⟩ (λ u → μ a ( (η (FObj F a) o FMap F ( (id1 Sets a )) ) u ) ) ≈⟨⟩ μ a o (η (FObj F a) o FMap F (id1 Sets a)) @@ -340,7 +342,7 @@ ( λ u → u ) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a } → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w) composition {a} {b} {c} {u} {v} {w} = ≡cong ( λ h → h w ) ( begin @@ -376,29 +378,29 @@ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) ≈⟨⟩ ( λ w → ( μ c o ((FMap F (λ k → FMap F k w) o μ (a → c) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )))) u ) - ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} {μ c} ( car {_} {_} {_} {_} {_} { FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)))} (nat (Monad.μ monad)) )))) ⟩ + ≈⟨ (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} {μ c} ( car {_} {_} {_} {_} {_} { FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)))} (nat (Monad.μ monad)) )))) ⟩ ( λ w → ( μ c o ((μ (FObj F c) o FMap F (FMap F (λ k → FMap F k w) ) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )))) u ) ≈⟨⟩ -- assoc ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) - ≈↑⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} { μ c} (cdr {_} {_} {_} {_} {_} {μ (FObj F c)} ( distr F ))))) ⟩ + ≈↑⟨ (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} { μ c} (cdr {_} {_} {_} {_} {_} {μ (FObj F c)} ( distr F ))))) ⟩ ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) ≈⟨⟩ ( λ w → (( μ c o μ (FObj F c) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) - ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (car {_} {_} {_} {_} {_} {( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )} (IsMonad.assoc (Monad.isMonad monad )) ) )) ⟩ + ≈⟨ (λ w → ( ≡cong ( λ h → h u ) (car {_} {_} {_} {_} {_} {( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )} (IsMonad.assoc (Monad.isMonad monad )) ) )) ⟩ ( λ w → (( μ c o (FMap F ( μ c )) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) ≈⟨⟩ ( λ w → ( μ c o (FMap F ( μ c ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) - ≈↑⟨ extensionality Sets (λ w → ( ≡cong ( λ h → ( μ c o h) u ) (distr F) )) ⟩ + ≈↑⟨ (λ w → ( ≡cong ( λ h → ( μ c o h) u ) (distr F) )) ⟩ ( λ w → ( μ c o (FMap F ( μ c o (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) ≈⟨⟩ ( λ w → ( μ c o (FMap F (λ x → ( μ c o (FMap F (λ k → FMap F k w) o (FMap F (λ g x₁ → x (g x₁))))) v ))) u ) - ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → ( μ c o h ) u ) (fcong F ( extensionality Sets (λ k → ≡cong ( λ h → h v ) ( begin + ≈⟨ (λ w → ( ≡cong ( λ h → ( μ c o h ) u ) (fcong F ( (λ k → ≡cong ( λ h → h v ) ( begin μ c o (FMap F (λ x → FMap F x w) o (FMap F (λ g x₁ → k (g x₁)))) ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ c} ( distr F ) ⟩ μ c o (FMap F ((λ x → FMap F x w) o (λ g x₁ → k (g x₁)))) ≈⟨⟩ μ c o (FMap F ((λ x → (FMap F ( k o x ) w)))) - ≈⟨ cdr {_} {_} {_} {_} {_} {μ c} ( fcong F ( extensionality Sets ( λ x → ≡cong ( λ h → h w ) (distr F ) ))) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {μ c} ( fcong F ( ( λ x → ≡cong ( λ h → h w ) (distr F ) ))) ⟩ μ c o (FMap F ((λ x → (FMap F k o FMap F x ) w))) ≈⟨⟩ μ c o (FMap F (FMap F k o (λ h → FMap F h w))) @@ -417,7 +419,7 @@ ( λ w → u <*> (v <*> w) ) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) homomorphism {a} {b} {f} {x} = ≡cong ( λ h → h x ) ( begin ( λ x → pure f <*> pure x ) @@ -425,7 +427,7 @@ ( λ x → μ b (FMap F (λ k → FMap F k (η a x)) ((η (a → b) f)) )) ≈⟨⟩ μ b o ( λ x → (FMap F ( λ k → FMap F k (η a x) ) o η (a → b) ) f ) - ≈⟨ cdr {_} {_} {_} {_} {_} {μ b} ( extensionality Sets ( λ x → ≡cong ( λ h → h f ) ( nat ( Monad.η monad ) ))) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {μ b} ( ( λ x → ≡cong ( λ h → h f ) ( nat ( Monad.η monad ) ))) ⟩ μ b o ( λ x → (η (FObj F b) o (λ k → FMap F k (η a x)) ) f ) ≈⟨⟩ μ b o (η (FObj F b) o (FMap F f o η a )) @@ -443,7 +445,7 @@ ( λ x → pure (f x )) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u interchange {a} {b} {u} {x} = ≡cong ( λ h → h x ) ( begin ( λ x → u <*> pure x ) @@ -451,31 +453,31 @@ ( λ x → μ b (FMap F (λ k → FMap F k (η a x)) u)) ≈⟨⟩ ( λ x → (μ b o (FMap F (λ k → (FMap F k o η a) x))) u ) - ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) (fcong F ( extensionality Sets ( λ k → ≡cong ( λ h → h x ) ( nat ( Monad.η monad )))))) ⟩ + ≈⟨ ( λ x → ≡cong ( λ h → ( μ b o h) u ) (fcong F ( ( λ k → ≡cong ( λ h → h x ) ( nat ( Monad.η monad )))))) ⟩ ( λ x → (μ b o FMap F (λ k → (η b o k ) x)) u ) ≈⟨⟩ (λ x → (μ b o FMap F ( η b o (λ f → f x) )) u) - ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( fcong F (nat ( Monad.η monad ) ))) ⟩ + ≈↑⟨ ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( fcong F (nat ( Monad.η monad ) ))) ⟩ (λ x → (μ b o FMap F ( FMap F (λ f → f x) o η (a → b) )) u) - ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( distr F ) ) ⟩ + ≈⟨ ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( distr F ) ) ⟩ ( λ x → (μ b o ( FMap F ( FMap F (λ f → f x) ) o FMap F ( η (a → b) ))) u ) ≈⟨⟩ ( λ x → ( (μ b o (FMap F ( FMap F (λ f → f x) )) ) o FMap F ( η (a → b) )) u ) - ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( h o FMap F ( η (a → b) )) u ) ( nat ( Monad.μ monad ))) ⟩ + ≈↑⟨ ( λ x → ≡cong ( λ h → ( h o FMap F ( η (a → b) )) u ) ( nat ( Monad.μ monad ))) ⟩ ( λ x → ((FMap F (λ f → f x) o (μ (a → b) o FMap F ( η (a → b) )))) u ) - ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → (FMap F (λ f → f x) o h ) u ) ( IsMonad.unity2 ( Monad.isMonad monad ) )) ⟩ + ≈⟨ ( λ x → ≡cong ( λ h → (FMap F (λ f → f x) o h ) u ) ( IsMonad.unity2 ( Monad.isMonad monad ) )) ⟩ ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u ) - ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idR {_} {_} {FMap F (λ f → f x)} )) ⟩ + ≈⟨ ( λ x → ≡cong ( λ h → h u ) ( idR {_} {_} {FMap F (λ f → f x)} )) ⟩ ( λ x → ( FMap F (λ f → f x) ) u ) - ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idL {_} {_} { FMap F (λ f → f x) }) ) ⟩ + ≈↑⟨ ( λ x → ≡cong ( λ h → h u ) ( idL {_} {_} { FMap F (λ f → f x) }) ) ⟩ ( λ x → (id1 Sets (FObj F b ) o FMap F (λ f → f x) ) u ) - ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → (h o FMap F (λ f → f x) ) u ) ( IsMonad.unity1 ( Monad.isMonad monad ) )) ⟩ + ≈↑⟨ ( λ x → ≡cong ( λ h → (h o FMap F (λ f → f x) ) u ) ( IsMonad.unity1 ( Monad.isMonad monad ) )) ⟩ ( λ x → (( μ b o η (FObj F b )) o FMap F (λ f → f x) ) u ) ≈⟨⟩ ( λ x → ( μ b o ( η (FObj F b ) o FMap F (λ f → f x))) u ) ≈⟨⟩ ( λ x → ( μ b o ( η (FObj F b ) o (λ k → FMap F k u) )) (λ f → f x) ) - ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h ) (λ f → f x) ) ( nat ( Monad.η monad ))) ⟩ + ≈↑⟨ ( λ x → ≡cong ( λ h → ( μ b o h ) (λ f → f x) ) ( nat ( Monad.η monad ))) ⟩ ( λ x → ( μ b o ((FMap F (λ k → FMap F k u) ) o η ((f : a → b) → b))) (λ f → f x) ) ≈⟨⟩ ( λ x → (( μ b o (FMap F (λ k → FMap F k u) )) o η ((f : a → b) → b)) (λ f → f x) ) @@ -485,7 +487,7 @@ ( λ x → pure (λ f → f x) <*> u ) ∎ ) where - open ≈-Reasoning Sets hiding ( _o_ ) + open ≈-Reasoning Sets -- an easy one ( we already have HaskellMonoidal→Applicative )
--- a/src/monoid-monad.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/monoid-monad.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + open import Category -- https://github.com/konn/category-agda open import Algebra open import Level @@ -6,7 +8,7 @@ open import Algebra.Structures open import HomReasoning -open import cat-utility +open import Definitions open import Category.Cat open import Data.Product open import Relation.Binary.Core @@ -26,173 +28,157 @@ ε : Carrier -- id in Monoid isMonoid : IsMonoid _≡_ _*_ ε -postulate M : ≡-Monoid c -open ≡-Monoid - -infixl 7 _∙_ +module _ (M : ≡-Monoid c) where -_∙_ : ( m m' : Carrier M ) → Carrier M -_∙_ m m' = _*_ M m m' + open ≡-Monoid -A = Sets {c} - --- T : A → (M x A) + infixl 7 _∙_ -T : Functor A A -T = record { - FObj = λ a → (Carrier M) × a - ; FMap = λ f p → (proj₁ p , f (proj₂ p )) - ; isFunctor = record { - identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) - ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) - ; ≈-cong = cong1 - } - } where - cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → - Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ] - cong1 _≡_.refl = _≡_.refl + _∙_ : ( m m' : Carrier M ) → Carrier M + _∙_ m m' = _*_ M m m' -open Functor + A = Sets {c} + + -- T : A → (M x A) -Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → - A [ A [ FMap T f o (λ x → ε M , x) ] ≈ - A [ (λ x → ε M , x) o f ] ] -Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in - begin - FMap T f o (λ x → ε M , x) - ≈⟨⟩ - (λ x → ε M , x) o f - ∎ - --- η : a → (ε,a) -η : NTrans A A identityFunctor T -η = record { - TMap = λ a → λ(x : a) → ( ε M , x ) ; - isNTrans = record { - commute = Lemma-MM1 - } - } - --- μ : (m,(m',a)) → (m*m,a) + T : Functor A A + T = record { + FObj = λ a → (Carrier M) × a + ; FMap = λ f p → (proj₁ p , f (proj₂ p )) + ; isFunctor = record { + identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) + ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) + ; ≈-cong = λ f≈g x → cong (λ k → proj₁ x , k ) (f≈g (proj₂ x)) + } + } -muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a ) -muMap a ( m , ( m' , x ) ) = ( m ∙ m' , x ) - -Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → - A [ A [ FMap T f o (λ x → muMap a x) ] ≈ - A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] -Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in - begin - FMap T f o (λ x → muMap a x) - ≈⟨⟩ - (λ x → muMap b x) o FMap (T ○ T) f - ∎ + open Functor -μ : NTrans A A ( T ○ T ) T -μ = record { - TMap = λ a → λ x → muMap a x ; - isNTrans = record { - commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f} - } - } - -open NTrans - -Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) -Lemma-MM33 = _≡_.refl + Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → + A [ A [ FMap T f o (λ x → ε M , x) ] ≈ + A [ (λ x → ε M , x) o f ] ] + Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A in + begin + FMap T f o (λ x → ε M , x) + ≈⟨⟩ + (λ x → ε M , x) o f + ∎ -Lemma-MM34 : ∀( x : Carrier M ) → ε M ∙ x ≡ x -Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) + -- η : a → (ε,a) + η : NTrans A A identityFunctor T + η = record { + TMap = λ a → λ(x : a) → ( ε M , x ) ; + isNTrans = record { + commute = Lemma-MM1 + } + } -Lemma-MM35 : ∀( x : Carrier M ) → x ∙ ε M ≡ x -Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x - -Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) -Lemma-MM36 x y z = ( IsMonoid.assoc ( isMonoid M )) x y z - -import Relation.Binary.PropositionalEquality + -- μ : (m,(m',a)) → (m*m,a) --- Multi Arguments Functional Extensionality -extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → - (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g ) -extensionality30 eq = extensionality A ( λ x → extensionality A ( λ y → extensionality A (eq x y) ) ) + muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a ) + muMap a ( m , ( m' , x ) ) = ( m ∙ m' , x ) -Lemma-MM9 : (λ(x : Carrier M) → ( ε M ∙ x )) ≡ ( λ(x : Carrier M) → x ) -Lemma-MM9 = extensionality A Lemma-MM34 - -Lemma-MM10 : ( λ x → (x ∙ ε M)) ≡ ( λ x → x ) -Lemma-MM10 = extensionality A Lemma-MM35 - -Lemma-MM11 : (λ x y z → ((x ∙ y ) ∙ z)) ≡ (λ x y z → ( x ∙ (y ∙ z ) )) -Lemma-MM11 = extensionality30 Lemma-MM36 + Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → + A [ A [ FMap T f o (λ x → muMap a x) ] ≈ + A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] + Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A in + begin + FMap T f o (λ x → muMap a x) + ≈⟨⟩ + (λ x → muMap b x) o FMap (T ○ T) f + ∎ -MonoidMonad : Monad A -MonoidMonad = record { - T = T - ; η = η - ; μ = μ - ; isMonad = record { - unity1 = Lemma-MM3 ; - unity2 = Lemma-MM4 ; - assoc = Lemma-MM5 - } - } where - Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) hiding (_∙_) in - begin - TMap μ a o TMap η ( FObj T a ) - ≈⟨⟩ - ( λ x → ε M ∙ (proj₁ x) , proj₂ x ) - ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ - ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) - ≈⟨⟩ - ( λ x → x ) - ≈⟨⟩ - Id {_} {_} {_} {A} (FObj T a) - ∎ - Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] - Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) hiding (_∙_) in - begin - TMap μ a o (FMap T (TMap η a )) - ≈⟨⟩ - ( λ x → ( proj₁ x ∙ (ε M) , proj₂ x )) - ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ - ( λ x → (proj₁ x) , proj₂ x ) - ≈⟨⟩ - ( λ x → x ) - ≈⟨⟩ - Id {_} {_} {_} {A} (FObj T a) - ∎ - Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] - Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) hiding (_∙_) in - begin - TMap μ a o TMap μ ( FObj T a ) - ≈⟨⟩ - ( λ x → (proj₁ x) ∙ (proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) - ≈⟨ cong ( λ f → ( λ x → - (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) ) - )) Lemma-MM11 ⟩ - ( λ x → ( proj₁ x) ∙(( proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) - ≈⟨⟩ - TMap μ a o FMap T (TMap μ a) - ∎ + μ : NTrans A A ( T ○ T ) T + μ = record { + TMap = λ a → λ x → muMap a x ; + isNTrans = record { + commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f} + } + } + + open NTrans + + Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) + Lemma-MM33 = _≡_.refl + + Lemma-MM34 : ∀( x : Carrier M ) → ε M ∙ x ≡ x + Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) + + Lemma-MM35 : ∀( x : Carrier M ) → x ∙ ε M ≡ x + Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x + + Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) + Lemma-MM36 x y z = ( IsMonoid.assoc ( isMonoid M )) x y z + + import Relation.Binary.PropositionalEquality -F : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b ) -F m {a} {b} f = λ (x : a ) → ( m , ( f x) ) - -postulate m m' : Carrier M -postulate a b c' : Obj A -postulate f : b → c' -postulate g : a → b + MonoidMonad : Monad A + MonoidMonad = record { + T = T + ; η = η + ; μ = μ + ; isMonad = record { + unity1 = λ {a} x → Lemma-MM3 x ; + unity2 = Lemma-MM4 ; + assoc = Lemma-MM5 + } + } where + Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + Lemma-MM3 {a} x = let open ≡-Reasoning in + begin + (Sets [ TMap μ a o TMap η ( FObj T a ) ]) x + ≡⟨⟩ + ε M ∙ (proj₁ x) , proj₂ x + ≡⟨ cong (λ k → (k , proj₂ x)) ( Lemma-MM34 (proj₁ x) ) ⟩ + ( (proj₁ x) , proj₂ x ) + ≡⟨⟩ + x + ≡⟨⟩ + Id {_} {_} {_} {A} (FObj T a) x + ∎ + Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + Lemma-MM4 {a} x = let open ≡-Reasoning in + begin + (Sets [ TMap μ a o (FMap T (TMap η a ))] ) x + ≡⟨⟩ + proj₁ x ∙ (ε M) , proj₂ x + ≡⟨ cong (λ k → (k , proj₂ x)) ( Lemma-MM35 (proj₁ x) ) ⟩ + ((proj₁ x) , proj₂ x ) + ≡⟨⟩ + x + ≡⟨⟩ + Id {_} {_} {_} {A} (FObj T a) x + ∎ + Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] + Lemma-MM5 {a} x = let open ≡-Reasoning in + begin + (Sets [ TMap μ a o TMap μ ( FObj T a ) ]) x + ≡⟨⟩ + (muMap a ( muMap (Carrier M × a) x )) + ≡⟨ cong₂ (λ j k → ( j , k )) (Lemma-MM36 _ _ _ ) refl ⟩ + muMap a (proj₁ x , muMap a (proj₂ x)) + ≡⟨⟩ + (Sets [ TMap μ a o FMap T (TMap μ a)]) x + ∎ -Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g) + + F : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b ) + F m {a} {b} f = λ (x : a ) → ( m , ( f x) ) -open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad} + -- postulate m m' : Carrier M + -- postulate a b c' : Obj A + -- postulate f : b → c' + -- postulate g : a → b --- nat-ε TMap = λ a₁ → record { KMap = λ x → x } --- nat-η TMap = λ a₁ → _,_ (ε, M) --- U_T Functor Kleisli A --- U_T FObj = λ B → Σ (Carrier M) (λ x → B) FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x))) , proj₂ (KMap f₁ (proj₂ x)) --- F_T Functor A Kleisli --- F_T FObj = λ a₁ → a₁ FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x } + -- Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g) + + open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad} + + -- nat-ε TMap = λ a₁ → record { KMap = λ x → x } + -- nat-η TMap = λ a₁ → _,_ (ε, M) + -- U_T Functor Kleisli A + -- U_T FObj = λ B → Σ (Carrier M) (λ x → B) FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x))) , proj₂ (KMap f₁ (proj₂ x)) + -- F_T Functor A Kleisli + -- F_T FObj = λ a₁ → a₁ FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x } +
--- a/src/monoidal.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/monoidal.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,11 +1,15 @@ +-- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + open import Level open import Category module monoidal where + open import Data.Product renaming (_×_ to _*_) open import Category.Constructions.Product open import HomReasoning -open import cat-utility +open import Definitions open import Relation.Binary.Core open import Relation.Binary @@ -288,13 +292,13 @@ ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f) (proj₂ f) ; isFunctor = record { ≈-cong = ≈-cong - ; identity = refl - ; distr = refl + ; identity = λ {a} x → refl + ; distr = λ {a b c} {f} {g} x → refl } } where ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} → (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ] - ≈-cong (refl , refl) = refl + ≈-cong eq (x , y) = cong₂ _,_ (proj₁ eq x) (proj₂ eq y) ----- -- @@ -313,16 +317,16 @@ m-i = One {c} ; m-bi = SetsTensorProduct ; isMonoidal = record { - mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ; - mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ; - mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ; - mα→nat1 = λ f → refl ; - mα→nat2 = λ f → refl ; - mα→nat3 = λ f → refl ; - mλ→nat = λ f → refl ; - mρ→nat = λ f → refl ; - comm-penta = refl ; - comm-unit = refl + mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = λ _ → refl ; iso← = λ _ → refl } ; + mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = λ x → mλiso x ; iso← = λ x → refl } ; + mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = λ x → mρiso x ; iso← = λ x → refl } ; + mα→nat1 = λ f x → refl ; + mα→nat2 = λ f x → refl ; + mα→nat3 = λ f x → refl ; + mλ→nat = λ f x → refl ; + mρ→nat = λ f x → refl ; + comm-penta = λ x → refl ; + comm-unit = λ x → refl } } where _⊗_ : ( a b : Obj Sets ) → Obj Sets @@ -439,7 +443,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] - comm0 {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x ) + comm0 {a} {b} {f} x = comm00 x comm10 : {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ o Sets [ id1 Sets (FObj F a) □ φ o Iso.≅→ (mα-iso isM) ] ]) x ≡ (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x comm10 {x} {y} {f} ((a , b) , c ) = begin @@ -456,7 +460,7 @@ comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] - comm1 {a} {b} {c} = extensionality Sets ( λ x → comm10 x ) + comm1 {a} {b} {c} x = comm10 x comm20 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x @@ -472,7 +476,7 @@ comm2 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] - comm2 {a} {b} = extensionality Sets ( λ x → comm20 {a} {b} x ) + comm2 {a} {b} x = comm20 {a} {b} x comm30 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x @@ -487,6 +491,6 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] - comm3 {a} {b} = extensionality Sets ( λ x → comm30 {a} {b} x ) + comm3 {a} {b} x = comm30 {a} {b} x -- end
--- a/src/stdalone-kleisli.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/stdalone-kleisli.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} module stdalone-kleisli where open import Level
--- a/src/yoneda.agda Tue Jul 02 08:34:33 2024 +0900 +++ b/src/yoneda.agda Wed Jul 03 11:44:58 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible --safe #-} --- -- -- A → Sets^A^op : Yoneda Functor @@ -76,7 +78,7 @@ o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i -- 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 +-- 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 --- -- @@ -87,7 +89,7 @@ open import Function y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) -y-obj a = Yoneda A (≈-≡ A) a +y-obj a = ? -- Yoneda A (≈-≡ A) a ---- -- @@ -95,8 +97,8 @@ -- ---- -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₂ y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (y-obj a) x → FObj (y-obj b ) x @@ -255,7 +257,7 @@ YonedaIso0 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → Nat2F ( FMap YonedaFunctor f ) ≡ f -YonedaIso0 {a} {a'} {f} = ≈-≡ A (≈-Reasoning.idR A) +YonedaIso0 {a} {a'} {f} = ? -- ≈-≡ A (≈-Reasoning.idR A) YonedaIso1 : {a a' : Obj A } → (ha : Hom SetsAop (y-obj a) (y-obj a')) → SetsAop [ FMap YonedaFunctor (Nat2F {a} ha) ≈ ha ] @@ -290,11 +292,11 @@ _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f f-unique : {a a' b : Obj A } (f : Hom A a a' ) → f ^ ≡ TMap (FMap YonedaFunctor f) b -f-unique {a} {a'} {b} f = extensionality A (λ g → begin - (f ^ ) g ≡⟨⟩ - (FMap (FObj YonedaFunctor a') g) f ≡⟨⟩ - A [ f o g ] ≡⟨⟩ - TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning +f-unique {a} {a'} {b} f = ? -- extensionality A (λ g → begin +-- (f ^ ) g ≡⟨⟩ +-- (FMap (FObj YonedaFunctor a') g) f ≡⟨⟩ +-- A [ f o g ] ≡⟨⟩ +-- TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning f-u : {a a' b : Obj A } (f : FObj (FObj YonedaFunctor a') a ) → Sets [ f ^ ≈ TMap (FMap YonedaFunctor f ) b ] f-u = ? -- f-unique @@ -372,13 +374,13 @@ → f ~ g → b ≡ b' ≃→b=b f g (~refl eqv) = refl -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- -- if Hom A a a ≡ Hom A a b, b must be a cod of id1 A a, so a ≡ b -- -postulate -- ? - ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b +--postulate -- ? +-- ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b -- Obj : Set c₂ -- Hom : Obj → Obj → Set c₂ @@ -386,7 +388,7 @@ -- cod {a} {b} _ = b Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b -Yoneda-full-embed {a} {b} eq = ylem0 ylem1 where +Yoneda-full-embed {a} {b} eq = ? where -- ylem0 ylem1 where ylem1 : Hom A a a ≡ Hom A a b ylem1 = cong (λ k → FObj k a) eq