Use implicit arguments for fun and profit
This commit is contained in:
parent
4d27bbb401
commit
7cbaf996f1
|
|
@ -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ℓ
|
||||
|
|
|
|||
|
|
@ -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 ∎)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 ]}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue