From c75a1d5d8b4ad52866d9ff34ec2d885facbce15f Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Tue, 15 May 2018 17:21:57 +0200 Subject: [PATCH] commented out code with holes --- src/Cat/Categories/Fun.agda | 139 +++++++++++++------------- src/Cat/Category.agda | 2 +- src/Cat/Category/Monad/Voevodsky.agda | 1 + src/Cat/Category/Product.agda | 3 +- 4 files changed, 74 insertions(+), 71 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index eb861e7..9a732f4 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,6 +1,7 @@ {-# OPTIONS --allow-unsolved-metas --cubical --caching #-} module Cat.Categories.Fun where + open import Cat.Prelude open import Cat.Equivalence @@ -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))) - -- 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 + -- 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))) + -- -- 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 } + -- 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 → ?!} , {!!} - - iso : (A ≡ B) ≅ (A ≊ B) - iso = f , g , inv + -- 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 univ : (A ≡ B) ≃ (A ≊ B) univ = fromIsomorphism _ _ iso diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 274f94e..ed453c2 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -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 diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index abc8438..0ad3d90 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -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 diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 4856668..2cf55ed 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -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 ]