Merge remote-tracking branch 'Saizan/benchmark' into dev
This commit is contained in:
commit
d4dc125fb0
|
|
@ -1,6 +1,7 @@
|
|||
{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
|
||||
module Cat.Categories.Fun where
|
||||
|
||||
|
||||
open import Cat.Prelude
|
||||
open import Cat.Equivalence
|
||||
open import Cat.Category
|
||||
|
|
@ -52,14 +53,14 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
|
|||
lem : coe (pp {C}) 𝔻.identity ≡ f→g
|
||||
lem = trans (𝔻.9-1-9-right {b = Functor.omap F C} 𝔻.identity p*) 𝔻.rightIdentity
|
||||
|
||||
idToNatTrans : NaturalTransformation F G
|
||||
idToNatTrans = (λ C → coe pp 𝔻.identity) , λ f → begin
|
||||
coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem ⟩
|
||||
-- Just need to show that f→g is a natural transformation
|
||||
-- I know that it has an inverse; g→f
|
||||
f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!} ⟩
|
||||
G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem) ⟩
|
||||
G.fmap f 𝔻.<<< coe pp 𝔻.identity ∎
|
||||
-- idToNatTrans : NaturalTransformation F G
|
||||
-- idToNatTrans = (λ C → coe pp 𝔻.identity) , λ f → begin
|
||||
-- coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem ⟩
|
||||
-- -- Just need to show that f→g is a natural transformation
|
||||
-- -- I know that it has an inverse; g→f
|
||||
-- f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!} ⟩
|
||||
-- G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem) ⟩
|
||||
-- G.fmap f 𝔻.<<< coe pp 𝔻.identity ∎
|
||||
|
||||
module _ {A B : Functor ℂ 𝔻} where
|
||||
module A = Functor A
|
||||
|
|
@ -92,70 +93,70 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
|
|||
U : (F : ℂ.Object → 𝔻.Object) → Set _
|
||||
U F = {A B : ℂ.Object} → ℂ [ A , B ] → 𝔻 [ F A , F B ]
|
||||
|
||||
module _
|
||||
(omap : ℂ.Object → 𝔻.Object)
|
||||
(p : A.omap ≡ omap)
|
||||
where
|
||||
D : Set _
|
||||
D = ( fmap : U omap)
|
||||
→ ( let
|
||||
raw-B : RawFunctor ℂ 𝔻
|
||||
raw-B = record { omap = omap ; fmap = fmap }
|
||||
)
|
||||
→ (isF-B' : IsFunctor ℂ 𝔻 raw-B)
|
||||
→ ( let
|
||||
B' : Functor ℂ 𝔻
|
||||
B' = record { raw = raw-B ; isFunctor = isF-B' }
|
||||
)
|
||||
→ (iso' : A ≊ B') → PathP (λ i → U (p i)) A.fmap fmap
|
||||
-- D : Set _
|
||||
-- D = PathP (λ i → U (p i)) A.fmap fmap
|
||||
-- eeq : (λ f → A.fmap f) ≡ fmap
|
||||
-- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
|
||||
-- module _
|
||||
-- (omap : ℂ.Object → 𝔻.Object)
|
||||
-- (p : A.omap ≡ omap)
|
||||
-- where
|
||||
-- module _ {X : ℂ.Object} {Y : ℂ.Object} (f : ℂ [ X , Y ]) where
|
||||
-- isofmap : A.fmap f ≡ fmap f
|
||||
-- isofmap = {!ap!}
|
||||
d : D A.omap refl
|
||||
d = res
|
||||
where
|
||||
module _
|
||||
( fmap : U A.omap )
|
||||
( let
|
||||
raw-B : RawFunctor ℂ 𝔻
|
||||
raw-B = record { omap = A.omap ; fmap = fmap }
|
||||
)
|
||||
( isF-B' : IsFunctor ℂ 𝔻 raw-B )
|
||||
( let
|
||||
B' : Functor ℂ 𝔻
|
||||
B' = record { raw = raw-B ; isFunctor = isF-B' }
|
||||
)
|
||||
( iso' : A ≊ B' )
|
||||
where
|
||||
module _ {X Y : ℂ.Object} (f : ℂ [ X , Y ]) where
|
||||
step : {!!} 𝔻.≊ {!!}
|
||||
step = {!!}
|
||||
resres : A.fmap {X} {Y} f ≡ fmap {X} {Y} f
|
||||
resres = {!!}
|
||||
res : PathP (λ i → U A.omap) A.fmap fmap
|
||||
res i {X} {Y} f = resres f i
|
||||
-- D : Set _
|
||||
-- D = ( fmap : U omap)
|
||||
-- → ( let
|
||||
-- raw-B : RawFunctor ℂ 𝔻
|
||||
-- raw-B = record { omap = omap ; fmap = fmap }
|
||||
-- )
|
||||
-- → (isF-B' : IsFunctor ℂ 𝔻 raw-B)
|
||||
-- → ( let
|
||||
-- B' : Functor ℂ 𝔻
|
||||
-- B' = record { raw = raw-B ; isFunctor = isF-B' }
|
||||
-- )
|
||||
-- → (iso' : A ≊ B') → PathP (λ i → U (p i)) A.fmap fmap
|
||||
-- -- D : Set _
|
||||
-- -- D = PathP (λ i → U (p i)) A.fmap fmap
|
||||
-- -- eeq : (λ f → A.fmap f) ≡ fmap
|
||||
-- -- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
|
||||
-- -- where
|
||||
-- -- module _ {X : ℂ.Object} {Y : ℂ.Object} (f : ℂ [ X , Y ]) where
|
||||
-- -- isofmap : A.fmap f ≡ fmap f
|
||||
-- -- isofmap = {!ap!}
|
||||
-- d : D A.omap refl
|
||||
-- d = res
|
||||
-- where
|
||||
-- module _
|
||||
-- ( fmap : U A.omap )
|
||||
-- ( let
|
||||
-- raw-B : RawFunctor ℂ 𝔻
|
||||
-- raw-B = record { omap = A.omap ; fmap = fmap }
|
||||
-- )
|
||||
-- ( isF-B' : IsFunctor ℂ 𝔻 raw-B )
|
||||
-- ( let
|
||||
-- B' : Functor ℂ 𝔻
|
||||
-- B' = record { raw = raw-B ; isFunctor = isF-B' }
|
||||
-- )
|
||||
-- ( iso' : A ≊ B' )
|
||||
-- where
|
||||
-- module _ {X Y : ℂ.Object} (f : ℂ [ X , Y ]) where
|
||||
-- step : {!!} 𝔻.≊ {!!}
|
||||
-- step = {!!}
|
||||
-- resres : A.fmap {X} {Y} f ≡ fmap {X} {Y} f
|
||||
-- resres = {!!}
|
||||
-- res : PathP (λ i → U A.omap) A.fmap fmap
|
||||
-- res i {X} {Y} f = resres f i
|
||||
|
||||
fmapEq : PathP (λ i → U (omapEq i)) A.fmap B.fmap
|
||||
fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
|
||||
-- fmapEq : PathP (λ i → U (omapEq i)) A.fmap B.fmap
|
||||
-- fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
|
||||
|
||||
rawEq : A.raw ≡ B.raw
|
||||
rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
|
||||
|
||||
private
|
||||
f : (A ≡ B) → (A ≊ B)
|
||||
f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C → {!!})) , {!!}
|
||||
g : (A ≊ B) → (A ≡ B)
|
||||
g = Functor≡ ∘ rawEq
|
||||
inv : AreInverses f g
|
||||
inv = {!funExt λ p → ?!} , {!!}
|
||||
-- rawEq : A.raw ≡ B.raw
|
||||
-- rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
|
||||
|
||||
-- private
|
||||
-- f : (A ≡ B) → (A ≊ B)
|
||||
-- f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C → {!!})) , {!!}
|
||||
-- g : (A ≊ B) → (A ≡ B)
|
||||
-- g = Functor≡ ∘ rawEq
|
||||
-- inv : AreInverses f g
|
||||
-- inv = {!funExt λ p → ?!} , {!!}
|
||||
postulate
|
||||
iso : (A ≡ B) ≅ (A ≊ B)
|
||||
iso = f , g , inv
|
||||
-- iso = f , g , inv
|
||||
|
||||
univ : (A ≡ B) ≃ (A ≊ B)
|
||||
univ = fromIsomorphism _ _ iso
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ open Cat.Equivalence
|
|||
-- about these. The laws defined are the types the propositions - not the
|
||||
-- witnesses to them!
|
||||
record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||
no-eta-equality
|
||||
-- no-eta-equality
|
||||
field
|
||||
Object : Set ℓa
|
||||
Arrow : Object → Object → Set ℓb
|
||||
|
|
|
|||
|
|
@ -230,6 +230,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
|
|||
m ∎
|
||||
|
||||
record Monad : Set ℓ where
|
||||
no-eta-equality
|
||||
field
|
||||
raw : RawMonad
|
||||
isMonad : IsMonad raw
|
||||
|
|
|
|||
|
|
@ -122,6 +122,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
|
|||
R.fmap a <<< R.fmap b <<< R.fmap c ∎
|
||||
|
||||
record Monad : Set ℓ where
|
||||
no-eta-equality
|
||||
field
|
||||
raw : RawMonad
|
||||
isMonad : IsMonad raw
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@ This module provides construction 2.3 in [voe]
|
|||
{-# OPTIONS --cubical --caching #-}
|
||||
module Cat.Category.Monad.Voevodsky where
|
||||
|
||||
|
||||
open import Cat.Prelude
|
||||
|
||||
open import Cat.Category
|
||||
|
|
@ -26,6 +27,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
|
||||
module §2-3 (omap : Object → Object) (pure : {X : Object} → Arrow X (omap X)) where
|
||||
record §1 : Set ℓ where
|
||||
no-eta-equality
|
||||
open M
|
||||
|
||||
field
|
||||
|
|
@ -76,12 +78,11 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
isMonad : IsMonad rawMnd
|
||||
|
||||
toMonad : Monad
|
||||
toMonad = record
|
||||
{ raw = rawMnd
|
||||
; isMonad = isMonad
|
||||
}
|
||||
toMonad .Monad.raw = rawMnd
|
||||
toMonad .Monad.isMonad = isMonad
|
||||
|
||||
record §2 : Set ℓ where
|
||||
no-eta-equality
|
||||
open K
|
||||
|
||||
field
|
||||
|
|
@ -98,28 +99,24 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
isMonad : IsMonad rawMnd
|
||||
|
||||
toMonad : Monad
|
||||
toMonad = record
|
||||
{ raw = rawMnd
|
||||
; isMonad = isMonad
|
||||
}
|
||||
toMonad .Monad.raw = rawMnd
|
||||
toMonad .Monad.isMonad = isMonad
|
||||
|
||||
§1-fromMonad : (m : M.Monad) → §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
|
||||
§1-fromMonad m = record
|
||||
{ fmap = Functor.fmap R
|
||||
; RisFunctor = Functor.isFunctor R
|
||||
; pureN = pureN
|
||||
; join = λ {X} → joinT X
|
||||
; joinN = joinN
|
||||
; isMonad = M.Monad.isMonad m
|
||||
}
|
||||
where
|
||||
module _ (m : M.Monad) where
|
||||
open M.Monad m
|
||||
|
||||
§1-fromMonad : §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
|
||||
§1-fromMonad .§2-3.§1.fmap = Functor.fmap R
|
||||
§1-fromMonad .§2-3.§1.RisFunctor = Functor.isFunctor R
|
||||
§1-fromMonad .§2-3.§1.pureN = pureN
|
||||
§1-fromMonad .§2-3.§1.join {X} = joinT X
|
||||
§1-fromMonad .§2-3.§1.joinN = joinN
|
||||
§1-fromMonad .§2-3.§1.isMonad = M.Monad.isMonad m
|
||||
|
||||
|
||||
§2-fromMonad : (m : K.Monad) → §2-3.§2 (K.Monad.omap m) (K.Monad.pure m)
|
||||
§2-fromMonad m = record
|
||||
{ bind = K.Monad.bind m
|
||||
; isMonad = K.Monad.isMonad m
|
||||
}
|
||||
§2-fromMonad m .§2-3.§2.bind = K.Monad.bind m
|
||||
§2-fromMonad m .§2-3.§2.isMonad = K.Monad.isMonad m
|
||||
|
||||
-- | In the following we seek to transform the equivalence `Monoidal≃Kleisli`
|
||||
-- | to talk about voevodsky's construction.
|
||||
|
|
@ -147,64 +144,64 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
|
||||
forthEq : ∀ m → (forth ∘ back) m ≡ m
|
||||
forthEq m = begin
|
||||
(forth ∘ back) m ≡⟨⟩
|
||||
-- In full gory detail:
|
||||
( §2-fromMonad
|
||||
∘ Monoidal→Kleisli
|
||||
∘ §2-3.§1.toMonad
|
||||
∘ §1-fromMonad
|
||||
∘ Kleisli→Monoidal
|
||||
∘ §2-3.§2.toMonad
|
||||
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
|
||||
( §2-fromMonad
|
||||
∘ Monoidal→Kleisli
|
||||
∘ Kleisli→Monoidal
|
||||
∘ §2-3.§2.toMonad
|
||||
) m ≡⟨ cong (λ φ → φ m) t ⟩
|
||||
-- Monoidal→Kleisli and Kleisli→Monoidal are inverses
|
||||
-- I should be able to prove this using congruence and `lem` below.
|
||||
( §2-fromMonad
|
||||
∘ §2-3.§2.toMonad
|
||||
) m ≡⟨⟩
|
||||
( §2-fromMonad
|
||||
∘ §2-3.§2.toMonad
|
||||
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
|
||||
§2-fromMonad
|
||||
(Monoidal→Kleisli
|
||||
(§2-3.§1.toMonad
|
||||
(§1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad m)))))
|
||||
≡⟨ cong-d (§2-fromMonad ∘ Monoidal→Kleisli) (lemmaz (Kleisli→Monoidal (§2-3.§2.toMonad m))) ⟩
|
||||
§2-fromMonad
|
||||
((Monoidal→Kleisli ∘ Kleisli→Monoidal)
|
||||
(§2-3.§2.toMonad m))
|
||||
≡⟨ (cong-d (\ φ → §2-fromMonad (φ (§2-3.§2.toMonad m))) re-ve) ⟩
|
||||
(§2-fromMonad ∘ §2-3.§2.toMonad) m
|
||||
≡⟨ lemma ⟩
|
||||
m ∎
|
||||
where
|
||||
t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
|
||||
≡ §2-3.§2.toMonad
|
||||
t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) re-ve
|
||||
t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
|
||||
≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
|
||||
t = cong-d (\ f → §2-fromMonad ∘ f) t'
|
||||
u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
|
||||
≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
|
||||
u = cong (\ φ → φ m) t
|
||||
lemma : (§2-fromMonad ∘ §2-3.§2.toMonad) m ≡ m
|
||||
§2-3.§2.bind (lemma i) = §2-3.§2.bind m
|
||||
§2-3.§2.isMonad (lemma i) = §2-3.§2.isMonad m
|
||||
lemmaz : ∀ m → §2-3.§1.toMonad (§1-fromMonad m) ≡ m
|
||||
M.Monad.raw (lemmaz m i) = M.Monad.raw m
|
||||
M.Monad.isMonad (lemmaz m i) = M.Monad.isMonad m
|
||||
|
||||
backEq : ∀ m → (back ∘ forth) m ≡ m
|
||||
backEq m = begin
|
||||
(back ∘ forth) m ≡⟨⟩
|
||||
( §1-fromMonad
|
||||
∘ Kleisli→Monoidal
|
||||
∘ §2-3.§2.toMonad
|
||||
∘ §2-fromMonad
|
||||
∘ Monoidal→Kleisli
|
||||
∘ §2-3.§1.toMonad
|
||||
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
|
||||
( §1-fromMonad
|
||||
∘ Kleisli→Monoidal
|
||||
∘ Monoidal→Kleisli
|
||||
∘ §2-3.§1.toMonad
|
||||
) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
|
||||
( §1-fromMonad
|
||||
∘ §2-3.§1.toMonad
|
||||
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
|
||||
§1-fromMonad
|
||||
(Kleisli→Monoidal
|
||||
(§2-3.§2.toMonad
|
||||
(§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
|
||||
≡⟨ cong-d (§1-fromMonad ∘ Kleisli→Monoidal) (lemma (Monoidal→Kleisli (§2-3.§1.toMonad m))) ⟩
|
||||
§1-fromMonad
|
||||
((Kleisli→Monoidal ∘ Monoidal→Kleisli)
|
||||
(§2-3.§1.toMonad m))
|
||||
≡⟨ (cong-d (\ φ → §1-fromMonad (φ (§2-3.§1.toMonad m))) ve-re) ⟩
|
||||
§1-fromMonad (§2-3.§1.toMonad m)
|
||||
≡⟨ lemmaz ⟩
|
||||
m ∎
|
||||
where
|
||||
t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad
|
||||
≡ §1-fromMonad ∘ §2-3.§1.toMonad
|
||||
-- Why does `re-ve` not satisfy this goal?
|
||||
t i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m))
|
||||
-- having eta equality on causes roughly the same work as checking this proof of foo,
|
||||
-- which is quite expensive because it ends up reducing complex terms.
|
||||
|
||||
-- rhs = §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
|
||||
-- foo : §1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad (§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
|
||||
-- ≡ §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
|
||||
-- §2-3.§1.fmap (foo i) = §2-3.§1.fmap rhs
|
||||
-- §2-3.§1.join (foo i) = §2-3.§1.join rhs
|
||||
-- §2-3.§1.RisFunctor (foo i) = §2-3.§1.RisFunctor rhs
|
||||
-- §2-3.§1.pureN (foo i) = §2-3.§1.pureN rhs
|
||||
-- §2-3.§1.joinN (foo i) = §2-3.§1.joinN rhs
|
||||
-- §2-3.§1.isMonad (foo i) = §2-3.§1.isMonad rhs
|
||||
|
||||
lemmaz : §1-fromMonad (§2-3.§1.toMonad m) ≡ m
|
||||
§2-3.§1.fmap (lemmaz i) = §2-3.§1.fmap m
|
||||
§2-3.§1.join (lemmaz i) = §2-3.§1.join m
|
||||
§2-3.§1.RisFunctor (lemmaz i) = §2-3.§1.RisFunctor m
|
||||
§2-3.§1.pureN (lemmaz i) = §2-3.§1.pureN m
|
||||
§2-3.§1.joinN (lemmaz i) = §2-3.§1.joinN m
|
||||
§2-3.§1.isMonad (lemmaz i) = §2-3.§1.isMonad m
|
||||
lemma : ∀ m → §2-3.§2.toMonad (§2-fromMonad m) ≡ m
|
||||
K.Monad.raw (lemma m i) = K.Monad.raw m
|
||||
K.Monad.isMonad (lemma m i) = K.Monad.isMonad m
|
||||
|
||||
voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
|
||||
voe-isEquiv = gradLemma forth back forthEq backEq
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
{-# OPTIONS --cubical --caching #-}
|
||||
module Cat.Category.Product where
|
||||
|
||||
|
||||
open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
|
||||
open import Cat.Equivalence
|
||||
|
||||
|
|
@ -11,7 +12,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
|
||||
module _ (A B : Object) where
|
||||
record RawProduct : Set (ℓa ⊔ ℓb) where
|
||||
no-eta-equality
|
||||
-- no-eta-equality
|
||||
field
|
||||
object : Object
|
||||
fst : ℂ [ object , A ]
|
||||
|
|
|
|||
Loading…
Reference in a new issue