From 7cbaf996f1973f61a171a73991e77a752bf578b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 1 May 2018 18:54:08 +0200 Subject: [PATCH] Use implicit arguments for fun and profit --- src/Cat/Categories/Cat.agda | 4 +- src/Cat/Category/Monad.agda | 38 +++++++++--------- src/Cat/Category/Monad/Kleisli.agda | 3 +- src/Cat/Category/Monad/Monoidal.agda | 30 +++++++++----- src/Cat/Category/Product.agda | 59 ++++++++++++++-------------- 5 files changed, 74 insertions(+), 60 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index a24abc8..de9b2ff 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -315,8 +315,8 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where exponent : Exponential Catℓ ℂ 𝔻 exponent = record { obj = CatExp.object - ; eval = eval - ; isExponential = isExponential + ; eval = {!eval!} + ; isExponential = {!isExponential!} } hasExponentials : HasExponentials Catℓ diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 63fbab7..e071d92 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -69,20 +69,22 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where M.RawMonad.joinNT backRaw = joinNT private - open M.RawMonad backRaw + open M.RawMonad backRaw renaming + ( join to join* + ; pure to pure* + ; bind to bind* + ; fmap to fmap* + ) module R = Functor (M.RawMonad.R backRaw) backIsMonad : M.IsMonad backRaw - M.IsMonad.isAssociative backIsMonad {X} = begin - joinT X <<< R.fmap (joinT X) ≡⟨⟩ - join <<< fmap (joinT X) ≡⟨⟩ - join <<< fmap join ≡⟨ isNaturalForeign ⟩ - join <<< join ≡⟨⟩ - joinT X <<< joinT (R.omap X) ∎ + M.IsMonad.isAssociative backIsMonad = begin + join* <<< R.fmap join* ≡⟨⟩ + join <<< fmap join ≡⟨ isNaturalForeign ⟩ + join <<< join ∎ M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r where inv-l = begin - joinT X <<< pureT (R.omap X) ≡⟨⟩ join <<< pure ≡⟨ fst isInverse ⟩ identity ∎ inv-r = begin @@ -140,7 +142,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f bindEq {X} {Y} {f} = begin KM.bind f ≡⟨⟩ - joinT Y <<< Rfmap f ≡⟨⟩ + joinT Y <<< fmap f ≡⟨⟩ bind f ∎ joinEq : ∀ {X} → KM.join ≡ joinT X @@ -148,21 +150,21 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where KM.join ≡⟨⟩ KM.bind identity ≡⟨⟩ bind identity ≡⟨⟩ - joinT X <<< Rfmap identity ≡⟨ cong (λ φ → _ <<< φ) R.isIdentity ⟩ + joinT X <<< fmap identity ≡⟨ cong (λ φ → _ <<< φ) R.isIdentity ⟩ joinT X <<< identity ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎ - fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap + fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ fmap fmapEq {A} {B} = funExt (λ f → begin KM.fmap f ≡⟨⟩ KM.bind (f >>> KM.pure) ≡⟨⟩ bind (f >>> pureT _) ≡⟨⟩ - Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩ - Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ - Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ - joinT B <<< Rfmap (pureT B) <<< Rfmap f ≡⟨ cong (λ φ → φ <<< Rfmap f) (snd isInverse) ⟩ - identity <<< Rfmap f ≡⟨ ℂ.leftIdentity ⟩ - Rfmap f ∎ + fmap (f >>> pureT B) >>> joinT B ≡⟨⟩ + fmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ + fmap f >>> fmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ + joinT B <<< fmap (pureT B) <<< fmap f ≡⟨ cong (λ φ → φ <<< fmap f) (snd isInverse) ⟩ + identity <<< fmap f ≡⟨ ℂ.leftIdentity ⟩ + fmap f ∎ ) rawEq : Functor.raw KM.R ≡ Functor.raw R @@ -183,7 +185,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where joinTEq = funExt (λ X → begin M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩ KM.join ≡⟨⟩ - joinT X <<< Rfmap identity ≡⟨ cong (λ φ → joinT X <<< φ) R.isIdentity ⟩ + joinT X <<< fmap identity ≡⟨ cong (λ φ → joinT X <<< φ) R.isIdentity ⟩ joinT X <<< identity ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎) diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index bdb4966..75e5a22 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -57,7 +57,8 @@ record RawMonad : Set ℓ where IsNatural = {X Y : Object} (f : ℂ [ X , omap Y ]) → pure >=> f ≡ f -- Composition interacts with bind in the following way. - IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ]) + IsDistributive = {X Y Z : Object} + (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ]) → (bind f) >>> (bind g) ≡ bind (f >=> g) RightIdentity = {A B : Object} {m : ℂ [ A , omap B ]} diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index fdd739e..86111b6 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -26,35 +26,45 @@ record RawMonad : Set ℓ where pureNT : NaturalTransformation Functors.identity R joinNT : NaturalTransformation F[ R ∘ R ] R + Romap = Functor.omap R + fmap = Functor.fmap R + -- Note that `pureT` and `joinT` differs from their definition in the -- kleisli formulation only by having an explicit parameter. pureT : Transformation Functors.identity R pureT = fst pureNT + + pure : {X : Object} → ℂ [ X , Romap X ] + pure = pureT _ + pureN : Natural Functors.identity R pureT pureN = snd pureNT joinT : Transformation F[ R ∘ R ] R joinT = fst joinNT + join : {X : Object} → ℂ [ Romap (Romap X) , Romap X ] + join = joinT _ joinN : Natural F[ R ∘ R ] R joinT joinN = snd joinNT - Romap = Functor.omap R - Rfmap = Functor.fmap R - bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ] - bind {X} {Y} f = joinT Y <<< Rfmap f + bind {X} {Y} f = join <<< fmap f IsAssociative : Set _ IsAssociative = {X : Object} - → joinT X <<< Rfmap (joinT X) ≡ joinT X <<< joinT (Romap X) + -- R and join commute + → joinT X <<< fmap join ≡ join <<< join IsInverse : Set _ IsInverse = {X : Object} - → joinT X <<< pureT (Romap X) ≡ identity - × joinT X <<< Rfmap (pureT X) ≡ identity - IsNatural = ∀ {X Y} f → joinT Y <<< Rfmap f <<< pureT X ≡ f + -- Talks about R's action on objects + → join <<< pure ≡ identity {Romap X} + -- Talks about R's action on arrows + × join <<< fmap pure ≡ identity {Romap X} + IsNatural = ∀ {X Y} (f : Arrow X (Romap Y)) + → join <<< fmap f <<< pure ≡ f IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y)) - → joinT Z <<< Rfmap g <<< (joinT Y <<< Rfmap f) - ≡ joinT Z <<< Rfmap (joinT Z <<< Rfmap g <<< f) + → join <<< fmap g <<< (join <<< fmap f) + ≡ join <<< fmap (join <<< fmap g <<< f) record IsMonad (raw : RawMonad) : Set ℓ where open RawMonad raw public diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 0d36004..c0c68c3 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -276,7 +276,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} open Σ uy renaming (fst to Y→X ; snd to contractible) open Σ Y→X renaming (fst to p0×p1 ; snd to cond) ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1) - ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → fst (k i) + ump = p0×p1 , cond , λ {f} cond-f → cong fst (contractible (f , cond-f)) isP : IsProduct ℂ 𝒜 ℬ rawP isP = record { ump = ump } p : Product ℂ 𝒜 ℬ @@ -285,42 +285,43 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} ; isProduct = isP } g : Product ℂ 𝒜 ℬ → Terminal - g p = o , t + g p = 𝒳 , t where + open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using () module p = Product p module isp = IsProduct p.isProduct - o : Object - o = p.object , p.fst , p.snd - module _ {Xx : Object} where - open Σ Xx renaming (fst to X ; snd to x) - ℂXo : ℂ [ X , isp.object ] - ℂXo = isp._P[_×_] (fst x) (snd x) - ump = p.ump (fst x) (snd x) - Xoo = fst (snd ump) - Xo : Arrow Xx o - Xo = ℂXo , Xoo - contractible : ∀ y → Xo ≡ y - contractible (y , yy) = res + 𝒳 : Object + 𝒳 = X , x₀ , x₁ + module _ {𝒴 : Object} where + open Σ 𝒴 renaming (fst to Y) + open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁) + ump = p.ump y₀ y₁ + open Σ ump renaming (fst to f') + open Σ (snd ump) renaming (fst to f'-cond) + 𝒻 : Arrow 𝒴 𝒳 + 𝒻 = f' , {!f'-cond!} + contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f + contractible ff@(f , f-cond) = res where - k : ℂXo ≡ y - k = snd (snd ump) (yy) - prp : ∀ a → isProp - ( (ℂ [ p.fst ∘ a ] ≡ fst x) - × (ℂ [ p.snd ∘ a ] ≡ snd x) + k : f' ≡ f + k = snd (snd ump) f-cond + prp : (a : ℂ.Arrow Y X) → isProp + ( (ℂ [ x₀ ∘ a ] ≡ y₀) + × (ℂ [ x₁ ∘ a ] ≡ y₁) ) - prp ab ac ad i - = ℂ.arrowsAreSets _ _ (fst ac) (fst ad) i - , ℂ.arrowsAreSets _ _ (snd ac) (snd ad) i + prp f f0 f1 = Σ≡ + (ℂ.arrowsAreSets _ _ (fst f0) (fst f1)) + (ℂ.arrowsAreSets _ _ (snd f0) (snd f1)) h : ( λ i - → ℂ [ p.fst ∘ k i ] ≡ fst x - × ℂ [ p.snd ∘ k i ] ≡ snd x - ) [ Xoo ≡ yy ] + → ℂ [ x₀ ∘ k i ] ≡ y₀ + × ℂ [ x₁ ∘ k i ] ≡ y₁ + ) [ f'-cond ≡ f-cond ] h = lemPropF prp k - res : (ℂXo , Xoo) ≡ (y , yy) - res i = k i , h i - t : IsTerminal o - t {Xx} = Xo , contractible + res : (f' , f'-cond) ≡ (f , f-cond) + res = Σ≡ k h + t : IsTerminal 𝒳 + t {𝒴} = 𝒻 , contractible ve-re : ∀ x → g (f x) ≡ x ve-re x = Propositionality.propTerminal _ _ re-ve : ∀ p → f (g p) ≡ p