fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Merge branch 'dev'

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-22 14:52:01 +01:00
parent 41e2d02c8d 4ae898dfe0
commit 73c3b35631
30 changed files with 1344 additions and 641 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
BACKLOG.md
View file

@ -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 ✓

19
CHANGELOG.md
View file

@ -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.

3
Makefile
View file

@ -1,2 +1,5 @@
build: src/**.agda
agda src/Cat.agda
clean:
find src -name "*.agdai" -type f -delete

22
proposal/BACKLOG.md Normal file
View file

@ -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

177
proposal/halftime.tex Normal file
View file

@ -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.

6
proposal/macros.tex
View file

@ -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]}}

3
proposal/proposal.tex
View file

@ -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}

3
src/Cat.agda
View file

@ -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

144
src/Cat/Categories/Cat.agda
View file

@ -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
@ -72,11 +63,13 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
Obj = Object ℂ × Object 𝔻
module _ where
private
Obj = ℂ.Object × 𝔻.Object
Arr : Obj → Obj → Set ℓ'
Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
𝟙' : {o : Obj} → Arr o o
𝟙' = 𝟙 ℂ , 𝟙 𝔻
𝟙 : {o : Obj} → Arr o o
𝟙 = ℂ.𝟙 , 𝔻.𝟙
_∘_ :
{a b c : Obj} →
Arr b c →
@ -87,17 +80,19 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
rawProduct : RawCategory ℓ ℓ'
RawCategory.Object rawProduct = Obj
RawCategory.Arrow rawProduct = Arr
RawCategory.𝟙 rawProduct = 𝟙'
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 ] ) ]

5
src/Cat/Categories/Cube.agda
View file

@ -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.

19
src/Cat/Categories/CwF.agda
View file

@ -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 : ????

11
src/Cat/Categories/Fam.agda
View file

@ -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

85
src/Cat/Categories/Free.agda
View file

@ -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
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 = 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 }

26
src/Cat/Categories/Fun.agda
View file

@ -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,7 +61,9 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
}
open RawCategory RawFun
open Univalence RawFun
open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
private
module _ {A B : Functor ℂ 𝔻} where
module A = Functor A
module B = Functor 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

20
src/Cat/Categories/Rel.agda
View file

@ -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)

423
src/Cat/Categories/Sets.agda
View file

@ -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
open _≃_ e
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
fromIsomorphism : hA ≅ hB → A ≃ B
fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto)
-- 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
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
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
fwd : Σ (A → B) isIso → hA ≅ hB
fwd (f , g , inv) = f , g , inv.toPair
where
areeqv = proj₂ (proj₂ eqv)
asPair =
let module Inv = AreInverses areeqv
in Inv.verso-recto , Inv.recto-verso
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 }
obverse : hA ≡ hB → hA ≅ hB
obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
conclusion : (hA ≅ hB) ≃ (hA ≡ hB)
conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2
-- 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
univ≃ : (hA ≅ hB) ≃ (hA ≡ hB)
univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2
module _ (hA : Object) where
open Σ hA renaming (proj₁ to A)
eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
eq1 = ua (lem3 (\ hB → univ≃))
univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB)
univalent[Contr] = subst {P = isContr} (sym eq1) tres
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 }
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
-- 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
tres : isContr (Σ[ hB ∈ Object ] hA ≡ hB)
tres = (hA , refl) , qres
-- 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 ∎
-- 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
}
}

153
src/Cat/Category.agda
View file

@ -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
-----------------
-- * 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 <Thierry.Coquand@cse.gu.se>
-- 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) = {!!}

4
src/Cat/Category/Exponential.agda
View file

@ -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

66
src/Cat/Category/Functor.agda
View file

@ -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
@ -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
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→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩
F→ (𝟙 B) ≡⟨ isIdentity F ⟩
(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

31
src/Cat/Category/Monad.agda
View file

@ -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

18
src/Cat/Category/Monad/Kleisli.agda
View file

@ -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 ⟩
𝟙 ∎

8
src/Cat/Category/Monad/Monoidal.agda
View file

@ -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,7 +71,7 @@ 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 ≡⟨ ℂ.leftIdentity ⟩
f ∎
isDistributive : IsDistributive

52
src/Cat/Category/Monad/Voevodsky.agda
View file

@ -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

2
src/Cat/Category/Monoid.agda
View file

@ -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

22
src/Cat/Category/NaturalTransformation.agda
View file

@ -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

74
src/Cat/Category/Product.agda
View file

@ -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'

50
src/Cat/Category/Yoneda.agda
View file

@ -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

22
src/Cat/Equality.agda
View file

@ -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

290
src/Cat/Equivalence.agda Normal file
View file

@ -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

65
src/Cat/Prelude.agda Normal file
View file

@ -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