diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 6829a3b..5ffde56 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -8,7 +8,7 @@ open import Cat.Category module _ (ℓa ℓb : Level) where private - Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb}) + Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb) Arr : Object → Object → Set (ℓa ⊔ ℓb) Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x))) 𝟙 : {A : Object} → Arr A A diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 75ff8b0..65533a4 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -147,26 +147,47 @@ module _ (ℓ : Level) where Q→P : ∀ {a} → Q a ≡ P a Q→P = sym P→Q f : Σ A P → Σ A Q - f (a , pA) = a , coe P→Q pA + f (a , pA) = a , _≃_.eqv (eA a) pA g : Σ A Q → Σ A P - g (a , qA) = a , coe Q→P qA + g (a , qA) = a , g' qA + where + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g') ve-re : (x : Σ A P) → (g ∘ f) x ≡ x ve-re x i = proj₁ x , eq i where eq : proj₂ ((g ∘ f) x) ≡ proj₂ x eq = begin proj₂ ((g ∘ f) x) ≡⟨⟩ - coe Q→P (proj₂ (f x)) ≡⟨⟩ - coe Q→P (coe P→Q (proj₂ x)) ≡⟨ inv-coe P→Q ⟩ - proj₂ x ∎ + proj₂ (g (f (a , pA))) ≡⟨⟩ + g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩ + pA ∎ + where + open Σ x renaming (proj₁ to a ; proj₂ to pA) + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g' ; proj₂ to inv) + module A = AreInverses inv + -- anti-funExt + lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA + lem i = A.verso-recto i pA re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x re-ve x i = proj₁ x , eq i where + open Σ x renaming (proj₁ to a ; proj₂ to qA) eq = begin proj₂ ((f ∘ g) x) ≡⟨⟩ - coe P→Q (coe Q→P (proj₂ x)) ≡⟨⟩ - coe P→Q (coe (sym P→Q) (proj₂ x)) ≡⟨ inv-coe' P→Q ⟩ - proj₂ x ∎ + _≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ + qA ∎ + where + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g' ; proj₂ to inv) + module A = AreInverses inv inv : AreInverses f g inv = record { verso-recto = funExt ve-re @@ -279,15 +300,11 @@ module _ (ℓ : Level) where -- -- is contractible, which implies univalence. - univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent' hA = {!!} , {!!} + univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent[Contr] hA = {!!} , {!!} - module _ {hA hB : hSet ℓ} where - - -- Thierry: `thr0` implies univalence. - univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = univalent'→univalent univalent' - -- let k = _≃_.isEqv (sym≃ conclusion) in {! k!} + univalent : Univalent + univalent = from[Contr] univalent[Contr] SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 74e4262..cd8a9ec 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -120,18 +120,16 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) - -- Alternative formulation of univalence which is easier to prove in the - -- case of the functor category. + + -- | Equivalent formulation of univalence. + Univalent[Contr] : Set _ + Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + + -- From: Thierry Coquand + -- Date: Wed, Mar 21, 2018 at 3:12 PM -- - -- ∀ A → isContr (Σ[ X ∈ Object ] iso A X) - - -- future work ideas: compile to CAM - Univalent' : Set _ - Univalent' = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) - - module _ (univalent' : Univalent') where - univalent'→univalent : Univalent - univalent'→univalent = {!!} + -- This is not so straight-forward so you can assume it + postulate from[Contr] : Univalent[Contr] → Univalent -- | The mere proposition of being a category. -- @@ -208,6 +206,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc hh = arrowsAreSets _ _ (snd x) (snd y) in h i , hh i + module _ {A B : Object} {p q : A ≅ B} where + open Σ p renaming (proj₁ to pf) + open Σ (snd p) renaming (proj₁ to pg ; proj₂ to pAreInv) + open Σ q renaming (proj₁ to qf) + open Σ (snd q) renaming (proj₁ to qg ; proj₂ to qAreInv) + module _ (a : pf ≡ qf) (b : pg ≡ qg) where + private + open import Cubical.Sigma + open import Cubical.NType.Properties + -- Problem: How do I apply lempPropF twice? + cc : (λ i → IsInverseOf (a i) pg) [ pAreInv ≡ _ ] + cc = lemPropF (λ x → propIsInverseOf {A} {B} {x}) a + c : (λ i → IsInverseOf (a i) (b i)) [ pAreInv ≡ qAreInv ] + c = lemPropF (λ x → propIsInverseOf {A} {B} {{!!}}) {!cc!} + + ≅-equality : p ≡ q + ≅-equality i = a i , b i , c i + module _ {A B : Object} {f : Arrow A B} where isoIsProp : isProp (Isomorphism f) isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 44b560e..390d8bc 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -78,8 +78,8 @@ EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _ EndoFunctor ℂ = Functor ℂ ℂ module _ - {ℓa ℓb : Level} - {ℂ 𝔻 : Category ℓa ℓb} + {ℓc ℓc' ℓd ℓd' : Level} + {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} (F : RawFunctor ℂ 𝔻) where private @@ -96,8 +96,7 @@ module _ -- Alternate version of above where `F` is indexed by an interval module _ - {ℓa ℓb : Level} - {ℂ 𝔻 : Category ℓa ℓb} + {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} {F : I → RawFunctor ℂ 𝔻} where private @@ -109,7 +108,7 @@ module _ IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} (\ F → propIsFunctor F) (\ i → F i) -module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where +module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where open Functor Functor≡ : {F G : Functor ℂ 𝔻} → Functor.raw F ≡ Functor.raw G