From 56d689fb4b9f2b2b0cdc8593d4c23856ee013d6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 7 Feb 2018 20:19:17 +0100 Subject: [PATCH 1/6] Use `arrowIsSet` to simplify equality constructor for functors --- src/Cat/Categories/Fun.agda | 17 +++++++++++++--- src/Cat/Category.agda | 37 ++++++++++++++++++++++++++++------- src/Cat/Category/Functor.agda | 21 +++++++++----------- 3 files changed, 53 insertions(+), 22 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index e60a118..4b1b001 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Categories.Fun where open import Agda.Primitive @@ -9,6 +9,9 @@ open import Data.Product open import Cat.Category open import Cat.Category.Functor +open import Cat.Equality +open Equality.Data.Product + module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where open Category hiding ( _∘_ ; Arrow ) open Functor @@ -86,12 +89,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat NatComp = _:⊕:_ private + module _ {F G : Functor ℂ 𝔻} where + naturalTransformationIsSets : IsSet (NaturalTransformation F G) + naturalTransformationIsSets {θ , θNat} {η , ηNat} p q i j + = (λ C → 𝔻.arrowIsSet (λ l → proj₁ (p l) C) (λ l → proj₁ (q l) C) i j) + , λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f {!!}) (λ l → proj₂ (p l) f {!!}) {!!} {!!} + where + module 𝔻 = IsCategory (isCategory 𝔻) + module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B} {g : NaturalTransformation B C} {h : NaturalTransformation C D} where _g⊕f_ = _:⊕:_ {A} {B} {C} _h⊕g_ = _:⊕:_ {B} {C} {D} :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f) - :assoc: = {!!} + :assoc: = Σ≡ (funExt λ x → {!Fun.arrowIsSet!}) {!!} module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f ident-r = {!!} @@ -116,7 +127,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat :isCategory: = record { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D} ; ident = λ {A B} → :ident: {A} {B} - ; arrowIsSet = {!!} + ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G} ; univalent = {!!} } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 168b2fc..a8a39de 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -26,6 +26,10 @@ syntax ∃!-syntax (λ x → B) = ∃![ x ] B IsSet : {ℓ : Level} (A : Set ℓ) → Set ℓ IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q +-- This follows from [HoTT-book: §7.1.10] +-- Andrea says the proof is in `cubical` but I can't find it. +postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (IsSet A) + record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where -- adding no-eta-equality can speed up type-checking. -- ONLY IF you define your categories with copatterns though. @@ -53,6 +57,7 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where -- (univalent). record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where open RawCategory ℂ + module Raw = RawCategory ℂ field assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D } → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f @@ -91,22 +96,40 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where -- This lemma will be useful to prove the equality of two categories. IsCategory-is-prop : isProp (IsCategory ℂ) IsCategory-is-prop x y i = record + -- Why choose `x`'s `arrowIsSet`? { assoc = x.arrowIsSet x.assoc y.assoc i ; ident = ( x.arrowIsSet (fst x.ident) (fst y.ident) i , x.arrowIsSet (snd x.ident) (snd y.ident) i ) - ; arrowIsSet = λ p q → - let - golden : x.arrowIsSet p q ≡ y.arrowIsSet p q - golden = {!!} - in - golden i - ; univalent = λ y₁ → {!!} + ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i + ; univalent = {!!} } where module x = IsCategory x module y = IsCategory y + xuni : x.Univalent + xuni = x.univalent + yuni : y.Univalent + yuni = y.univalent + open RawCategory ℂ + T : I → Set (ℓa ⊔ ℓb) + T i = {A B : Object} → + isEquiv (A ≡ B) (A x.≅ B) + (λ A≡B → + transp + (λ j → + Σ-syntax (Arrow A (A≡B j)) + (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙))) + ( 𝟙 + , 𝟙 + , x.arrowIsSet (fst x.ident) (fst y.ident) i + , x.arrowIsSet (snd x.ident) (snd y.ident) i + ) + ) + eqUni : T [ xuni ≡ yuni ] + eqUni = {!!} + record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where field diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 8097071..726f56f 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical #-} module Cat.Category.Functor where open import Agda.Primitive @@ -78,14 +79,11 @@ module _ IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ] - postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) - -- IsFunctorIsProp' isF0 isF1 i = record - -- { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!} - -- ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!} - -- } - -- where - -- module isF0 = IsFunctor isF0 - -- module isF1 = IsFunctor isF1 + IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) + IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} + (\ F → IsFunctorIsProp {F = F}) (\ i → F i) + where + open import Cubical.GradLemma using (lemPropF) module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where Functor≡ : {F G : Functor ℂ 𝔻} @@ -95,14 +93,13 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where → F ≡ G Functor≡ {F} {G} eq* eq→ i = record { raw = eqR i - ; isFunctor = f i + ; isFunctor = eqIsF i } where eqR : raw F ≡ raw G eqR i = record { func* = eq* i ; func→ = eq→ i } - postulate T : isSet (IsFunctor _ _ (raw F)) - f : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ] - f = IsFunctorIsProp' (isFunctor F) (isFunctor G) + eqIsF : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ] + eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G) module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private From 7d4aae4f49f15ad5499f4327fb4f64c76fa296ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 9 Feb 2018 12:09:59 +0100 Subject: [PATCH 2/6] Try to show that natural transformations are sets --- src/Cat/Categories/Free.agda | 2 +- src/Cat/Categories/Fun.agda | 72 ++++++++++++++++++++++++++++++----- src/Cat/Category.agda | 19 ++++----- src/Cat/Category/Functor.agda | 6 +-- src/Cat/Equality.agda | 26 +++++++++++++ 5 files changed, 100 insertions(+), 25 deletions(-) diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 16b37c0..703a7d2 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -44,7 +44,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where -- ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p -- ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p module _ {A B : Object ℂ} where - isSet : IsSet (Path A B) + isSet : Cubical.isSet (Path A B) isSet = {!!} RawFree : RawCategory ℓ (ℓ ⊔ ℓ') RawFree = record diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 4b1b001..4ae4251 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -5,6 +5,7 @@ open import Agda.Primitive open import Cubical open import Function open import Data.Product +import Cubical.GradLemma open import Cat.Category open import Cat.Category.Functor @@ -30,6 +31,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat → (f : ℂ [ A , B ]) → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ] + -- naturalIsProp : ∀ θ → isProp (Natural θ) + -- naturalIsProp θ x y = {!funExt!} + NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') NaturalTransformation = Σ Transformation Natural @@ -90,19 +94,67 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat private module _ {F G : Functor ℂ 𝔻} where - naturalTransformationIsSets : IsSet (NaturalTransformation F G) - naturalTransformationIsSets {θ , θNat} {η , ηNat} p q i j - = (λ C → 𝔻.arrowIsSet (λ l → proj₁ (p l) C) (λ l → proj₁ (q l) C) i j) - , λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f {!!}) (λ l → proj₂ (p l) f {!!}) {!!} {!!} - where - module 𝔻 = IsCategory (isCategory 𝔻) + module 𝔻 = IsCategory (isCategory 𝔻) - module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B} - {g : NaturalTransformation B C} {h : NaturalTransformation C D} where + transformationIsSet : isSet (Transformation F G) + transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j + IsSet' : {ℓ : Level} (A : Set ℓ) → Set ℓ + IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q + + -- Example 3.1.6. in HoTT states that + -- If `B a` is a set for all `a : A` then `(a : A) → B a` is a set. + -- In the case below `B = Natural F G`. + + -- naturalIsSet : (θ : Transformation F G) → IsSet' (Natural F G θ) + -- naturalIsSet = {!!} + + -- isS : IsSet' ((θ : Transformation F G) → Natural F G θ) + -- isS = {!!} + + naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ) + naturalIsProp θ θNat θNat' = lem + where + lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] + lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i + + naturalTransformationIsSets : isSet (NaturalTransformation F G) + naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j + = θ-η + -- `i or `j - `p'` or `q'`? + , refl {x = t} i + -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j + -- naturalIsSet {!p''!} {!p''!} {!!} i j + -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!} + where + θ≡η θ≡η' : θ ≡ η + θ≡η i = proj₁ (p i) + θ≡η' i = proj₁ (q i) + θ-η : Transformation F G + θ-η = transformationIsSet _ _ θ≡η θ≡η' i j + θNat≡ηNat : (λ i → Natural F G (θ≡η i)) [ θNat ≡ ηNat ] + θNat≡ηNat i = proj₂ (p i) + θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ] + θNat≡ηNat' i = proj₂ (q i) + k : Natural F G (θ≡η i) + k = θNat≡ηNat i + k' : Natural F G (θ≡η' i) + k' = θNat≡ηNat' i + t : Natural F G θ-η + t = naturalIsProp {!θ!} {!!} {!!} {!!} + + module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} + {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where + private + θ = proj₁ θ' + η = proj₁ η' + ζ = proj₁ ζ' _g⊕f_ = _:⊕:_ {A} {B} {C} _h⊕g_ = _:⊕:_ {B} {C} {D} - :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f) - :assoc: = Σ≡ (funExt λ x → {!Fun.arrowIsSet!}) {!!} + :assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ') + :assoc: = Σ≡ (funExt (λ _ → assoc)) {!!} + where + open IsCategory (isCategory 𝔻) + module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f ident-r = {!!} diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index a8a39de..f1badc3 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -11,7 +11,7 @@ open import Data.Product renaming ) open import Data.Empty import Function -open import Cubical hiding (isSet) +open import Cubical open import Cubical.GradLemma using ( propIsEquiv ) ∃! : ∀ {a b} {A : Set a} @@ -23,12 +23,9 @@ open import Cubical.GradLemma using ( propIsEquiv ) syntax ∃!-syntax (λ x → B) = ∃![ x ] B -IsSet : {ℓ : Level} (A : Set ℓ) → Set ℓ -IsSet A = {x y : A} → (p q : x ≡ y) → p ≡ q - -- This follows from [HoTT-book: §7.1.10] -- Andrea says the proof is in `cubical` but I can't find it. -postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (IsSet A) +postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A) record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where -- adding no-eta-equality can speed up type-checking. @@ -63,7 +60,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f ident : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f - arrowIsSet : ∀ {A B : Object} → IsSet (Arrow A B) + arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B) Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙 @@ -97,10 +94,10 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where IsCategory-is-prop : isProp (IsCategory ℂ) IsCategory-is-prop x y i = record -- Why choose `x`'s `arrowIsSet`? - { assoc = x.arrowIsSet x.assoc y.assoc i + { assoc = x.arrowIsSet _ _ x.assoc y.assoc i ; ident = - ( x.arrowIsSet (fst x.ident) (fst y.ident) i - , x.arrowIsSet (snd x.ident) (snd y.ident) i + ( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i + , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i ) ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i ; univalent = {!!} @@ -123,8 +120,8 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙))) ( 𝟙 , 𝟙 - , x.arrowIsSet (fst x.ident) (fst y.ident) i - , x.arrowIsSet (snd x.ident) (snd y.ident) i + , x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i + , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i ) ) eqUni : T [ xuni ≡ yuni ] diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 726f56f..bf5afed 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -61,14 +61,14 @@ module _ IsFunctorIsProp : isProp (IsFunctor _ _ F) IsFunctorIsProp isF0 isF1 i = record - { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i - ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i + { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i + ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i } where module isF0 = IsFunctor isF0 module isF1 = IsFunctor isF1 --- Alternate version of above where `F` is a path in +-- Alternate version of above where `F` is indexed by an interval module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda index bf94143..c3c333d 100644 --- a/src/Cat/Equality.agda +++ b/src/Cat/Equality.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical #-} -- Defines equality-principles for data-types from the standard library. module Cat.Equality where @@ -19,3 +20,28 @@ module Equality where Σ≡ : a ≡ b proj₁ (Σ≡ i) = proj₁≡ i proj₂ (Σ≡ i) = proj₂≡ i + + -- Remark 2.7.1: This theorem: + -- + -- (x , u) ≡ (x , v) → u ≡ v + -- + -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x` + -- such that + -- + -- p* u ≡ v + -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B) + -- thm sA sB (x , y) (x' , y') p q = res + -- where + -- x≡x'0 : x ≡ x' + -- x≡x'0 = λ i → proj₁ (p i) + -- x≡x'1 : x ≡ x' + -- x≡x'1 = λ i → proj₁ (q i) + -- someP : x ≡ x' + -- someP = {!!} + -- tricky : {!y!} ≡ y' + -- tricky = {!!} + -- -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ] + -- res' : ({!!} , {!!}) ≡ ({!!} , {!!}) + -- res' = {!!} + -- res : p ≡ q + -- res i = {!res'!} From ad84b15da5478abc926272651cf49b298f3b5f51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 16 Feb 2018 10:22:46 +0100 Subject: [PATCH 3/6] [WIP] natural transformations are sets --- src/Cat/Categories/Fun.agda | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 4ae4251..4d32e47 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -6,6 +6,7 @@ open import Cubical open import Function open import Data.Product import Cubical.GradLemma +module UIP = Cubical.GradLemma open import Cat.Category open import Cat.Category.Functor @@ -117,11 +118,29 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i - naturalTransformationIsSets : isSet (NaturalTransformation F G) + naturalTransformationIsSets f : isSet (NaturalTransformation F G) + f a b p q i = res + where + k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy + k θ x y = let kk = naturalIsProp θ x y in {!!} + res : a ≡ b + res j = {!!} , {!!} + -- naturalTransformationIsSets σa σb p q + -- where + -- -- In Andrea's proof `lemSig` he proves something very similiar to + -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather + -- -- than `Σ`. In that proof, he just needs *one* proof that the first + -- -- components are equal - hence the arbitrary usage of `p` here. + -- secretSauce : proj₁ σa ≡ proj₁ σb + -- secretSauce i = proj₁ (p i) + -- lemSig : σa ≡ σb + -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i + -- res : p ≡ q + -- res = {!!} naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j = θ-η -- `i or `j - `p'` or `q'`? - , refl {x = t} i + , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} i -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j -- naturalIsSet {!p''!} {!p''!} {!!} i j -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!} From 8a3a5199556fda2709c70ca9a247091c479c6c13 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 16 Feb 2018 10:25:33 +0100 Subject: [PATCH 4/6] Do not use `depend`-flag --- cat.agda-lib | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/cat.agda-lib b/cat.agda-lib index fa6c713..32833fd 100644 --- a/cat.agda-lib +++ b/cat.agda-lib @@ -2,11 +2,13 @@ name: cat -- version: 0.0.1 -- description: -- A formalization of category theory in Agda using cubical type theory. -depend: - standard-library - cubical +-- depend: +-- standard-library +-- cubical include: src + libs/agda-stdlib/src + libs/cubical/src -- libraries: -- libs/agda-stdlib -- libs/cubical From 23c458983c36b6df7f7f13ec72313cecb5c8e3ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 16 Feb 2018 11:36:44 +0100 Subject: [PATCH 5/6] Rely on global `cubical` again --- cat.agda-lib | 8 ++-- libs/agda-stdlib | 2 +- libs/cubical | 2 +- src/Cat/Categories/Fun.agda | 86 ++++++++++++++++++----------------- src/Cat/Category.agda | 2 +- src/Cat/Category/Functor.agda | 2 +- 6 files changed, 51 insertions(+), 51 deletions(-) diff --git a/cat.agda-lib b/cat.agda-lib index 32833fd..fa6c713 100644 --- a/cat.agda-lib +++ b/cat.agda-lib @@ -2,13 +2,11 @@ name: cat -- version: 0.0.1 -- description: -- A formalization of category theory in Agda using cubical type theory. --- depend: --- standard-library --- cubical +depend: + standard-library + cubical include: src - libs/agda-stdlib/src - libs/cubical/src -- libraries: -- libs/agda-stdlib -- libs/cubical diff --git a/libs/agda-stdlib b/libs/agda-stdlib index b5bfbc3..157497a 160000 --- a/libs/agda-stdlib +++ b/libs/agda-stdlib @@ -1 +1 @@ -Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6 +Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68 diff --git a/libs/cubical b/libs/cubical index 1d6730c..12c2c62 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48 +Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151 diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 4d32e47..81e656f 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -7,6 +7,7 @@ open import Function open import Data.Product import Cubical.GradLemma module UIP = Cubical.GradLemma +open import Cubical.Sigma open import Cat.Category open import Cat.Category.Functor @@ -118,48 +119,49 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i - naturalTransformationIsSets f : isSet (NaturalTransformation F G) - f a b p q i = res - where - k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy - k θ x y = let kk = naturalIsProp θ x y in {!!} - res : a ≡ b - res j = {!!} , {!!} - -- naturalTransformationIsSets σa σb p q - -- where - -- -- In Andrea's proof `lemSig` he proves something very similiar to - -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather - -- -- than `Σ`. In that proof, he just needs *one* proof that the first - -- -- components are equal - hence the arbitrary usage of `p` here. - -- secretSauce : proj₁ σa ≡ proj₁ σb - -- secretSauce i = proj₁ (p i) - -- lemSig : σa ≡ σb - -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i - -- res : p ≡ q - -- res = {!!} - naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j - = θ-η - -- `i or `j - `p'` or `q'`? - , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} i - -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j - -- naturalIsSet {!p''!} {!p''!} {!!} i j - -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!} - where - θ≡η θ≡η' : θ ≡ η - θ≡η i = proj₁ (p i) - θ≡η' i = proj₁ (q i) - θ-η : Transformation F G - θ-η = transformationIsSet _ _ θ≡η θ≡η' i j - θNat≡ηNat : (λ i → Natural F G (θ≡η i)) [ θNat ≡ ηNat ] - θNat≡ηNat i = proj₂ (p i) - θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ] - θNat≡ηNat' i = proj₂ (q i) - k : Natural F G (θ≡η i) - k = θNat≡ηNat i - k' : Natural F G (θ≡η' i) - k' = θNat≡ηNat' i - t : Natural F G θ-η - t = naturalIsProp {!θ!} {!!} {!!} {!!} + naturalTransformationIsSets : isSet (NaturalTransformation F G) + naturalTransformationIsSets = {!sigPresSet!} + -- f a b p q i = res + -- where + -- k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy + -- k θ x y = let kk = naturalIsProp θ x y in {!!} + -- res : a ≡ b + -- res j = {!!} , {!!} + -- -- naturalTransformationIsSets σa σb p q + -- -- where + -- -- -- In Andrea's proof `lemSig` he proves something very similiar to + -- -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather + -- -- -- than `Σ`. In that proof, he just needs *one* proof that the first + -- -- -- components are equal - hence the arbitrary usage of `p` here. + -- -- secretSauce : proj₁ σa ≡ proj₁ σb + -- -- secretSauce i = proj₁ (p i) + -- -- lemSig : σa ≡ σb + -- -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i + -- -- res : p ≡ q + -- -- res = {!!} + -- naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j + -- = θ-η + -- -- `i or `j - `p'` or `q'`? + -- , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} i + -- -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j + -- -- naturalIsSet {!p''!} {!p''!} {!!} i j + -- -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!} + -- where + -- θ≡η θ≡η' : θ ≡ η + -- θ≡η i = proj₁ (p i) + -- θ≡η' i = proj₁ (q i) + -- θ-η : Transformation F G + -- θ-η = transformationIsSet _ _ θ≡η θ≡η' i j + -- θNat≡ηNat : (λ i → Natural F G (θ≡η i)) [ θNat ≡ ηNat ] + -- θNat≡ηNat i = proj₂ (p i) + -- θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ] + -- θNat≡ηNat' i = proj₂ (q i) + -- k : Natural F G (θ≡η i) + -- k = θNat≡ηNat i + -- k' : Natural F G (θ≡η' i) + -- k' = θNat≡ηNat' i + -- t : Natural F G θ-η + -- t = naturalIsProp {!θ!} {!!} {!!} {!!} module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index f1badc3..cee681f 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -12,7 +12,7 @@ open import Data.Product renaming open import Data.Empty import Function open import Cubical -open import Cubical.GradLemma using ( propIsEquiv ) +open import Cubical.NType.Properties using ( propIsEquiv ) ∃! : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index bf5afed..ff5d659 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -83,7 +83,7 @@ module _ IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} (\ F → IsFunctorIsProp {F = F}) (\ i → F i) where - open import Cubical.GradLemma using (lemPropF) + open import Cubical.NType.Properties using (lemPropF) module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where Functor≡ : {F G : Functor ℂ 𝔻} From 7dc7a5aee37deb41f2c2ebea4b8e023f1a647bc8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 16 Feb 2018 12:03:02 +0100 Subject: [PATCH 6/6] Prove that naturalTransformations are sets Also adds a new module `Cat.Wishlist` of things I hope to put get from upstream `cubical`. --- src/Cat/Categories/Fun.agda | 60 +++++-------------------------------- src/Cat/Wishlist.agda | 6 ++++ 2 files changed, 14 insertions(+), 52 deletions(-) create mode 100644 src/Cat/Wishlist.agda diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 81e656f..522bb34 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -8,9 +8,13 @@ open import Data.Product import Cubical.GradLemma module UIP = Cubical.GradLemma open import Cubical.Sigma +open import Cubical.NType +open import Data.Nat using (_≤_ ; z≤n ; s≤s) +module Nat = Data.Nat open import Cat.Category open import Cat.Category.Functor +open import Cat.Wishlist open import Cat.Equality open Equality.Data.Product @@ -103,16 +107,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat IsSet' : {ℓ : Level} (A : Set ℓ) → Set ℓ IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q - -- Example 3.1.6. in HoTT states that - -- If `B a` is a set for all `a : A` then `(a : A) → B a` is a set. - -- In the case below `B = Natural F G`. - - -- naturalIsSet : (θ : Transformation F G) → IsSet' (Natural F G θ) - -- naturalIsSet = {!!} - - -- isS : IsSet' ((θ : Transformation F G) → Natural F G θ) - -- isS = {!!} - naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ) naturalIsProp θ θNat θNat' = lem where @@ -120,48 +114,10 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i naturalTransformationIsSets : isSet (NaturalTransformation F G) - naturalTransformationIsSets = {!sigPresSet!} - -- f a b p q i = res - -- where - -- k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy - -- k θ x y = let kk = naturalIsProp θ x y in {!!} - -- res : a ≡ b - -- res j = {!!} , {!!} - -- -- naturalTransformationIsSets σa σb p q - -- -- where - -- -- -- In Andrea's proof `lemSig` he proves something very similiar to - -- -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather - -- -- -- than `Σ`. In that proof, he just needs *one* proof that the first - -- -- -- components are equal - hence the arbitrary usage of `p` here. - -- -- secretSauce : proj₁ σa ≡ proj₁ σb - -- -- secretSauce i = proj₁ (p i) - -- -- lemSig : σa ≡ σb - -- -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i - -- -- res : p ≡ q - -- -- res = {!!} - -- naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j - -- = θ-η - -- -- `i or `j - `p'` or `q'`? - -- , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} i - -- -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j - -- -- naturalIsSet {!p''!} {!p''!} {!!} i j - -- -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!} - -- where - -- θ≡η θ≡η' : θ ≡ η - -- θ≡η i = proj₁ (p i) - -- θ≡η' i = proj₁ (q i) - -- θ-η : Transformation F G - -- θ-η = transformationIsSet _ _ θ≡η θ≡η' i j - -- θNat≡ηNat : (λ i → Natural F G (θ≡η i)) [ θNat ≡ ηNat ] - -- θNat≡ηNat i = proj₂ (p i) - -- θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ] - -- θNat≡ηNat' i = proj₂ (q i) - -- k : Natural F G (θ≡η i) - -- k = θNat≡ηNat i - -- k' : Natural F G (θ≡η' i) - -- k' = θNat≡ηNat' i - -- t : Natural F G θ-η - -- t = naturalIsProp {!θ!} {!!} {!!} {!!} + naturalTransformationIsSets = sigPresSet transformationIsSet + λ θ → ntypeCommulative + (s≤s {n = Nat.suc Nat.zero} z≤n) + (naturalIsProp θ) module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda new file mode 100644 index 0000000..2e56a27 --- /dev/null +++ b/src/Cat/Wishlist.agda @@ -0,0 +1,6 @@ +module Cat.Wishlist where + +open import Cubical.NType +open import Data.Nat using (_≤_ ; z≤n ; s≤s) + +postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A