More readable goal for voevodsky's construction

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-13 11:29:13 +01:00
parent 3ab88395dc
commit 7065455712
2 changed files with 35 additions and 14 deletions

View file

@ -1,13 +1,14 @@
Backlog Backlog
======= =======
Prove postulates in `Cat.Wishlist` Prove postulates in `Cat.Wishlist`:
`ntypeCommulative` might be there as well. * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A`
Prove that the opposite category is a category.
Prove univalence for the category of Prove univalence for the category of
* the opposite category
* sets * sets
This does not follow trivially from `Cubical.Univalence.univalence` because
objects are not `Set` but `hSet`
* functors and natural transformations * functors and natural transformations
Prove: Prove:
@ -24,7 +25,10 @@ Prove:
* Monad * Monad
* Monoidal monad ✓ * Monoidal monad ✓
* Kleisli monad ✓ * Kleisli monad ✓
* Problem 2.3 in voe * Kleisli ≃ Monoidal ✓
* Problem 2.3 in [voe]
* 1st contruction ~ monoidal ✓ * 1st contruction ~ monoidal ✓
* 2nd contruction ~ klesli ✓ * 2nd contruction ~ klesli ✓
* 1st ≃ 2nd ✗ * 1st ≃ 2nd ✗
I've managed to set this up so I should be able to reuse the proof that
Kleisli ≃ Monoidal, but I don't know why it doesn't typecheck.

View file

@ -7,6 +7,7 @@ module Cat.Category.Monad.Voevodsky where
open import Agda.Primitive open import Agda.Primitive
open import Data.Product open import Data.Product
open import Function using (_∘_ ; _$_)
open import Cubical open import Cubical
open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP)
@ -20,13 +21,26 @@ import Cat.Category.Monad.Monoidal as Monoidal
import Cat.Category.Monad.Kleisli as Kleisli import Cat.Category.Monad.Kleisli as Kleisli
open import Cat.Categories.Fun open import Cat.Categories.Fun
-- Utilities
module _ {a b : Level} {A : Set a} {B : Set b} where
module _ (e : A B) where
obverse : A B
obverse = proj₁ e
reverse : B A
reverse = inverse e
-- TODO Implement and push upstream.
postulate
verso-recto : reverse obverse Function.id
recto-verso : obverse reverse Function.id
module voe {a b : Level} ( : Category a b) where module voe {a b : Level} ( : Category a b) where
private private
= a b = a b
module = Category module = Category
open using (Object ; Arrow) open using (Object ; Arrow)
open NaturalTransformation open NaturalTransformation
open import Function using (_∘_ ; _$_)
module M = Monoidal module M = Monoidal
module K = Kleisli module K = Kleisli
@ -162,7 +176,7 @@ module voe {a b : Level} ( : Category a b) where
Monoidal→Kleisli Monoidal→Kleisli
Kleisli→Monoidal Kleisli→Monoidal
§2-3.§2.toMonad §2-3.§2.toMonad
) m ≡⟨ u ) m ≡⟨ cong (λ φ φ m) t
-- Monoidal→Kleisli and Kleisli→Monoidal are inverses -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-- I should be able to prove this using congruence and `lem` below. -- I should be able to prove this using congruence and `lem` below.
( §2-fromMonad ( §2-fromMonad
@ -173,14 +187,12 @@ module voe {a b : Level} ( : Category a b) where
) m ≡⟨⟩ -- fromMonad and toMonad are inverses ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m m
where where
lem : Monoidal→Kleisli Kleisli→Monoidal Function.id ve-re : Monoidal→Kleisli Kleisli→Monoidal Function.id
lem = {!!} -- verso-recto Monoidal≃Kleisli ve-re = recto-verso Monoidal≃Kleisli
t : (§2-fromMonad (Monoidal→Kleisli Kleisli→Monoidal) §2-3.§2.toMonad) t : (§2-fromMonad (Monoidal→Kleisli Kleisli→Monoidal) §2-3.§2.toMonad)
(§2-fromMonad §2-3.§2.toMonad) (§2-fromMonad §2-3.§2.toMonad)
t = cong (λ φ §2-fromMonad (λ{ {ω} φ {{!????!}}}) §2-3.§2.toMonad) {!lem!} -- Why can I not give φ in the first hole like I do below in `backEq.t`?
u : (§2-fromMonad (Monoidal→Kleisli Kleisli→Monoidal) §2-3.§2.toMonad) m t = cong (λ φ §2-fromMonad {!φ!} §2-3.§2.toMonad) ve-re
(§2-fromMonad §2-3.§2.toMonad) m
u = cong (λ φ φ m) t
backEq : m (back forth) m m backEq : m (back forth) m m
backEq m = begin backEq m = begin
@ -202,7 +214,12 @@ module voe {a b : Level} ( : Category a b) where
) m ≡⟨⟩ -- fromMonad and toMonad are inverses ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m m
where where
t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli) re-ve : Kleisli→Monoidal Monoidal→Kleisli Function.id
re-ve = verso-recto Monoidal≃Kleisli
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 = cong (λ φ §1-fromMonad φ §2-3.§1.toMonad) ({!re-ve!})
voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
voe-isEquiv = gradLemma forth back forthEq backEq voe-isEquiv = gradLemma forth back forthEq backEq