diff --git a/BACKLOG.md b/BACKLOG.md index ed1b205..91d6b63 100644 --- a/BACKLOG.md +++ b/BACKLOG.md @@ -1,19 +1,40 @@ Backlog ======= -Prove postulates in `Cat.Wishlist` -`ntypeCommulative` might be there as well. +Prove postulates in `Cat.Wishlist`: + * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A` -Prove that the opposite category is a category. +Prove that these two formulations of univalence are equivalent: + + ∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) + ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) Prove univalence for the category of - * sets + * the opposite category * functors and natural transformations Prove: * `isProp (Product ...)` * `isProp (HasProducts ...)` +Ideas for future work +--------------------- + +It would be nice if my formulation of monads is not so "stand-alone" as it is at +the moment. + +We can built up the notion of monads and related concept in multiple ways as +demonstrated in the two equivalent formulations of monads (kleisli/monoidal): +There seems to be a category-theoretic approach and an approach more in the +style of functional programming as e.g. the related typeclasses in the +standard library of Haskell. + +It would be nice to build up this hierarchy in two ways: The +"category-theoretic" way and the "functional programming" way. + +Here is an overview of some of the concepts that need to be developed to acheive +this: + * Functor ✓ * Applicative Functor ✗ * Lax monoidal functor ✗ @@ -24,7 +45,8 @@ Prove: * Monad * Monoidal monad ✓ * Kleisli monad ✓ - * Problem 2.3 in voe + * Kleisli ≃ Monoidal ✓ + * Problem 2.3 in [voe] ✓ * 1st contruction ~ monoidal ✓ * 2nd contruction ~ klesli ✓ - * 1st ≃ 2nd ✗ + * 1st ≃ 2nd ✓ diff --git a/CHANGELOG.md b/CHANGELOG.md index 625d640..42ab3e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,25 @@ Changelog ========= +Version 1.4.1 +------------- +Defines a module to work with equivalence providing a way to go between +equivalences and quasi-inverses (in the parlance of HoTT). + +Finishes the proof that the category of homotopy-sets are univalent. + +Defines a custom "prelude" module that wraps the `cubical` library and provides +a few utilities. + +Reorders Category.isIdentity such that the left projection is left identity. + +Include some text for the half-time report. + +Renames IsProduct.isProduct to IsProduct.ump to avoid ambiguity in some +circumstances. + +[WIP]: Adds some stuff about propositionality for products. + Version 1.4.0 ------------- Adds documentation to a number of modules. diff --git a/Makefile b/Makefile index 051f9ce..1a3e6e8 100644 --- a/Makefile +++ b/Makefile @@ -1,2 +1,5 @@ build: src/**.agda agda src/Cat.agda + +clean: + find src -name "*.agdai" -type f -delete diff --git a/proposal/BACKLOG.md b/proposal/BACKLOG.md new file mode 100644 index 0000000..b889c92 --- /dev/null +++ b/proposal/BACKLOG.md @@ -0,0 +1,22 @@ +Remove stuff about models of type theory + +Add references to specific (noteable) implementaitons of category theory: +* Unimath +* cubicaltt +* https://github.com/pcapriotti/agda-categories +* https://github.com/copumpkin/categories +* ... + +Talk about structure of library: +=== + +Propositional- and non-propositional stuff split up +Providing "equiality principles" +Provide overview of what has been proven. + +What can I say about reusability? + +Misc +==== + +Propositional content diff --git a/proposal/halftime.tex b/proposal/halftime.tex new file mode 100644 index 0000000..11dc836 --- /dev/null +++ b/proposal/halftime.tex @@ -0,0 +1,177 @@ +\section{Halftime report} +I've written this as an appendix because 1) the aim of the thesis changed +drastically from the planning report/proposal 2) partly I'm not sure how to +structure my thesis. + +My work so far has very much focused on the formalization, i.e. coding. It's +unclear to me at this point what I should have in the final report. Here I will +describe what I have managed to formalize so far and what outstanding challenges +I'm facing. + +\subsection{Implementation overview} +The overall structure of my project is as follows: + +\begin{itemize} +\item Core categorical concepts +\subitem Categories +\subitem Functors +\subitem Products +\subitem Exponentials +\subitem Cartesian closed categories +\subitem Natural transformations +\subitem Yoneda embedding +\subitem Monads +\subsubitem Monoidal monads +\subsubitem Kleisli monads +\subsubitem Voevodsky's construction +\item Category of \ldots +\subitem Homotopy sets +\subitem Categories +\subitem Relations +\subitem Functors +\subitem Free category +\end{itemize} + +I also started work on the category with families as well as the cubical +category as per the original goal of the thesis. However I have not gotten so +far with this. + +In the following I will give an overview of overall results in each of these +categories (no pun). + +As an overall design-guideline I've defined concepts in a such a way that the +``data'' and the ``laws'' about that data is split up in seperate modules. As an +example a category is defined to have two members: `raw` which is a collection +of the data and `isCategory` which asserts some laws about that data. + +This allows me to reason about things in a more mathematical way, where one can +reason about two categories by simply focusing on the data. This is acheived by +creating a function embodying the ``equality principle'' for a given record. In +the case of monads, to prove two categories propositionally equal it enough to +provide a proof that their data is equal. + +\subsubsection{Categories} +Defines the basic notion of a category. This definition closely follows that of +[HoTT]: That is, the standard definition of a category (data; objects, arrows, +composition and identity, laws; preservation of identity and composition) plus +the extra condition that it is univalent - namely that you can get an equality +of two objects from an isomorphism. + +I make no distinction between a pre-category and a real category (as in the +[HoTT]-sense). A pre-category in my implementation would be a category sans the +witness to univalence. + +I also prove that being a category is a proposition. This gives rise to an +equality principle for monads that focuses on the data-part. + +I also show that the opposite category is indeed a category. (\WIP{} I have not +shown that univalence holds for such a construction) + +I also show that taking the opposite is an involution. + +\subsubsection{Functors} +Defines the notion of a functor - also split up into data and laws. + +Propositionality for being a functor. + +Composition of functors and the identity functor. + +\subsubsection{Products} +Definition of what it means for an object to be a product in a given category. + +Definition of what it means for a category to have all products. + +\WIP Prove propositionality for being a product and having products. + +\subsubsection{Exponentials} +Definition of what it means to be an exponential object. + +Definition of what it means for a category to have all exponential objects. + +\subsubsection{Cartesian closed categories} +Definition of what it means for a category to be cartesian closed; namely that +it has all products and all exponentials. + +\subsubsection{Natural transformations} +Definition of transformations\footnote{Maybe this is a name I made up for a + family of morphisms} and the naturality condition for these. + +Proof that naturality is a mere proposition and the accompanying equality +principle. Proof that natural transformations are homotopic sets. + +The identity natural transformation. + +\subsubsection{Yoneda embedding} + +The yoneda embedding is typically presented in terms of the category of +categories (cf. Awodey) \emph however this is not stricly needed - all we need +is what would be the exponential object in that category - this happens to be +functors and so this is how we define the yoneda embedding. + +\subsubsection{Monads} + +Defines an equivalence between these two formulations of a monad: + +\subsubsubsection{Monoidal monads} + +Defines the standard monoidal representation of a monad: + +An endofunctor with two natural transformations (called ``pure'' and ``join'') +and some laws about these natural transformations. + +Propositionality proofs and equality principle is provided. + +\subsubsubsection{Kleisli monads} + +A presentation of monads perhaps more familiar to a functional programer: + +A map on objects and two maps on morphisms (called ``pure'' and ``bind'') and +some laws about these maps. + +Propositionality proofs and equality principle is provided. + +\subsubsubsection{Voevodsky's construction} + +Provides construction 2.3 as presented in an unpublished paper by the late +Vladimir Voevodsky. This construction is similiar to the equivalence provided +for the two preceding formulations +\footnote{ TODO: I would like to include in the thesis some motivation for why + this construction is particularly interesting.} + +\subsubsection{Homotopy sets} +The typical category of sets where the objects are modelled by an Agda set +(henceforth ``type'') at a given level is not a valid category in this cubical +settings, we need to restrict the types to be those that are homotopy sets. Thus the objects of this category are: +% +$$\Set_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$ +% +\WIP{} I'm still missing a few details for the proof that this category is +univalent. Indeed this doesn't not follow immediately from +% +$$\mathit{univalence} \tp (A \cong B) \simeq (A \simeq B)$$ +% +since $A$ and $B$ are of type $\MCU \neq \Set$. +\subsubsection{Categories} +Note that this category does in fact not exist. In stead I provide the +definition of the ``raw'' category as well as some of the laws. + +Furthermore I provide some helpful lemmas about this raw category. For instance +I have shown what would be the exponential object in such a category. + +These lemmas can be used to provide the actual exponential object in a context +where we have a witness to this being a category. This is useful if this library +is later extended to talk about higher categories. + +\subsubsection{Functors} +The category of functors and natural transformations. An immediate corrolary is +the set of presheaf categories. + +\WIP{} I have not shown that the category of functors is univalent. + +\subsubsection{Relations} +The category of relations. \WIP I have not shown that this category is +univalent. Not sure I intend to do so either. + +\subsubsection{Free category} +The free category of a category. \WIP I have not shown that this category is +univalent. diff --git a/proposal/macros.tex b/proposal/macros.tex index d1bf101..2653ac3 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -18,3 +18,9 @@ \newcommand{\fmap}{\mathit{fmap}} \newcommand{\idFun}{\mathit{id}} \newcommand{\Sets}{\mathit{Sets}} +\newcommand{\Set}{\mathit{Set}} +\newcommand{\MCU}{\UU} +\newcommand{\isSet}{\mathit{isSet}} +\newcommand{\tp}{\;\mathord{:}\;} +\newcommand{\subsubsubsection}[1]{\textbf{#1}} +\newcommand{\WIP}[1]{\textbf{[WIP]}} diff --git a/proposal/proposal.tex b/proposal/proposal.tex index c6cb67d..073ecb5 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -13,6 +13,8 @@ \usepackage{multicol} \usepackage{amsmath,amssymb} \usepackage[toc,page]{appendix} +\usepackage{xspace} + % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -282,5 +284,6 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda. \bibliography{refs} \begin{appendices} \input{planning.tex} +\input{halftime.tex} \end{appendices} \end{document} diff --git a/src/Cat.agda b/src/Cat.agda index 86e6879..80d101d 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -8,7 +8,10 @@ open import Cat.Category.Exponential open import Cat.Category.CartesianClosed open import Cat.Category.NaturalTransformation open import Cat.Category.Yoneda +open import Cat.Category.Monoid open import Cat.Category.Monad +open Cat.Category.Monad.Monoidal +open Cat.Category.Monad.Kleisli open import Cat.Category.Monad.Voevodsky open import Cat.Categories.Sets diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 8c7bcbb..e8a6f73 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -3,22 +3,14 @@ module Cat.Categories.Cat where -open import Agda.Primitive -open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) - -open import Cubical -open import Cubical.Sigma +open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd) open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Category.Exponential hiding (_×_ ; product) open import Cat.Category.NaturalTransformation - -open import Cat.Equality -open Equality.Data.Product - -open Category using (Object ; 𝟙) +open import Cat.Categories.Fun -- The category of categories module _ (ℓ ℓ' : Level) where @@ -35,19 +27,18 @@ module _ (ℓ ℓ' : Level) where ident-l = Functor≡ refl RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - RawCat = - record - { Object = Category ℓ ℓ' - ; Arrow = Functor - ; 𝟙 = identity - ; _∘_ = F[_∘_] - } + RawCategory.Object RawCat = Category ℓ ℓ' + RawCategory.Arrow RawCat = Functor + RawCategory.𝟙 RawCat = identity + RawCategory._∘_ RawCat = F[_∘_] + private open RawCategory RawCat isAssociative : IsAssociative isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} - ident : IsIdentity identity - ident = ident-r , ident-l + + isIdentity : IsIdentity identity + isIdentity = ident-l , ident-r -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -55,7 +46,7 @@ module _ (ℓ ℓ' : Level) where -- -- Because of this there is no category of categories. Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - Category.raw (Cat _) = RawCat + Category.raw (Cat _) = RawCat Category.isCategory (Cat unprovable) = unprovable -- | In the following we will pretend there is a category of categories when @@ -72,32 +63,36 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where module ℂ = Category ℂ module 𝔻 = Category 𝔻 - Obj = Object ℂ × Object 𝔻 - Arr : Obj → Obj → Set ℓ' - Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] - 𝟙' : {o : Obj} → Arr o o - 𝟙' = 𝟙 ℂ , 𝟙 𝔻 - _∘_ : - {a b c : Obj} → - Arr b c → - Arr a b → - Arr a c - _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} + module _ where + private + Obj = ℂ.Object × 𝔻.Object + Arr : Obj → Obj → Set ℓ' + Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] + 𝟙 : {o : Obj} → Arr o o + 𝟙 = ℂ.𝟙 , 𝔻.𝟙 + _∘_ : + {a b c : Obj} → + Arr b c → + Arr a b → + Arr a c + _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} - rawProduct : RawCategory ℓ ℓ' - RawCategory.Object rawProduct = Obj - RawCategory.Arrow rawProduct = Arr - RawCategory.𝟙 rawProduct = 𝟙' - RawCategory._∘_ rawProduct = _∘_ - open RawCategory rawProduct + rawProduct : RawCategory ℓ ℓ' + RawCategory.Object rawProduct = Obj + RawCategory.Arrow rawProduct = Arr + RawCategory.𝟙 rawProduct = 𝟙 + RawCategory._∘_ rawProduct = _∘_ + + open RawCategory rawProduct arrowsAreSets : ArrowsAreSets arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets} - isIdentity : IsIdentity 𝟙' + isIdentity : IsIdentity 𝟙 isIdentity = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity) , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity) - postulate univalent : Univalence.Univalent rawProduct isIdentity + + postulate univalent : Univalence.Univalent isIdentity instance isCategory : IsCategory rawProduct IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative @@ -167,7 +162,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where RawProduct.proj₂ rawProduct = P.proj₂ isProduct : IsProduct Catℓ _ _ rawProduct - IsProduct.isProduct isProduct = P.isProduct + IsProduct.ump isProduct = P.isProduct product : Product Catℓ ℂ 𝔻 Product.raw product = rawProduct @@ -181,109 +176,70 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where -- it is therefory also cartesian closed. module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where private - open Data.Product - open import Cat.Categories.Fun module ℂ = Category ℂ module 𝔻 = Category 𝔻 Categoryℓ = Category ℓ ℓ open Fun ℂ 𝔻 renaming (identity to idN) - omap : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 + omap : Functor ℂ 𝔻 × ℂ.Object → 𝔻.Object omap (F , A) = Functor.omap F A -- The exponential object object : Categoryℓ object = Fun - module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where + module _ {dom cod : Functor ℂ 𝔻 × ℂ.Object} where + open Σ dom renaming (proj₁ to F ; proj₂ to A) + open Σ cod renaming (proj₁ to G ; proj₂ to B) private - F : Functor ℂ 𝔻 - F = proj₁ dom - A : Object ℂ - A = proj₂ dom - - G : Functor ℂ 𝔻 - G = proj₁ cod - B : Object ℂ - B = proj₂ cod - module F = Functor F module G = Functor G fmap : (pobj : NaturalTransformation F G × ℂ [ A , B ]) → 𝔻 [ F.omap A , G.omap B ] - fmap ((θ , θNat) , f) = result - where - θA : 𝔻 [ F.omap A , G.omap A ] - θA = θ A - θB : 𝔻 [ F.omap B , G.omap B ] - θB = θ B - F→f : 𝔻 [ F.omap A , F.omap B ] - F→f = F.fmap f - G→f : 𝔻 [ G.omap A , G.omap B ] - G→f = G.fmap f - l : 𝔻 [ F.omap A , G.omap B ] - l = 𝔻 [ θB ∘ F.fmap f ] - r : 𝔻 [ F.omap A , G.omap B ] - r = 𝔻 [ G.fmap f ∘ θA ] - result : 𝔻 [ F.omap A , G.omap B ] - result = l + fmap ((θ , θNat) , f) = 𝔻 [ θ B ∘ F.fmap f ] + -- Alternatively: + -- + -- fmap ((θ , θNat) , f) = 𝔻 [ G.fmap f ∘ θ A ] + -- + -- Since they are equal by naturality of θ. open CatProduct renaming (object to _⊗_) using () - module _ {c : Functor ℂ 𝔻 × Object ℂ} where - private - F : Functor ℂ 𝔻 - F = proj₁ c - C : Object ℂ - C = proj₂ c + module _ {c : Functor ℂ 𝔻 × ℂ.Object} where + open Σ c renaming (proj₁ to F ; proj₂ to C) - ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 + ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙 ident = begin - fmap {c} {c} (𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ - fmap {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ - 𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ - F.fmap (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ - 𝟙 𝔻 ∎ + fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ + fmap {c} {c} (idN F , ℂ.𝟙) ≡⟨⟩ + 𝔻 [ identityTrans F C ∘ F.fmap ℂ.𝟙 ] ≡⟨⟩ + 𝔻 [ 𝔻.𝟙 ∘ F.fmap ℂ.𝟙 ] ≡⟨ 𝔻.leftIdentity ⟩ + F.fmap ℂ.𝟙 ≡⟨ F.isIdentity ⟩ + 𝔻.𝟙 ∎ where module F = Functor F - module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where + module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ.Object} where + open Σ F×A renaming (proj₁ to F ; proj₂ to A) + open Σ G×B renaming (proj₁ to G ; proj₂ to B) + open Σ H×C renaming (proj₁ to H ; proj₂ to C) private - F = F×A .proj₁ - A = F×A .proj₂ - G = G×B .proj₁ - B = G×B .proj₂ - H = H×C .proj₁ - C = H×C .proj₂ module F = Functor F module G = Functor G module H = Functor H module _ - -- NaturalTransformation F G × ℂ .Arrow A B {θ×f : NaturalTransformation F G × ℂ [ A , B ]} {η×g : NaturalTransformation G H × ℂ [ B , C ]} where + open Σ θ×f renaming (proj₁ to θNT ; proj₂ to f) + open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat) + open Σ η×g renaming (proj₁ to ηNT ; proj₂ to g) + open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat) private - θ : Transformation F G - θ = proj₁ (proj₁ θ×f) - θNat : Natural F G θ - θNat = proj₂ (proj₁ θ×f) - f : ℂ [ A , B ] - f = proj₂ θ×f - η : Transformation G H - η = proj₁ (proj₁ η×g) - ηNat : Natural G H η - ηNat = proj₂ (proj₁ η×g) - g : ℂ [ B , C ] - g = proj₂ η×g - ηθNT : NaturalTransformation F H - ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) - - ηθ = proj₁ ηθNT - ηθNat = proj₂ ηθNT + ηθNT = NT[_∘_] {F} {G} {H} ηNT θNT + open Σ ηθNT renaming (proj₁ to ηθ ; proj₂ to ηθNat) isDistributive : 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ] diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index 00f10e3..f338343 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -1,21 +1,18 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Cube where +open import Cat.Prelude open import Level open import Data.Bool hiding (T) open import Data.Sum hiding ([_,_]) open import Data.Unit open import Data.Empty -open import Data.Product -open import Cubical open import Function open import Relation.Nullary open import Relation.Nullary.Decidable open import Cat.Category open import Cat.Category.Functor -open import Cat.Equality -open Equality.Data.Product -- See chapter 1 for a discussion on how presheaf categories are CwF's. diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda index ea369ef..45dbf2b 100644 --- a/src/Cat/Categories/CwF.agda +++ b/src/Cat/Categories/CwF.agda @@ -1,36 +1,33 @@ module Cat.Categories.CwF where -open import Agda.Primitive -open import Data.Product +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor open import Cat.Categories.Fam -open Category -open Functor - module _ {ℓa ℓb : Level} where record CwF : Set (lsuc (ℓa ⊔ ℓb)) where -- "A category with families consists of" field -- "A base category" ℂ : Category ℓa ℓb + module ℂ = Category ℂ -- It's objects are called contexts - Contexts = Object ℂ + Contexts = ℂ.Object -- It's arrows are called substitutions - Substitutions = Arrow ℂ + Substitutions = ℂ.Arrow field -- A functor T T : Functor (opposite ℂ) (Fam ℓa ℓb) -- Empty context - [] : Terminal ℂ + [] : ℂ.Terminal private module T = Functor T - Type : (Γ : Object ℂ) → Set ℓa + Type : (Γ : ℂ.Object) → Set ℓa Type Γ = proj₁ (proj₁ (T.omap Γ)) - module _ {Γ : Object ℂ} {A : Type Γ} where + module _ {Γ : ℂ.Object} {A : Type Γ} where -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where -- k : Σ (proj₁ (omap T B) → proj₁ (omap T A)) @@ -46,7 +43,7 @@ module _ {ℓa ℓb : Level} where record ContextComprehension : Set (ℓa ⊔ ℓb) where field - Γ&A : Object ℂ + Γ&A : ℂ.Object proj1 : ℂ [ Γ&A , Γ ] -- proj2 : ???? diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index d100b77..5ffde56 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -1,21 +1,14 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Fam where -open import Agda.Primitive -open import Data.Product +open import Cat.Prelude import Function -open import Cubical -open import Cubical.Universe - open import Cat.Category -open import Cat.Equality - -open Equality.Data.Product 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/Free.agda b/src/Cat/Categories/Free.agda index 7e80478..1d262dd 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -1,62 +1,77 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Free where -open import Agda.Primitive -open import Cubical hiding (Path ; isSet ; empty) -open import Data.Product +open import Cat.Prelude hiding (Path ; empty) + +open import Relation.Binary open import Cat.Category -data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where - empty : {a : A} → Path R a a - cons : {a b c : A} → R b c → Path R a b → Path R a c +module _ {ℓ : Level} {A : Set ℓ} {ℓr : Level} where + data Path (R : Rel A ℓr) : (a b : A) → Set (ℓ ⊔ ℓr) where + empty : {a : A} → Path R a a + cons : {a b c : A} → R b c → Path R a b → Path R a c -concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c -concatenate empty p = p -concatenate (cons x q) p = cons x (concatenate q p) -_++_ = concatenate + module _ {R : Rel A ℓr} where + concatenate : {a b c : A} → Path R b c → Path R a b → Path R a c + concatenate empty p = p + concatenate (cons x q) p = cons x (concatenate q p) + _++_ : {a b c : A} → Path R b c → Path R a b → Path R a c + a ++ b = concatenate a b -singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B -singleton f = cons f empty + singleton : {a b : A} → R a b → Path R a b + singleton f = cons f empty -module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private module ℂ = Category ℂ - open Category ℂ - p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D} + RawFree : RawCategory ℓa (ℓa ⊔ ℓb) + RawCategory.Object RawFree = ℂ.Object + RawCategory.Arrow RawFree = Path ℂ.Arrow + RawCategory.𝟙 RawFree = empty + RawCategory._∘_ RawFree = concatenate + + open RawCategory RawFree + + isAssociative : {A B C D : ℂ.Object} {r : Path ℂ.Arrow A B} {q : Path ℂ.Arrow B C} {p : Path ℂ.Arrow C D} → p ++ (q ++ r) ≡ (p ++ q) ++ r - p-isAssociative {r = r} {q} {empty} = refl - p-isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin + isAssociative {r = r} {q} {empty} = refl + isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin cons x p ++ (q ++ r) ≡⟨ cong (cons x) lem ⟩ cons x ((p ++ q) ++ r) ≡⟨⟩ (cons x p ++ q) ++ r ∎ where - lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r) - lem = p-isAssociative {r = r} {q} {p} + lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r) + lem = isAssociative {r = r} {q} {p} - ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p + ident-r : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate p empty ≡ p ident-r {p = empty} = refl ident-r {p = cons x p} = cong (cons x) ident-r - ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p + ident-l : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate empty p ≡ p ident-l = refl - module _ {A B : Object} where - isSet : Cubical.isSet (Path Arrow A B) - isSet a b p q = {!!} + isIdentity : IsIdentity 𝟙 + isIdentity = ident-l , ident-r - RawFree : RawCategory ℓ (ℓ ⊔ ℓ') - RawFree = record - { Object = Object - ; Arrow = Path Arrow - ; 𝟙 = empty - ; _∘_ = concatenate - } - RawIsCategoryFree : IsCategory RawFree - RawIsCategoryFree = record - { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}} - ; isIdentity = ident-r , ident-l - ; arrowsAreSets = {!!} - ; univalent = {!!} - } + open Univalence isIdentity + + module _ {A B : ℂ.Object} where + arrowsAreSets : isSet (Path ℂ.Arrow A B) + arrowsAreSets a b p q = {!!} + + eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B) + eqv = {!!} + + univalent : Univalent + univalent = eqv + + isCategory : IsCategory RawFree + IsCategory.isAssociative isCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h} + IsCategory.isIdentity isCategory = isIdentity + IsCategory.arrowsAreSets isCategory = arrowsAreSets + IsCategory.univalent isCategory = univalent + + Free : Category _ _ + Free = record { raw = RawFree ; isCategory = isCategory } diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 019e8b6..18165d3 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,13 +1,7 @@ {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Categories.Fun where -open import Agda.Primitive -open import Data.Product - - -open import Cubical -open import Cubical.GradLemma -open import Cubical.NType.Properties +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor hiding (identity) @@ -45,18 +39,18 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C eq-r C = begin 𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩ - 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.isIdentity ⟩ + 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ 𝔻.rightIdentity ⟩ f' C ∎ eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C - eq-l C = proj₂ 𝔻.isIdentity + eq-l C = 𝔻.leftIdentity ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f ident-r = lemSig allNatural _ _ (funExt eq-r) ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f ident-l = lemSig allNatural _ _ (funExt eq-l) isIdentity - : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f - × (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f - isIdentity = ident-r , ident-l + : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f + × (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f + isIdentity = ident-l , ident-r -- Functor categories. Objects are functors, arrows are natural transformations. RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') RawFun = record @@ -67,55 +61,57 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C } open RawCategory RawFun - open Univalence RawFun - module _ {A B : Functor ℂ 𝔻} where - module A = Functor A - module B = Functor B - module _ (p : A ≡ B) where - omapP : A.omap ≡ B.omap - omapP i = Functor.omap (p i) + open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) - coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ] - coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP + private + module _ {A B : Functor ℂ 𝔻} where + module A = Functor A + module B = Functor B + module _ (p : A ≡ B) where + omapP : A.omap ≡ B.omap + omapP i = Functor.omap (p i) - -- The transformation will be the identity on 𝔻. Such an arrow has the - -- type `A.omap A → A.omap A`. Which we can coerce to have the type - -- `A.omap → B.omap` since `A` and `B` are equal. - coe𝟙 : Transformation A B - coe𝟙 X = coe coerceAB 𝔻.𝟙 + coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ] + coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP - module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where - nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ] - nat' = begin - (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ - (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎ + -- The transformation will be the identity on 𝔻. Such an arrow has the + -- type `A.omap A → A.omap A`. Which we can coerce to have the type + -- `A.omap → B.omap` since `A` and `B` are equal. + coe𝟙 : Transformation A B + coe𝟙 X = coe coerceAB 𝔻.𝟙 - transs : (i : I) → Transformation A (p i) - transs = {!!} + module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where + nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ] + nat' = begin + (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ + (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎ - natt : (i : I) → Natural A (p i) {!!} - natt = {!!} + transs : (i : I) → Transformation A (p i) + transs = {!!} - t : Natural A B coe𝟙 - t = coe c (identityNatural A) - where - c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙 - c = begin - Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩ - Natural A B coe𝟙 ∎ - -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!} + natt : (i : I) → Natural A (p i) {!!} + natt = {!!} - k : Natural A A (identityTrans A) → Natural A B coe𝟙 - k n {a} {b} f = res - where - res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ]) - res = {!!} + t : Natural A B coe𝟙 + t = coe c (identityNatural A) + where + c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙 + c = begin + Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩ + Natural A B coe𝟙 ∎ + -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!} - nat : Natural A B coe𝟙 - nat = nat' + k : Natural A A (identityTrans A) → Natural A B coe𝟙 + k n {a} {b} f = res + where + res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ]) + res = {!!} - fromEq : NaturalTransformation A B - fromEq = coe𝟙 , nat + nat : Natural A B coe𝟙 + nat = nat' + + fromEq : NaturalTransformation A B + fromEq = coe𝟙 , nat module _ {A B : Functor ℂ 𝔻} where obverse : A ≡ B → A ≅ B @@ -145,10 +141,10 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x re-ve = {!!} - done : isEquiv (A ≡ B) (A ≅ B) (id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B) + done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B) done = {!gradLemma obverse reverse ve-re re-ve!} - univalent : Univalent (λ{ {A} {B} → isIdentity {A} {B}}) + univalent : Univalent univalent = done instance diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 1dbed3d..5b44601 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,12 +1,8 @@ {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Categories.Rel where -open import Cubical -open import Cubical.GradLemma -open import Agda.Primitive -open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) +open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd) open import Function -import Cubical.FromStdLib open import Cat.Category @@ -74,11 +70,11 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≃ (a , b) ∈ S - equi = backwards Cubical.FromStdLib., isequiv + equi = backwards , isequiv - ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) + ident-r : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≡ (a , b) ∈ S - ident-l = equivToPath equi + ident-r = equivToPath equi module _ where private @@ -108,11 +104,11 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≃ ab ∈ S - equi = backwards Cubical.FromStdLib., isequiv + equi = backwards , isequiv - ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) + ident-l : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≡ ab ∈ S - ident-r = equivToPath equi + ident-l = equivToPath equi module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset (C × D)} (ad : A × D) where private @@ -146,7 +142,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) - equi = fwd Cubical.FromStdLib., isequiv + equi = fwd , isequiv -- isAssociativec : Q + (R + S) ≡ (Q + R) + S is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index a329a0f..05c64b3 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,166 +1,289 @@ -- | The category of homotopy sets -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} module Cat.Categories.Sets where -open import Agda.Primitive -open import Data.Product -open import Function using (_∘_) +open import Cat.Prelude hiding (_≃_) +import Data.Product -open import Cubical hiding (_≃_ ; inverse) -open import Cubical.Equivalence - renaming - ( _≅_ to _A≅_ ) - using - (_≃_ ; con ; AreInverses) -open import Cubical.Univalence -open import Cubical.GradLemma +open import Function using (_∘_ ; _∘′_) + +open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Wishlist +open import Cat.Equivalence as Eqv using (AreInverses ; module Equiv≃ ; module NoEta) + +open NoEta + +module Equivalence = Equivalence′ + +_⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C +eqA ⊙ eqB = Equivalence.compose eqA eqB + +sym≃ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ≃ B → B ≃ A +sym≃ = Equivalence.symmetry + +infixl 10 _⊙_ + +module _ {ℓ : Level} {A : Set ℓ} {a : A} where + id-coe : coe refl a ≡ a + id-coe = begin + coe refl a ≡⟨⟩ + pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩ + _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩ + a ∎ + +module _ {ℓ : Level} {A B : Set ℓ} {a : A} where + inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a + inv-coe p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + d : D A refl + d = begin + coe (sym refl) (coe refl a) ≡⟨⟩ + coe refl (coe refl a) ≡⟨ id-coe ⟩ + coe refl a ≡⟨ id-coe ⟩ + a ∎ + in pathJ D d B p + inv-coe' : (p : B ≡ A) → coe p (coe (sym p) a) ≡ a + inv-coe' p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + k : coe p (coe (sym p) a) ≡ a + k = pathJ D (trans id-coe id-coe) B (sym p) + in k module _ (ℓ : Level) where private - open import Cubical.Univalence - open import Cubical.NType.Properties - open import Cubical.Universe - SetsRaw : RawCategory (lsuc ℓ) ℓ - RawCategory.Object SetsRaw = hSet + RawCategory.Object SetsRaw = hSet ℓ RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U RawCategory.𝟙 SetsRaw = Function.id RawCategory._∘_ SetsRaw = Function._∘′_ open RawCategory SetsRaw hiding (_∘_) - open Univalence SetsRaw isIdentity : IsIdentity Function.id proj₁ isIdentity = funExt λ _ → refl proj₂ isIdentity = funExt λ _ → refl + open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) + arrowsAreSets : ArrowsAreSets arrowsAreSets {B = (_ , s)} = setPi λ _ → s + isIso = Eqv.Isomorphism + module _ {hA hB : hSet ℓ} where + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) + lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f) + lem1 f sA sB = res + where + module _ (x y : isIso f) where + module x = Σ x renaming (proj₁ to inverse ; proj₂ to areInverses) + module y = Σ y renaming (proj₁ to inverse ; proj₂ to areInverses) + module xA = AreInverses x.areInverses + module yA = AreInverses y.areInverses + -- I had a lot of difficulty using the corresponding proof where + -- AreInverses is defined. This is sadly a bit anti-modular. The + -- reason for my troubles is probably related to the type of objects + -- being hSet's rather than sets. + p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g) + p {f} g xx yy i = record + { verso-recto = ve-re + ; recto-verso = re-ve + } + where + module xxA = AreInverses xx + module yyA = AreInverses yy + ve-re : g ∘ f ≡ Function.id + ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i + re-ve : f ∘ g ≡ Function.id + re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i + 1eq : x.inverse ≡ y.inverse + 1eq = begin + x.inverse ≡⟨⟩ + x.inverse ∘ Function.id ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩ + x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩ + (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩ + Function.id ∘ y.inverse ≡⟨⟩ + y.inverse ∎ + 2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ] + 2eq = lemPropF p 1eq + res : x ≡ y + res i = 1eq i , 2eq i + module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where + lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) + → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) + lem2 pA p q = fromIsomorphism iso + where + f : ∀ {p q} → p ≡ q → proj₁ p ≡ proj₁ q + f e i = proj₁ (e i) + g : ∀ {p q} → proj₁ p ≡ proj₁ q → p ≡ q + g {p} {q} = lemSig pA p q + ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e + ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e) + (\ i j → p .proj₁ , propSet (pA (p .proj₁)) (p .proj₂) (p .proj₂) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .proj₂) (λ i → p .proj₂) i j ) q + re-ve : (e : proj₁ p ≡ proj₁ q) → (f {p} {q} ∘ g {p} {q}) e ≡ e + re-ve e = refl + inv : AreInverses (f {p} {q}) (g {p} {q}) + inv = record + { verso-recto = funExt ve-re + ; recto-verso = funExt re-ve + } + iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) + iso = f , g , inv + + lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)} + → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q + lem3 {Q = Q} eA = res + where + f : Σ A P → Σ A Q + f (a , pA) = a , _≃_.eqv (eA a) pA + g : Σ A Q → Σ A P + g (a , qA) = a , g' qA + where + k : Eqv.Isomorphism _ + k = Equiv≃.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) ≡⟨⟩ + proj₂ (g (f (a , pA))) ≡⟨⟩ + g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩ + pA ∎ + where + open Σ x renaming (proj₁ to a ; proj₂ to pA) + k : Eqv.Isomorphism _ + k = Equiv≃.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) ≡⟨⟩ + _≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ + qA ∎ + where + k : Eqv.Isomorphism _ + k = Equiv≃.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 + ; recto-verso = funExt re-ve + } + iso : Σ A P Eqv.≅ Σ A Q + iso = f , g , inv + res : Σ A P ≃ Σ A Q + res = fromIsomorphism iso + + module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + lem4 : isSet A → isSet B → (f : A → B) + → isEquiv A B f ≃ isIso f + lem4 sA sB f = + let + obv : isEquiv A B f → isIso f + obv = Equiv≃.toIso A B + inv : isIso f → isEquiv A B f + inv = Equiv≃.fromIso A B + re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x + re-ve = Equiv≃.inverse-from-to-iso A B + ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x + ve-re = Equiv≃.inverse-to-from-iso A B sA sB + iso : isEquiv A B f Eqv.≅ isIso f + iso = obv , inv , + record + { verso-recto = funExt re-ve + ; recto-verso = funExt ve-re + } + in fromIsomorphism iso + module _ {hA hB : Object} where - private - A = proj₁ hA - isSetA : isSet A - isSetA = proj₂ hA - B = proj₁ hB - isSetB : isSet B - isSetB = proj₂ hB + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) - toIsomorphism : A ≃ B → hA ≅ hB - toIsomorphism e = obverse , inverse , verso-recto , recto-verso + -- lem3 and the equivalence from lem4 + step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) + step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f)) + + -- univalence + step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) + step1 = hh ⊙ h + where + h : (A ≃ B) ≃ (A ≡ B) + h = sym≃ (univalence {A = A} {B}) + obv : Σ (A → B) (isEquiv A B) → A ≃ B + obv = Eqv.deEta + inv : A ≃ B → Σ (A → B) (isEquiv A B) + inv = Eqv.doEta + re-ve : (x : _) → (inv ∘ obv) x ≡ x + re-ve x = refl + -- Because _≃_ does not have eta equality! + ve-re : (x : _) → (obv ∘ inv) x ≡ x + ve-re (con eqv isEqv) i = con eqv isEqv + areInv : AreInverses obv inv + areInv = record { verso-recto = funExt re-ve ; recto-verso = funExt ve-re } + eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B) + eqv = obv , inv , areInv + hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B) + hh = fromIsomorphism eqv + + -- lem2 with propIsSet + step2 : (A ≡ B) ≃ (hA ≡ hB) + step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB) + + -- Go from an isomorphism on sets to an isomorphism on homotopic sets + trivial? : (hA ≅ hB) ≃ (A Eqv.≅ B) + trivial? = sym≃ (fromIsomorphism res) + where + fwd : Σ (A → B) isIso → hA ≅ hB + fwd (f , g , inv) = f , g , inv.toPair where - open _≃_ e + module inv = AreInverses inv + bwd : hA ≅ hB → Σ (A → B) isIso + bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y } + res : Σ (A → B) isIso Eqv.≅ (hA ≅ hB) + res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl } - fromIsomorphism : hA ≅ hB → A ≃ B - fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto) - where - obverse : A → B - obverse = proj₁ iso - inverse : B → A - inverse = proj₁ (proj₂ iso) - -- FIXME IsInverseOf should change name to AreInverses and the - -- ordering should be swapped. - areInverses : IsInverseOf {A = hA} {hB} obverse inverse - areInverses = proj₂ (proj₂ iso) - verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a - verso-recto a i = proj₁ areInverses i a - recto-verso : ∀ b → (obverse Function.∘ inverse) b ≡ b - recto-verso b i = proj₂ areInverses i b + conclusion : (hA ≅ hB) ≃ (hA ≡ hB) + conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2 - private - univIso : (A ≡ B) A≅ (A ≃ B) - univIso = _≃_.toIsomorphism univalence - obverse' : A ≡ B → A ≃ B - obverse' = proj₁ univIso - inverse' : A ≃ B → A ≡ B - inverse' = proj₁ (proj₂ univIso) - -- Drop proof of being a set from both sides of an equality. - dropP : hA ≡ hB → A ≡ B - dropP eq i = proj₁ (eq i) - -- Add proof of being a set to both sides of a set-theoretic equivalence - -- returning a category-theoretic equivalence. - addE : A A≅ B → hA ≅ hB - addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair - where - areeqv = proj₂ (proj₂ eqv) - asPair = - let module Inv = AreInverses areeqv - in Inv.verso-recto , Inv.recto-verso + univ≃ : (hA ≅ hB) ≃ (hA ≡ hB) + univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2 - obverse : hA ≡ hB → hA ≅ hB - obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP + module _ (hA : Object) where + open Σ hA renaming (proj₁ to A) - -- Drop proof of being a set form both sides of a category-theoretic - -- equivalence returning a set-theoretic equivalence. - dropE : hA ≅ hB → A A≅ B - dropE eqv = obv , inv , asAreInverses - where - obv = proj₁ eqv - inv = proj₁ (proj₂ eqv) - areEq = proj₂ (proj₂ eqv) - asAreInverses : AreInverses A B obv inv - asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq } + eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) + eq1 = ua (lem3 (\ hB → univ≃)) - -- Dunno if this is a thing. - isoToEquiv : A A≅ B → A ≃ B - isoToEquiv = {!!} - -- Add proof of being a set to both sides of an equality. - addP : A ≡ B → hA ≡ hB - addP p = lemSig (λ X → propPi λ x → propPi (λ y → propIsProp)) hA hB p - inverse : hA ≅ hB → hA ≡ hB - inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE + univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent[Contr] = subst {P = isContr} (sym eq1) tres + where + module _ (y : Σ[ hB ∈ Object ] hA ≡ hB) where + open Σ y renaming (proj₁ to hB ; proj₂ to hA≡hB) + qres : (hA , refl) ≡ (hB , hA≡hB) + qres = contrSingl hA≡hB - -- open AreInverses (proj₂ (proj₂ univIso)) renaming - -- ( verso-recto to verso-recto' - -- ; recto-verso to recto-verso' - -- ) - -- I can just open them but I wanna be able to see the type annotations. - verso-recto' : inverse' ∘ obverse' ≡ Function.id - verso-recto' = AreInverses.verso-recto (proj₂ (proj₂ univIso)) - recto-verso' : obverse' ∘ inverse' ≡ Function.id - recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso)) - verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso - verso-recto iso = begin - obverse (inverse iso) ≡⟨⟩ - ( addE ∘ _≃_.toIsomorphism - ∘ obverse' ∘ dropP ∘ addP - ∘ inverse' ∘ isoToEquiv - ∘ dropE) iso - ≡⟨⟩ - ( addE ∘ _≃_.toIsomorphism - ∘ obverse' - ∘ inverse' ∘ isoToEquiv - ∘ dropE) iso - ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses - ( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso - ≡⟨ {!!} ⟩ -- should be easy to prove - -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id - (addE ∘ dropE) iso - ≡⟨⟩ - iso ∎ + tres : isContr (Σ[ hB ∈ Object ] hA ≡ hB) + tres = (hA , refl) , qres - -- Similar to above. - recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq - recto-verso eq = begin - inverse (obverse eq) ≡⟨ {!!} ⟩ - eq ∎ - - -- Use the fact that being an h-level is a mere proposition. - -- This is almost provable using `Wishlist.isSetIsProp` - although - -- this creates homogenous paths. - isSetEq : (p : A ≡ B) → (λ i → isSet (p i)) [ isSetA ≡ isSetB ] - isSetEq = {!!} - - res : hA ≡ hB - proj₁ (res i) = {!!} - proj₂ (res i) = isSetEq {!!} i - univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = {!gradLemma obverse inverse verso-recto recto-verso!} + univalent : Univalent + univalent = from[Contr] univalent[Contr] SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl @@ -179,39 +302,35 @@ module _ {ℓ : Level} where open Category 𝓢 open import Cubical.Sigma - module _ (0A 0B : Object) where + module _ (hA hB : Object) where + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) + private - A : Set ℓ - A = proj₁ 0A - sA : isSet A - sA = proj₂ 0A - B : Set ℓ - B = proj₁ 0B - sB : isSet B - sB = proj₂ 0B - 0A×0B : Object - 0A×0B = (A × B) , sigPresSet sA λ _ → sB + productObject : Object + productObject = (A × B) , sigPresSet sA λ _ → sB module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where _&&&_ : (X → A × B) _&&&_ x = f x , g x - module _ {0X : Object} where - X = proj₁ 0X - module _ (f : X → A ) (g : X → B) where - lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g - proj₁ lem = refl - proj₂ lem = refl - rawProduct : RawProduct 𝓢 0A 0B - RawProduct.object rawProduct = 0A×0B + module _ (hX : Object) where + open Σ hX renaming (proj₁ to X) + module _ (f : X → A ) (g : X → B) where + ump : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g + proj₁ ump = refl + proj₂ ump = refl + + rawProduct : RawProduct 𝓢 hA hB + RawProduct.object rawProduct = productObject RawProduct.proj₁ rawProduct = Data.Product.proj₁ RawProduct.proj₂ rawProduct = Data.Product.proj₂ isProduct : IsProduct 𝓢 _ _ rawProduct - IsProduct.isProduct isProduct {X = X} f g - = (f &&& g) , lem {0X = X} f g + IsProduct.ump isProduct {X = hX} f g + = (f &&& g) , ump hX f g - product : Product 𝓢 0A 0B + product : Product 𝓢 hA hB Product.raw product = rawProduct Product.isProduct product = isProduct @@ -220,6 +339,8 @@ module _ {ℓ : Level} where SetsHasProducts = record { product = product } module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + open Category ℂ + -- Covariant Presheaf Representable : Set (ℓa ⊔ lsuc ℓb) Representable = Functor ℂ (𝓢𝓮𝓽 ℓb) @@ -228,8 +349,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Presheaf : Set (ℓa ⊔ lsuc ℓb) Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb) - open Category ℂ - -- The "co-yoneda" embedding. representable : Category.Object ℂ → Representable representable A = record @@ -238,7 +357,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; fmap = ℂ [_∘_] } ; isFunctor = record - { isIdentity = funExt λ _ → proj₂ isIdentity + { isIdentity = funExt λ _ → leftIdentity ; isDistributive = funExt λ x → sym isAssociative } } @@ -251,7 +370,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; fmap = λ f g → ℂ [ g ∘ f ] } ; isFunctor = record - { isIdentity = funExt λ x → proj₁ isIdentity + { isIdentity = funExt λ x → rightIdentity ; isDistributive = funExt λ x → isAssociative } } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 5b2f025..70eb654 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -28,37 +28,17 @@ module Cat.Category where -open import Agda.Primitive -open import Data.Unit.Base -open import Data.Product renaming +open import Cat.Prelude + renaming ( proj₁ to fst ; proj₂ to snd - ; ∃! to ∃!≈ ) -open import Data.Empty -import Function -open import Cubical -open import Cubical.NType.Properties using ( propIsEquiv ; lemPropF ) -open import Cat.Wishlist +import Function ------------------ --- * Utilities -- ------------------ - --- | Unique existensials. -∃! : ∀ {a b} {A : Set a} - → (A → Set b) → Set (a ⊔ b) -∃! = ∃!≈ _≡_ - -∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) -∃!-syntax = ∃ - -syntax ∃!-syntax (λ x → B) = ∃![ x ] B - ------------------ +------------------ -- * Categories -- ------------------ +------------------ -- | Raw categories -- @@ -96,7 +76,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb) IsIdentity id = {A B : Object} {f : Arrow A B} - → f ∘ id ≡ f × id ∘ f ≡ f + → id ∘ f ≡ f × f ∘ id ≡ f ArrowsAreSets : Set (ℓa ⊔ ℓb) ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) @@ -129,22 +109,34 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Terminal : Set (ℓa ⊔ ℓb) Terminal = Σ Object IsTerminal --- | Univalence is indexed by a raw category as well as an identity proof. --- --- FIXME Put this in `RawCategory` and index it on the witness to `isIdentity`. -module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where - open RawCategory ℂ - module _ (isIdentity : IsIdentity 𝟙) where + -- | Univalence is indexed by a raw category as well as an identity proof. + module Univalence (isIdentity : IsIdentity 𝟙) where + -- | The identity isomorphism idIso : (A : Object) → A ≅ A idIso A = 𝟙 , (𝟙 , isIdentity) - -- Lemma 9.1.4 in [HoTT] + -- | Extract an isomorphism from an equality + -- + -- [HoTT §9.1.4] id-to-iso : (A B : Object) → A ≡ B → A ≅ B id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A) Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) + -- A perhaps more readable version of univalence: + Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B) + + -- | 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 + -- + -- This is not so straight-forward so you can assume it + postulate from[Contr] : Univalent[Contr] → Univalent + -- | The mere proposition of being a category. -- -- Also defines a few lemmas: @@ -156,52 +148,59 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where -- [HoTT]. record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where open RawCategory ℂ public - open Univalence ℂ public field isAssociative : IsAssociative isIdentity : IsIdentity 𝟙 arrowsAreSets : ArrowsAreSets - univalent : Univalent isIdentity + open Univalence isIdentity public + field + univalent : Univalent - -- Some common lemmas about categories. + leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f + leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) + + rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f + rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) + + ------------ + -- Lemmas -- + ------------ + + -- | Relation between iso- epi- and mono- morphisms. module _ {A B : Object} {X : Object} (f : Arrow A B) where - iso-is-epi : Isomorphism f → Epimorphism {X = X} f - iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin - g₀ ≡⟨ sym (fst isIdentity) ⟩ + iso→epi : Isomorphism f → Epimorphism {X = X} f + iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin + g₀ ≡⟨ sym rightIdentity ⟩ g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ (g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ - g₁ ∘ 𝟙 ≡⟨ fst isIdentity ⟩ + g₁ ∘ 𝟙 ≡⟨ rightIdentity ⟩ g₁ ∎ - iso-is-mono : Isomorphism f → Monomorphism {X = X} f - iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = + iso→mono : Isomorphism f → Monomorphism {X = X} f + iso→mono (f- , left-inv , right-inv) g₀ g₁ eq = begin - g₀ ≡⟨ sym (snd isIdentity) ⟩ + g₀ ≡⟨ sym leftIdentity ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ - 𝟙 ∘ g₁ ≡⟨ snd isIdentity ⟩ + 𝟙 ∘ g₁ ≡⟨ leftIdentity ⟩ g₁ ∎ - iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f - iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso + iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f + iso→epi×mono iso = iso→epi iso , iso→mono iso --- | Propositionality of being a category --- --- Proves that all projections of `IsCategory` are mere propositions as well as --- `IsCategory` itself being a mere proposition. -module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where - open RawCategory ℂ - module _ (ℂ : IsCategory ℂ) where - open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent) - open import Cubical.NType - open import Cubical.NType.Properties + -- | The formulation of univalence expressed with _≃_ is trivially admissable - + -- just "forget" the equivalence. + univalent≃ : Univalent≃ + univalent≃ = _ , univalent + -- | All projections are propositions. + module Propositionality where propIsAssociative : isProp IsAssociative propIsAssociative x y i = arrowsAreSets _ _ x y i @@ -227,31 +226,34 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = lemSig (λ g → propIsInverseOf) a a' geq where - open Cubical.NType.Properties geq : g ≡ g' geq = begin - g ≡⟨ sym (fst isIdentity) ⟩ + g ≡⟨ sym rightIdentity ⟩ g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ - 𝟙 ∘ g' ≡⟨ snd isIdentity ⟩ + 𝟙 ∘ g' ≡⟨ leftIdentity ⟩ g' ∎ - propUnivalent : isProp (Univalent isIdentity) - propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i + propUnivalent : isProp Univalent + propUnivalent a b i = propPi (λ iso → propIsContr) a b i +-- | Propositionality of being a category +module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where + open RawCategory ℂ + open Univalence private module _ (x y : IsCategory ℂ) where - module IC = IsCategory module X = IsCategory x module Y = IsCategory y - open Univalence ℂ -- In a few places I use the result of propositionality of the various - -- projections of `IsCategory` - I've arbitrarily chosed to use this + -- projections of `IsCategory` - Here I arbitrarily chose to use this -- result from `x : IsCategory C`. I don't know which (if any) possibly -- adverse effects this may have. + module Prop = X.Propositionality + isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ] - isIdentity = propIsIdentity x X.isIdentity Y.isIdentity + isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ] → (b : Univalent a) @@ -264,16 +266,16 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where P y eq = ∀ (univ : Univalent y) → U eq univ p : ∀ (b' : Univalent X.isIdentity) → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ] - p univ = propUnivalent x X.univalent univ + p univ = Prop.propUnivalent X.univalent univ helper : P Y.isIdentity isIdentity helper = pathJ P p Y.isIdentity isIdentity eqUni : U isIdentity Y.univalent eqUni = helper Y.univalent done : x ≡ y - IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i - IC.isIdentity (done i) = isIdentity i - IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i - IC.univalent (done i) = eqUni i + IsCategory.isAssociative (done i) = Prop.propIsAssociative X.isAssociative Y.isAssociative i + IsCategory.isIdentity (done i) = isIdentity i + IsCategory.arrowsAreSets (done i) = Prop.propArrowIsSet X.arrowsAreSets Y.arrowsAreSets i + IsCategory.univalent (done i) = eqUni i propIsCategory : isProp (IsCategory ℂ) propIsCategory = done @@ -298,7 +300,7 @@ module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where private isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ] - isCategoryEq = lemPropF Propositionality.propIsCategory rawEq + isCategoryEq = lemPropF propIsCategory rawEq Category≡ : ℂ ≡ 𝔻 Category≡ i = record @@ -330,21 +332,22 @@ module Opposite {ℓa ℓb : Level} where RawCategory._∘_ opRaw = Function.flip ℂ._∘_ open RawCategory opRaw - open Univalence opRaw isIdentity : IsIdentity 𝟙 isIdentity = swap ℂ.isIdentity + open Univalence isIdentity + module _ {A B : ℂ.Object} where univalent : isEquiv (A ≡ B) (A ≅ B) - (id-to-iso (swap ℂ.isIdentity) A B) + (Univalence.id-to-iso (swap ℂ.isIdentity) A B) fst (univalent iso) = flipFiber (fst (ℂ.univalent (flipIso iso))) where flipIso : A ≅ B → B ℂ.≅ A flipIso (f , f~ , iso) = f , f~ , swap iso flipFiber - : fiber (ℂ.id-to-iso ℂ.isIdentity B A) (flipIso iso) - → fiber ( id-to-iso isIdentity A B) iso + : fiber (ℂ.id-to-iso B A) (flipIso iso) + → fiber ( id-to-iso A B) iso flipFiber (eq , eqIso) = sym eq , {!!} snd (univalent iso) = {!!} diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda index 87769f6..76652d2 100644 --- a/src/Cat/Category/Exponential.agda +++ b/src/Cat/Category/Exponential.agda @@ -1,8 +1,6 @@ module Cat.Category.Exponential where -open import Agda.Primitive -open import Data.Product hiding (_×_) -open import Cubical +open import Cat.Prelude hiding (_×_) open import Cat.Category open import Cat.Category.Product diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index fc23c2e..390d8bc 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -2,9 +2,11 @@ module Cat.Category.Functor where open import Agda.Primitive -open import Cubical open import Function +open import Cubical +open import Cubical.NType.Properties using (lemPropF) + open import Cat.Category open Category hiding (_∘_ ; raw ; IsIdentity) @@ -72,14 +74,12 @@ module _ {ℓc ℓc' ℓd ℓd'} open IsFunctor isFunctor public -open Functor - 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 @@ -87,7 +87,7 @@ module _ propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor isF0 isF1 i = record - { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i + { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i ; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i } where @@ -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 @@ -108,15 +107,14 @@ module _ IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} (\ F → propIsFunctor F) (\ i → F i) - where - open import Cubical.NType.Properties using (lemPropF) -module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where +module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where + open Functor Functor≡ : {F G : Functor ℂ 𝔻} - → raw F ≡ raw G + → Functor.raw F ≡ Functor.raw G → F ≡ G - raw (Functor≡ eq i) = eq i - isFunctor (Functor≡ {F} {G} eq i) + Functor.raw (Functor≡ eq i) = eq i + Functor.isFunctor (Functor≡ {F} {G} eq i) = res i where res : (λ i → IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ] @@ -124,35 +122,37 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private - F* = omap F - F→ = fmap F - G* = omap G - G→ = fmap G + module F = Functor F + module G = Functor G module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where - - dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] + dist : (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) ≡ C [ (F.fmap ∘ G.fmap) α1 ∘ (F.fmap ∘ G.fmap) α0 ] dist = begin - (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ - F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (isDistributive G) ⟩ - F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ isDistributive F ⟩ - C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ + (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) + ≡⟨ refl ⟩ + F.fmap (G.fmap (A [ α1 ∘ α0 ])) + ≡⟨ cong F.fmap G.isDistributive ⟩ + F.fmap (B [ G.fmap α1 ∘ G.fmap α0 ]) + ≡⟨ F.isDistributive ⟩ + C [ (F.fmap ∘ G.fmap) α1 ∘ (F.fmap ∘ G.fmap) α0 ] + ∎ - _∘fr_ : RawFunctor A C - RawFunctor.omap _∘fr_ = F* ∘ G* - RawFunctor.fmap _∘fr_ = F→ ∘ G→ - instance - isFunctor' : IsFunctor A C _∘fr_ - isFunctor' = record - { isIdentity = begin - (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ - F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩ - F→ (𝟙 B) ≡⟨ isIdentity F ⟩ - 𝟙 C ∎ - ; isDistributive = dist - } + raw : RawFunctor A C + RawFunctor.omap raw = F.omap ∘ G.omap + RawFunctor.fmap raw = F.fmap ∘ G.fmap + + isFunctor : IsFunctor A C raw + isFunctor = record + { isIdentity = begin + (F.fmap ∘ G.fmap) (𝟙 A) ≡⟨ refl ⟩ + F.fmap (G.fmap (𝟙 A)) ≡⟨ cong F.fmap (G.isIdentity)⟩ + F.fmap (𝟙 B) ≡⟨ F.isIdentity ⟩ + 𝟙 C ∎ + ; isDistributive = dist + } F[_∘_] : Functor A C - raw F[_∘_] = _∘fr_ + Functor.raw F[_∘_] = raw + Functor.isFunctor F[_∘_] = isFunctor -- The identity functor identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 2f42f32..3b65149 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -20,23 +20,19 @@ The monoidal representation is exposed by default from this module. {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Category.Monad where -open import Agda.Primitive - -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) - +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad.Monoidal as Monoidal public -open import Cat.Category.Monad.Kleisli as Kleisli +import Cat.Category.Monad.Monoidal +import Cat.Category.Monad.Kleisli open import Cat.Categories.Fun +module Monoidal = Cat.Category.Monad.Monoidal +module Kleisli = Cat.Category.Monad.Kleisli + -- | The monoidal- and kleisli presentation of monads are equivalent. -module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private module ℂ = Category ℂ open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_) @@ -121,7 +117,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where bind (f >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩ bind (f >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind f ∎ forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m @@ -152,7 +148,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where KM.bind 𝟙 ≡⟨⟩ bind 𝟙 ≡⟨⟩ joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩ + joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎ fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap @@ -164,7 +160,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩ - 𝟙 ∘ Rfmap f ≡⟨ proj₂ ℂ.isIdentity ⟩ + 𝟙 ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ Rfmap f ∎ ) @@ -189,7 +185,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩ KM.join ≡⟨⟩ joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩ + joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎) joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i)) @@ -207,5 +203,10 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where eqv : isEquiv M.Monad K.Monad forth eqv = gradLemma forth back fortheq backeq + open import Cat.Equivalence + + Monoidal≅Kleisli : M.Monad ≅ K.Monad + Monoidal≅Kleisli = forth , (back , (record { verso-recto = funExt backeq ; recto-verso = funExt fortheq })) + Monoidal≃Kleisli : M.Monad ≃ K.Monad Monoidal≃Kleisli = forth , eqv diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index 8f96b82..7377cdf 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -4,11 +4,7 @@ The Kleisli formulation of monads {-# OPTIONS --cubical --allow-unsolved-metas #-} open import Agda.Primitive -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F @@ -104,7 +100,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where isFunctorR : IsFunctor ℂ ℂ rawR IsFunctor.isIdentity isFunctorR = begin - bind (pure ∘ 𝟙) ≡⟨ cong bind (proj₁ ℂ.isIdentity) ⟩ + bind (pure ∘ 𝟙) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ bind pure ≡⟨ isIdentity ⟩ 𝟙 ∎ @@ -156,9 +152,9 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (bind (f >>> pure) >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩ bind (bind (f >>> pure) >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind (bind (f >>> pure)) - ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩ + ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩ bind (𝟙 >=> (f >>> pure)) ≡⟨ sym (isDistributive _ _) ⟩ @@ -186,10 +182,10 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (join >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩ bind (join >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind join ≡⟨⟩ bind (bind 𝟙) - ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩ + ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ bind (𝟙 >>> bind 𝟙) ≡⟨⟩ bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _) ⟩ bind 𝟙 >>> bind 𝟙 ≡⟨⟩ @@ -212,7 +208,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (pure >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩ bind (pure >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind pure ≡⟨ isIdentity ⟩ 𝟙 ∎ diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index b969187..360e5df 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -4,11 +4,7 @@ Monoidal formulation of monads {-# OPTIONS --cubical --allow-unsolved-metas #-} open import Agda.Primitive -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F @@ -75,8 +71,8 @@ record IsMonad (raw : RawMonad) : Set ℓ where joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩ joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩ joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩ - 𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩ - f ∎ + 𝟙 ∘ f ≡⟨ ℂ.leftIdentity ⟩ + f ∎ isDistributive : IsDistributive isDistributive {X} {Y} {Z} g f = sym aux diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index a9447f9..f30aa9a 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -4,22 +4,15 @@ This module provides construction 2.3 in [voe] {-# OPTIONS --cubical --allow-unsolved-metas --caching #-} module Cat.Category.Monad.Voevodsky where -open import Agda.Primitive - -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude +open import Function open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad using (Monoidal≃Kleisli) -import Cat.Category.Monad.Monoidal as Monoidal -import Cat.Category.Monad.Kleisli as Kleisli +open import Cat.Category.Monad open import Cat.Categories.Fun -open import Function using (_∘′_) +open import Cat.Equivalence module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private @@ -27,11 +20,10 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where module ℂ = Category ℂ open ℂ using (Object ; Arrow) open NaturalTransformation ℂ ℂ - open import Function using (_∘_ ; _$_) module M = Monoidal ℂ module K = Kleisli ℂ - module §2-3 (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where + module §2-3 (omap : Object → Object) (pure : {X : Object} → Arrow X (omap X)) where record §1 : Set ℓ where open M @@ -134,13 +126,23 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; isMnd = K.Monad.isMonad m } + -- | In the following we seek to transform the equivalence `Monoidal≃Kleisli` + -- | to talk about voevodsky's construction. module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where private + module E = AreInverses (Monoidal≅Kleisli ℂ .proj₂ .proj₂) + Monoidal→Kleisli : M.Monad → K.Monad - Monoidal→Kleisli = proj₁ Monoidal≃Kleisli + Monoidal→Kleisli = E.obverse Kleisli→Monoidal : K.Monad → M.Monad - Kleisli→Monoidal = inverse Monoidal≃Kleisli + Kleisli→Monoidal = E.reverse + + ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id + ve-re = E.verso-recto + + re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id + re-ve = E.recto-verso forth : §2-3.§1 omap pure → §2-3.§2 omap pure forth = §2-fromMonad ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad @@ -163,7 +165,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ∘ Monoidal→Kleisli ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad - ) m ≡⟨ u ⟩ + ) 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 @@ -174,23 +176,18 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id - lem = {!!} -- verso-recto Monoidal≃Kleisli t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure}) ≡ §2-3.§2.toMonad - t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) lem - cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A} → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y) + cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A} + → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y) cong-d f p = λ i → f (p i) + 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 (\ f → f m) t -{- -(K.RawMonad.omap (K.Monad.raw (?0 ℂ omap pure m i (§2-3.§2.toMonad m))) x) = (omap x) : Object -(K.RawMonad.pure (K.Monad.raw (?0 ℂ omap pure m x (§2-3.§2.toMonad x)))) = pure : Arrow X (_350 ℂ omap pure m x x X) --} + u = cong (\ φ → φ m) t backEq : ∀ m → (back ∘ forth) m ≡ m backEq m = begin @@ -212,7 +209,10 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso 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 i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m)) voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth voe-isEquiv = gradLemma forth back forthEq backEq diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda index a17468e..75eaa68 100644 --- a/src/Cat/Category/Monoid.agda +++ b/src/Cat/Category/Monoid.agda @@ -19,7 +19,7 @@ module _ (ℓa ℓb : Level) where -- -- Since it doesn't we'll make the following (definitionally equivalent) ad-hoc definition. _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb - ℂ × 𝔻 = Cat.CatProduct.obj ℂ 𝔻 + ℂ × 𝔻 = Cat.CatProduct.object ℂ 𝔻 record RawMonoidalCategory : Set ℓ where field diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index dea2e50..13e3d89 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -19,15 +19,12 @@ -- * A composition operator. {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category.NaturalTransformation where -open import Agda.Primitive -open import Data.Product + +open import Cat.Prelude + open import Data.Nat using (_≤_ ; z≤n ; s≤s) module Nat = Data.Nat -open import Cubical -open import Cubical.Sigma -open import Cubical.NType.Properties - open import Cat.Category open import Cat.Category.Functor hiding (identity) open import Cat.Wishlist @@ -72,8 +69,8 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩ - F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩ + 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩ + F→ f ≡⟨ sym 𝔻.rightIdentity ⟩ 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where @@ -113,8 +110,11 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i - naturalTransformationIsSet : isSet (NaturalTransformation F G) - naturalTransformationIsSet = sigPresSet transformationIsSet - λ θ → ntypeCommulative + naturalIsSet : (θ : Transformation F G) → isSet (Natural F G θ) + naturalIsSet θ = + ntypeCommulative (s≤s {n = Nat.suc Nat.zero} z≤n) (naturalIsProp θ) + + naturalTransformationIsSet : isSet (NaturalTransformation F G) + naturalTransformationIsSet = sigPresSet transformationIsSet naturalIsSet diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index dff488a..1ce45c5 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -1,11 +1,10 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Category.Product where -open import Agda.Primitive -open import Cubical -open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂) +open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂) +import Data.Product as P -open import Cat.Category hiding (module Propositionality) +open import Cat.Category module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where @@ -24,13 +23,13 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where open RawProduct raw public field - isProduct : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) + ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) → ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g) -- | Arrow product _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ]) → ℂ [ X , object ] - _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂) + _P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂) record Product : Set (ℓa ⊔ ℓb) where field @@ -59,10 +58,63 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where × ℂ [ g ∘ snd ] ] -module Propositionality {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where - -- TODO I'm not sure this is actually provable. Check with Thierry. - propProduct : isProp (Product ℂ A B) - propProduct = {!!} +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where + private + open Category ℂ + module _ (raw : RawProduct ℂ A B) where + module _ (x y : IsProduct ℂ A B raw) where + private + module x = IsProduct x + module y = IsProduct y + + module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where + prodAux : x.ump f g ≡ y.ump f g + prodAux = {!!} + + propIsProduct' : x ≡ y + propIsProduct' i = record { ump = λ f g → prodAux f g i } + + propIsProduct : isProp (IsProduct ℂ A B raw) + propIsProduct = propIsProduct' + + Product≡ : {x y : Product ℂ A B} → (Product.raw x ≡ Product.raw y) → x ≡ y + Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i } + where + q : (λ i → IsProduct ℂ A B (p i)) [ Product.isProduct x ≡ Product.isProduct y ] + q = lemPropF propIsProduct p + +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where + open Category ℂ + private + module _ (x y : HasProducts ℂ) where + private + module x = HasProducts x + module y = HasProducts y + module _ (A B : Object) where + module pX = Product (x.product A B) + module pY = Product (y.product A B) + objEq : pX.object ≡ pY.object + objEq = {!!} + proj₁Eq : (λ i → ℂ [ objEq i , A ]) [ pX.proj₁ ≡ pY.proj₁ ] + proj₁Eq = {!!} + proj₂Eq : (λ i → ℂ [ objEq i , B ]) [ pX.proj₂ ≡ pY.proj₂ ] + proj₂Eq = {!!} + rawEq : pX.raw ≡ pY.raw + RawProduct.object (rawEq i) = objEq i + RawProduct.proj₁ (rawEq i) = {!!} + RawProduct.proj₂ (rawEq i) = {!!} + + isEq : (λ i → IsProduct ℂ A B (rawEq i)) [ pX.isProduct ≡ pY.isProduct ] + isEq = {!!} + + appEq : x.product A B ≡ y.product A B + appEq = Product≡ rawEq + + productEq : x.product ≡ y.product + productEq i = λ A B → appEq A B i + + propHasProducts' : x ≡ y + propHasProducts' i = record { product = productEq i } propHasProducts : isProp (HasProducts ℂ) - propHasProducts = {!!} + propHasProducts = propHasProducts' diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index af7567a..47ac1ec 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -2,61 +2,61 @@ module Cat.Category.Yoneda where -open import Agda.Primitive -open import Data.Product -open import Cubical -open import Cubical.NType.Properties +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor -open import Cat.Equality open import Cat.Categories.Fun -open import Cat.Categories.Sets -open import Cat.Categories.Cat +open import Cat.Categories.Sets hiding (presheaf) + +-- There is no (small) category of categories. So we won't use _⇑_ from +-- `HasExponential` +-- +-- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_) +-- +-- In stead we'll use an ad-hoc definition -- which is definitionally equivalent +-- to that other one - even without mentioning the category of categories. +_⇑_ : {ℓ : Level} → Category ℓ ℓ → Category ℓ ℓ → Category ℓ ℓ +_⇑_ = Fun.Fun module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where private 𝓢 = Sets ℓ open Fun (opposite ℂ) 𝓢 - prshf = presheaf ℂ + module ℂ = Category ℂ - -- There is no (small) category of categories. So we won't use _⇑_ from - -- `HasExponential` - -- - -- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_) - -- - -- In stead we'll use an ad-hoc definition -- which is definitionally - -- equivalent to that other one. - _⇑_ = CatExponential.object + presheaf : ℂ.Object → Presheaf ℂ + presheaf = Cat.Categories.Sets.presheaf ℂ module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where - fmap : Transformation (prshf A) (prshf B) + fmap : Transformation (presheaf A) (presheaf B) fmap C x = ℂ [ f ∘ x ] - fmapNatural : Natural (prshf A) (prshf B) fmap + fmapNatural : Natural (presheaf A) (presheaf B) fmap fmapNatural g = funExt λ _ → ℂ.isAssociative - fmapNT : NaturalTransformation (prshf A) (prshf B) + fmapNT : NaturalTransformation (presheaf A) (presheaf B) fmapNT = fmap , fmapNatural rawYoneda : RawFunctor ℂ Fun - RawFunctor.omap rawYoneda = prshf + RawFunctor.omap rawYoneda = presheaf RawFunctor.fmap rawYoneda = fmapNT + open RawFunctor rawYoneda hiding (fmap) isIdentity : IsIdentity - isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq + isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq where - eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) - eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity + eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c) + eq = funExt λ A → funExt λ B → ℂ.leftIdentity isDistributive : IsDistributive isDistributive {A} {B} {C} {f = f} {g} - = lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq + = lemSig (propIsNatural (presheaf A) (presheaf C)) _ _ eq where - T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C} + T[_∘_]' = T[_∘_] {F = presheaf A} {presheaf B} {presheaf C} eqq : (X : ℂ.Object) → (x : ℂ [ X , A ]) → fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x eqq X x = begin @@ -76,5 +76,5 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where IsFunctor.isDistributive isFunctor = isDistributive yoneda : Functor ℂ Fun - Functor.raw yoneda = rawYoneda + Functor.raw yoneda = rawYoneda Functor.isFunctor yoneda = isFunctor diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda deleted file mode 100644 index d6b3dc0..0000000 --- a/src/Cat/Equality.agda +++ /dev/null @@ -1,22 +0,0 @@ -{-# OPTIONS --cubical #-} --- Defines equality-principles for data-types from the standard library. - -module Cat.Equality where - -open import Level -open import Cubical - --- _[_≡_] = PathP - -module Equality where - module Data where - module Product where - open import Data.Product - - module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} - (proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ]) - (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where - - Σ≡ : a ≡ b - proj₁ (Σ≡ i) = proj₁≡ i - proj₂ (Σ≡ i) = proj₂≡ i diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda new file mode 100644 index 0000000..b63e4ec --- /dev/null +++ b/src/Cat/Equivalence.agda @@ -0,0 +1,290 @@ +{-# OPTIONS --allow-unsolved-metas --cubical #-} +module Cat.Equivalence where + +open import Cubical.Primitives +open import Cubical.FromStdLib renaming (ℓ-max to _⊔_) +open import Cubical.PathPrelude hiding (inverse ; _≃_) +open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public +open import Cubical.GradLemma + +module _ {ℓa ℓb : Level} where + private + ℓ = ℓa ⊔ ℓb + + module _ {A : Set ℓa} {B : Set ℓb} where + -- Quasi-inverse in [HoTT] §2.4.6 + -- FIXME Maybe rename? + record AreInverses (f : A → B) (g : B → A) : Set ℓ where + field + verso-recto : g ∘ f ≡ idFun A + recto-verso : f ∘ g ≡ idFun B + obverse = f + reverse = g + inverse = reverse + toPair : Σ _ _ + toPair = verso-recto , recto-verso + + Isomorphism : (f : A → B) → Set _ + Isomorphism f = Σ (B → A) λ g → AreInverses f g + + module _ {f : A → B} {g : B → A} + (inv : (g ∘ f) ≡ idFun A + × (f ∘ g) ≡ idFun B) where + open Σ inv renaming (fst to ve-re ; snd to re-ve) + toAreInverses : AreInverses f g + toAreInverses = record + { verso-recto = ve-re + ; recto-verso = re-ve + } + + _≅_ : Set ℓa → Set ℓb → Set _ + A ≅ B = Σ (A → B) Isomorphism + +module _ {ℓ : Level} {A B : Set ℓ} {f : A → B} + (g : B → A) (s : {A B : Set ℓ} → isSet (A → B)) where + + propAreInverses : isProp (AreInverses {A = A} {B} f g) + propAreInverses x y i = record + { verso-recto = ve-re + ; recto-verso = re-ve + } + where + open AreInverses + ve-re : g ∘ f ≡ idFun A + ve-re = s (g ∘ f) (idFun A) (verso-recto x) (verso-recto y) i + re-ve : f ∘ g ≡ idFun B + re-ve = s (f ∘ g) (idFun B) (recto-verso x) (recto-verso y) i + +-- In HoTT they generalize an equivalence to have the following 3 properties: +module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where + record Equiv (iseqv : (A → B) → Set ℓ) : Set (ℓa ⊔ ℓb ⊔ ℓ) where + field + fromIso : {f : A → B} → Isomorphism f → iseqv f + toIso : {f : A → B} → iseqv f → Isomorphism f + propIsEquiv : (f : A → B) → isProp (iseqv f) + + -- You're alerady assuming here that we don't need eta-equality on the + -- equivalence! + _~_ : Set ℓa → Set ℓb → Set _ + A ~ B = Σ _ iseqv + + inverse-from-to-iso : ∀ {f} (x : _) → (fromIso {f} ∘ toIso {f}) x ≡ x + inverse-from-to-iso x = begin + (fromIso ∘ toIso) x ≡⟨⟩ + fromIso (toIso x) ≡⟨ propIsEquiv _ (fromIso (toIso x)) x ⟩ + x ∎ + + -- `toIso` is abstract - so I probably can't close this proof. + module _ (sA : isSet A) (sB : isSet B) where + module _ {f : A → B} (iso : Isomorphism f) where + module _ (iso-x iso-y : Isomorphism f) where + open Σ iso-x renaming (fst to x ; snd to inv-x) + open Σ iso-y renaming (fst to y ; snd to inv-y) + module inv-x = AreInverses inv-x + module inv-y = AreInverses inv-y + + fx≡fy : x ≡ y + fx≡fy = begin + x ≡⟨ cong (λ φ → x ∘ φ) (sym inv-y.recto-verso) ⟩ + x ∘ (f ∘ y) ≡⟨⟩ + (x ∘ f) ∘ y ≡⟨ cong (λ φ → φ ∘ y) inv-x.verso-recto ⟩ + y ∎ + + open import Cat.Prelude + + propInv : ∀ g → isProp (AreInverses f g) + propInv g t u i = record { verso-recto = a i ; recto-verso = b i } + where + module t = AreInverses t + module u = AreInverses u + a : t.verso-recto ≡ u.verso-recto + a i = h + where + hh : ∀ a → (g ∘ f) a ≡ a + hh a = sA ((g ∘ f) a) a (λ i → t.verso-recto i a) (λ i → u.verso-recto i a) i + h : g ∘ f ≡ idFun A + h i a = hh a i + b : t.recto-verso ≡ u.recto-verso + b i = h + where + hh : ∀ b → (f ∘ g) b ≡ b + hh b = sB _ _ (λ i → t.recto-verso i b) (λ i → u.recto-verso i b) i + h : f ∘ g ≡ idFun B + h i b = hh b i + + inx≡iny : (λ i → AreInverses f (fx≡fy i)) [ inv-x ≡ inv-y ] + inx≡iny = lemPropF propInv fx≡fy + + propIso : iso-x ≡ iso-y + propIso i = fx≡fy i , inx≡iny i + + inverse-to-from-iso : (toIso {f} ∘ fromIso {f}) iso ≡ iso + inverse-to-from-iso = begin + (toIso ∘ fromIso) iso ≡⟨⟩ + toIso (fromIso iso) ≡⟨ propIso _ _ ⟩ + iso ∎ + + fromIsomorphism : A ≅ B → A ~ B + fromIsomorphism (f , iso) = f , fromIso iso + + toIsomorphism : A ~ B → A ≅ B + toIsomorphism (f , eqv) = f , toIso eqv + +module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where + -- A wrapper around PathPrelude.≃ + open Cubical.PathPrelude using (_≃_ ; isEquiv) + private + module _ {obverse : A → B} (e : isEquiv A B obverse) where + inverse : B → A + inverse b = fst (fst (e b)) + + reverse : B → A + reverse = inverse + + areInverses : AreInverses obverse inverse + areInverses = record + { verso-recto = funExt verso-recto + ; recto-verso = funExt recto-verso + } + where + recto-verso : ∀ b → (obverse ∘ inverse) b ≡ b + recto-verso b = begin + (obverse ∘ inverse) b ≡⟨ sym (μ b) ⟩ + b ∎ + where + μ : (b : B) → b ≡ obverse (inverse b) + μ b = snd (fst (e b)) + verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a + verso-recto a = begin + (inverse ∘ obverse) a ≡⟨ sym h ⟩ + a' ≡⟨ u' ⟩ + a ∎ + where + c : isContr (fiber obverse (obverse a)) + c = e (obverse a) + fbr : fiber obverse (obverse a) + fbr = fst c + a' : A + a' = fst fbr + allC : (y : fiber obverse (obverse a)) → fbr ≡ y + allC = snd c + k : fbr ≡ (inverse (obverse a), _) + k = allC (inverse (obverse a) , sym (recto-verso (obverse a))) + h : a' ≡ inverse (obverse a) + h i = fst (k i) + u : fbr ≡ (a , refl) + u = allC (a , refl) + u' : a' ≡ a + u' i = fst (u i) + + iso : Isomorphism obverse + iso = reverse , areInverses + + toIsomorphism : {f : A → B} → isEquiv A B f → Isomorphism f + toIsomorphism = iso + + ≃isEquiv : Equiv A B (isEquiv A B) + Equiv.fromIso ≃isEquiv {f} (f~ , iso) = gradLemma f f~ rv vr + where + open AreInverses iso + rv : (b : B) → _ ≡ b + rv b i = recto-verso i b + vr : (a : A) → _ ≡ a + vr a i = verso-recto i a + Equiv.toIso ≃isEquiv = toIsomorphism + Equiv.propIsEquiv ≃isEquiv = P.propIsEquiv + where + import Cubical.NType.Properties as P + + module Equiv≃ where + open Equiv ≃isEquiv public + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + open Cubical.PathPrelude using (_≃_) + + -- Gives the quasi inverse from an equivalence. + module Equivalence (e : A ≃ B) where + open Equiv≃ A B public + private + iso : Isomorphism (fst e) + iso = snd (toIsomorphism e) + + open AreInverses (snd iso) public + + composeIso : {ℓc : Level} {C : Set ℓc} → (B ≅ C) → A ≅ C + composeIso {C = C} (g , g' , iso-g) = g ∘ obverse , inverse ∘ g' , inv + where + module iso-g = AreInverses iso-g + inv : AreInverses (g ∘ obverse) (inverse ∘ g') + AreInverses.verso-recto inv = begin + (inverse ∘ g') ∘ (g ∘ obverse) ≡⟨⟩ + (inverse ∘ (g' ∘ g) ∘ obverse) + ≡⟨ cong (λ φ → φ ∘ obverse) (cong (λ φ → inverse ∘ φ) iso-g.verso-recto) ⟩ + (inverse ∘ idFun B ∘ obverse) ≡⟨⟩ + (inverse ∘ obverse) ≡⟨ verso-recto ⟩ + idFun A ∎ + AreInverses.recto-verso inv = begin + g ∘ obverse ∘ inverse ∘ g' + ≡⟨ cong (λ φ → φ ∘ g') (cong (λ φ → g ∘ φ) recto-verso) ⟩ + g ∘ idFun B ∘ g' ≡⟨⟩ + g ∘ g' ≡⟨ iso-g.recto-verso ⟩ + idFun C ∎ + + compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C + compose {C = C} e = A≃C.fromIsomorphism is + where + module B≃C = Equiv≃ B C + module A≃C = Equiv≃ A C + is : A ≅ C + is = composeIso (B≃C.toIsomorphism e) + + symmetryIso : B ≅ A + symmetryIso + = inverse + , obverse + , record + { verso-recto = recto-verso + ; recto-verso = verso-recto + } + + symmetry : B ≃ A + symmetry = B≃A.fromIsomorphism symmetryIso + where + module B≃A = Equiv≃ B A + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + open import Cubical.PathPrelude renaming (_≃_ to _≃η_) + open import Cubical.Univalence using (_≃_) + + doEta : A ≃ B → A ≃η B + doEta (_≃_.con eqv isEqv) = eqv , isEqv + + deEta : A ≃η B → A ≃ B + deEta (eqv , isEqv) = _≃_.con eqv isEqv + +module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + open import Cubical.PathPrelude renaming (_≃_ to _≃η_) + open import Cubical.Univalence using (_≃_) + + module Equivalence′ (e : A ≃ B) where + open Equivalence (doEta e) hiding + ( toIsomorphism ; fromIsomorphism ; _~_ + ; compose ; symmetryIso ; symmetry ) public + + compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C + compose ee = deEta (Equivalence.compose (doEta e) (doEta ee)) + + symmetry : B ≃ A + symmetry = deEta (Equivalence.symmetry (doEta e)) + + -- fromIso : {f : A → B} → Isomorphism f → isEquiv f + -- fromIso = ? + + -- toIso : {f : A → B} → isEquiv f → Isomorphism f + -- toIso = ? + + fromIsomorphism : A ≅ B → A ≃ B + fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso) + + toIsomorphism : A ≃ B → A ≅ B + toIsomorphism (_≃_.con f eqv) = f , Equiv≃.toIso _ _ eqv diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda new file mode 100644 index 0000000..f561330 --- /dev/null +++ b/src/Cat/Prelude.agda @@ -0,0 +1,65 @@ +-- | Custom prelude for this module +module Cat.Prelude where + +open import Agda.Primitive public +-- FIXME Use: +-- open import Agda.Builtin.Sigma public +-- Rather than +open import Data.Product public + renaming (∃! to ∃!≈) + +-- TODO Import Data.Function under appropriate names. + +open import Cubical public +-- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper +-- module. +open import Cubical.GradLemma + using (gradLemma) + public +open import Cubical.NType + using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel) + public +open import Cubical.NType.Properties + using + ( lemPropF ; lemSig ; lemSigP ; isSetIsProp + ; propPi ; propHasLevel ; setPi ; propSet) + public + +propIsContr : {ℓ : Level} → {A : Set ℓ} → isProp (isContr A) +propIsContr = propHasLevel ⟨-2⟩ + +open import Cubical.Sigma using (setSig ; sigPresSet) public + +module _ (ℓ : Level) where + -- FIXME Ask if we can push upstream. + -- A redefinition of `Cubical.Universe` with an explicit parameter + _-type : TLevel → Set (lsuc ℓ) + n -type = Σ (Set ℓ) (HasLevel n) + + hSet : Set (lsuc ℓ) + hSet = ⟨0⟩ -type + + Prop : Set (lsuc ℓ) + Prop = ⟨-1⟩ -type + +----------------- +-- * Utilities -- +----------------- + +-- | Unique existensials. +∃! : ∀ {a b} {A : Set a} + → (A → Set b) → Set (a ⊔ b) +∃! = ∃!≈ _≡_ + +∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) +∃!-syntax = ∃ + +syntax ∃!-syntax (λ x → B) = ∃![ x ] B + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} + (proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ]) + (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where + + Σ≡ : a ≡ b + proj₁ (Σ≡ i) = proj₁≡ i + proj₂ (Σ≡ i) = proj₂≡ i