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-13 10:41:54 +01:00
parent 9c8bc1b1f4 6db2a3e5d4
commit 3ab88395dc
25 changed files with 1827 additions and 931 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
BACKLOG.md
View file

@ -1,9 +1,18 @@
Backlog
=======
Prove univalence for various categories
Prove postulates in `Cat.Wishlist`
`ntypeCommulative` might be there as well.
Prove that the opposite category is a category.
Prove univalence for the category of
* sets
* functors and natural transformations
Prove:
* `isProp (Product ...)`
* `isProp (HasProducts ...)`
* Functor ✓
* Applicative Functor ✗
@ -11,4 +20,11 @@ Prove postulates in `Cat.Wishlist`
* Monoidal functor ✗
* Tensorial strength ✗
* Category ✓
* Monoidal category ✗
* Monoidal category ✗
* Monad
* Monoidal monad ✓
* Kleisli monad ✓
* Problem 2.3 in voe
* 1st contruction ~ monoidal ✓
* 2nd contruction ~ klesli ✓
* 1st ≃ 2nd ✗

20
CHANGELOG.md
View file

@ -1,9 +1,27 @@
Changelog
=========
Version 1.4.0
-------------
Adds documentation to a number of modules.
Adds an "equality principle" for categories and monads.
Prove that `IsMonad` is a mere proposition.
Provides the yoneda embedding without relying on the existence of a category of
categories. This is acheived by providing some of the data needed to make a ccc
out of the category of categories without actually having such a category.
Renames functors object map and arrow map to `omap` and `fmap`.
Prove that kleisli- and monoidal- monads are equivalent!
[WIP] Started working on the proofs for univalence for the category of sets and
the category of functors.
Version 1.3.0
-------------
Removed unused modules and streamlined things more: All specific categories are
in the namespace `Cat.Categories`.

6
README.md
View file

@ -14,10 +14,12 @@ Dependencies
------------
To succesfully compile the following is needed:
* Agda version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
* [Agda Standard Library](https://github.com/agda/agda-stdlib)
* The Agda release candidate 2.5.4[^1]
* The experimental branch of [Agda Standard Library](https://github.com/agda/agda-stdlib)
* [Cubical](https://github.com/Saizan/cubical-demo/)
[^1]: At least version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
It's important to have the right version of these - but which one is the right
is in constant flux. It's most likely the newest one.

2
libs/agda-stdlib

@ -1 +1 @@
Subproject commit b9c8e02597751a1b15045cbc5108c221999bd540
Subproject commit fbd8ba7ea84c4b643fd08797b4031b18a59f561d

2
libs/cubical

@ -1 +1 @@
Subproject commit 0d3f02e68297e940227137beac45fc1bce6e2bea
Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe

31
src/Cat.agda
View file

@ -1,19 +1,20 @@
module Cat where
import Cat.Category
open import Cat.Category
import Cat.Category.Functor
import Cat.Category.Product
import Cat.Category.Exponential
import Cat.Category.CartesianClosed
import Cat.Category.NaturalTransformation
import Cat.Category.Yoneda
import Cat.Category.Monad
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Category.Exponential
open import Cat.Category.CartesianClosed
open import Cat.Category.NaturalTransformation
open import Cat.Category.Yoneda
open import Cat.Category.Monad
open import Cat.Category.Monad.Voevodsky
import Cat.Categories.Sets
import Cat.Categories.Cat
import Cat.Categories.Rel
import Cat.Categories.Free
import Cat.Categories.Fun
import Cat.Categories.Cube
import Cat.Categories.CwF
open import Cat.Categories.Sets
open import Cat.Categories.Cat
open import Cat.Categories.Rel
open import Cat.Categories.Free
open import Cat.Categories.Fun
open import Cat.Categories.Cube
open import Cat.Categories.CwF

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

@ -4,20 +4,20 @@
module Cat.Categories.Cat where
open import Agda.Primitive
open import Cubical
open import Function
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Cubical
open import Cubical.Sigma
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Category.Exponential
open import Cat.Category.Exponential hiding (_×_ ; product)
open import Cat.Category.NaturalTransformation
open import Cat.Equality
open Equality.Data.Product
open Functor using (func→ ; func*)
open Category using (Object ; 𝟙)
-- The category of categories
@ -25,14 +25,14 @@ module _ (ℓ ℓ' : Level) where
private
module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
assc = Functor≡ refl refl
assc = Functor≡ refl
module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
ident-r : F[ F ∘ identity ] ≡ F
ident-r = Functor≡ refl refl
ident-r = Functor≡ refl
ident-l : F[ identity ∘ F ] ≡ F
ident-l = Functor≡ refl refl
ident-l = Functor≡ refl
RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
RawCat =
@ -46,313 +46,325 @@ module _ (ℓ ℓ' : Level) where
open RawCategory RawCat
isAssociative : IsAssociative
isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
-- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor.
ident' : IsIdentity identity
ident' = ident-r , ident-l
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
-- categories. There does, however, exist a 2-category of 1-categories.
ident : IsIdentity identity
ident = ident-r , ident-l
-- Because of the note above there is not category of categories.
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
-- categories. There does, however, exist a 2-category of 1-categories.
--
-- Because of this there is no category of categories.
Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
Category.raw (Cat _) = RawCat
Category.isCategory (Cat unprovable) = unprovable
-- Category.raw Cat _ = RawCat
-- Category.isCategory Cat unprovable = unprovable
-- The following to some extend depends on the category of categories being a
-- category. In some places it may not actually be needed, however.
-- | In the following we will pretend there is a category of categories when
-- e.g. talking about it being cartesian closed. It still makes sense to
-- construct these things even though that category does not exist.
--
-- If the notion of a category is later generalized to work on different
-- homotopy levels, then the proof that the category of categories is cartesian
-- closed will follow immediately from these constructions.
-- | the category of categories have products.
module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
private
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 ]}
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
= Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
, Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
postulate univalent : Univalence.Univalent rawProduct isIdentity
instance
isCategory : IsCategory rawProduct
IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = arrowsAreSets
IsCategory.univalent isCategory = univalent
object : Category ℓ ℓ'
Category.raw object = rawProduct
proj₁ : Functor object ℂ
proj₁ = record
{ raw = record
{ omap = fst ; fmap = fst }
; isFunctor = record
{ isIdentity = refl ; isDistributive = refl }
}
proj₂ : Functor object 𝔻
proj₂ = record
{ raw = record
{ omap = snd ; fmap = snd }
; isFunctor = record
{ isIdentity = refl ; isDistributive = refl }
}
module _ {X : Category ℓ ℓ'} (x₁ : Functor X ℂ) (x₂ : Functor X 𝔻) where
private
x : Functor X object
x = record
{ raw = record
{ omap = λ x → x₁.omap x , x₂.omap x
; fmap = λ x → x₁.fmap x , x₂.fmap x
}
; isFunctor = record
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
}
}
where
open module x₁ = Functor x₁
open module x₂ = Functor x₂
isUniqL : F[ proj₁ ∘ x ] ≡ x₁
isUniqL = Functor≡ refl
isUniqR : F[ proj₂ ∘ x ] ≡ x₂
isUniqR = Functor≡ refl
isUniq : F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂
isUniq = isUniqL , isUniqR
isProduct : ∃![ x ] (F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂)
isProduct = x , isUniq
module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
private
Catℓ = Cat ℓ ℓ' unprovable
module _ (ℂ 𝔻 : Category ℓ ℓ') where
private
Catt = Cat ℓ ℓ' unprovable
:Object: = Object ℂ × Object 𝔻
:Arrow: : :Object: → :Object: → Set ℓ'
:Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
:𝟙: : {o : :Object:} → :Arrow: o o
:𝟙: = 𝟙 ℂ , 𝟙 𝔻
_:⊕:_ :
{a b c : :Object:} →
:Arrow: b c →
:Arrow: a b →
:Arrow: a c
_:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
module P = CatProduct ℂ 𝔻
:rawProduct: : RawCategory ℓ ℓ'
RawCategory.Object :rawProduct: = :Object:
RawCategory.Arrow :rawProduct: = :Arrow:
RawCategory.𝟙 :rawProduct: = :𝟙:
RawCategory._∘_ :rawProduct: = _:⊕:_
open RawCategory :rawProduct:
rawProduct : RawProduct Catℓ ℂ 𝔻
RawProduct.object rawProduct = P.object
RawProduct.proj₁ rawProduct = P.proj₁
RawProduct.proj₂ rawProduct = P.proj₂
module C = Category ℂ
module D = Category 𝔻
open import Cubical.Sigma
issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
issSet = setSig {sA = C.arrowsAreSets} {sB = λ x → D.arrowsAreSets}
ident' : IsIdentity :𝟙:
ident'
= Σ≡ (fst C.isIdentity) (fst D.isIdentity)
, Σ≡ (snd C.isIdentity) (snd D.isIdentity)
postulate univalent : Univalence.Univalent :rawProduct: ident'
instance
:isCategory: : IsCategory :rawProduct:
IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
IsCategory.isIdentity :isCategory: = ident'
IsCategory.arrowsAreSets :isCategory: = issSet
IsCategory.univalent :isCategory: = univalent
isProduct : IsProduct Catℓ _ _ rawProduct
IsProduct.isProduct isProduct = P.isProduct
:product: : Category ℓ ℓ'
Category.raw :product: = :rawProduct:
product : Product Catℓ ℂ 𝔻
Product.raw product = rawProduct
Product.isProduct product = isProduct
proj₁ : Catt [ :product: , ℂ ]
proj₁ = record
{ raw = record { func* = fst ; func→ = fst }
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
}
proj₂ : Catt [ :product: , 𝔻 ]
proj₂ = record
{ raw = record { func* = snd ; func→ = snd }
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
}
module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
x : Functor X :product:
x = record
{ raw = record
{ func* = λ x → x₁ .func* x , x₂ .func* x
; func→ = λ x → func→ x₁ x , func→ x₂ x
}
; isFunctor = record
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
}
}
where
open module x₁ = Functor x₁
open module x₂ = Functor x₂
isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
isUniqL = Functor≡ eq* eq→
where
eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
eq* = refl
eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
[ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
eq→ = refl
isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
isUniqR = Functor≡ refl refl
isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂)
uniq = x , isUniq
instance
isProduct : IsProduct Catt proj₁ proj₂
isProduct = uniq
product : Product {ℂ = Catt} ℂ 𝔻
product = record
{ obj = :product:
; proj₁ = proj₁
; proj₂ = proj₂
}
module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
Catt = Cat ℓ ℓ' unprovable
instance
hasProducts : HasProducts Catt
hasProducts = record { product = product unprovable }
hasProducts : HasProducts Catℓ
hasProducts = record { product = product }
-- Basically proves that `Cat ℓ ℓ` is cartesian closed.
module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
-- | The category of categories have expoentntials - and because it has products
-- 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 (F , A) = Functor.omap F A
-- The exponential object
object : Categoryℓ
object = Fun
module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
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
open CatProduct renaming (object to _⊗_) using ()
module _ {c : Functor ℂ 𝔻 × Object ℂ} where
private
F : Functor ℂ 𝔻
F = proj₁ c
C : Object ℂ
C = proj₂ c
ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ 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 ⟩
𝟙 𝔻 ∎
where
module F = Functor F
module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
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
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
isDistributive :
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ]
isDistributive = begin
𝔻 [ (ηθ C) ∘ F.fmap (ℂ [ g ∘ f ]) ]
≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
𝔻 [ H.fmap (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
𝔻 [ 𝔻 [ H.fmap g ∘ H.fmap f ] ∘ (ηθ A) ]
≡⟨ sym 𝔻.isAssociative ⟩
𝔻 [ H.fmap g ∘ 𝔻 [ H.fmap f ∘ ηθ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) 𝔻.isAssociative ⟩
𝔻 [ H.fmap g ∘ 𝔻 [ 𝔻 [ H.fmap f ∘ η A ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
𝔻 [ H.fmap g ∘ 𝔻 [ 𝔻 [ η B ∘ G.fmap f ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H.fmap g ∘ φ ]) (sym 𝔻.isAssociative) ⟩
𝔻 [ H.fmap g ∘ 𝔻 [ η B ∘ 𝔻 [ G.fmap f ∘ θ A ] ] ]
≡⟨ 𝔻.isAssociative ⟩
𝔻 [ 𝔻 [ H.fmap g ∘ η B ] ∘ 𝔻 [ G.fmap f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G.fmap f ∘ θ A ] ]) (sym (ηNat g)) ⟩
𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ G.fmap f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ φ ]) (sym (θNat f)) ⟩
𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ] ∎
eval : Functor (CatProduct.object object ℂ) 𝔻
eval = record
{ raw = record
{ omap = omap
; fmap = λ {dom} {cod} → fmap {dom} {cod}
}
; isFunctor = record
{ isIdentity = λ {o} → ident {o}
; isDistributive = λ {f u n k y} → isDistributive {f} {u} {n} {k} {y}
}
}
module _ (𝔸 : Category ℓ ℓ) (F : Functor (𝔸 ⊗ ℂ) 𝔻) where
postulate
parallelProduct
: Functor 𝔸 object → Functor ℂ ℂ
→ Functor (𝔸 ⊗ ℂ) (object ⊗ ℂ)
transpose : Functor 𝔸 object
eq : F[ eval ∘ (parallelProduct transpose (identity {C = ℂ})) ] ≡ F
-- eq : F[ :eval: ∘ {!!} ] ≡ F
-- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
-- eq' : (Catℓ [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
-- (𝟙 Catℓ)
-- ])
-- ≡ F
-- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
-- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
-- transpose , eq
-- We don't care about filling out the holes below since they are anyways hidden
-- behind an unprovable statement.
module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
private
Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
Catℓ = Cat ℓ ℓ unprovable
module _ (ℂ 𝔻 : Category ℓ ℓ) where
open Fun ℂ 𝔻 renaming (identity to idN)
private
:obj: : Object Catℓ
:obj: = Fun
module CatExp = CatExponential ℂ 𝔻
_⊗_ = CatProduct.object
:func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
:func*: (F , A) = func* F A
-- Filling the hole causes Agda to loop indefinitely.
eval : Functor (CatExp.object ⊗ ℂ) 𝔻
eval = {!CatExp.eval!}
module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
private
F : Functor ℂ 𝔻
F = proj₁ dom
A : Object ℂ
A = proj₂ dom
isExponential : IsExponential Catℓ ℂ 𝔻 CatExp.object eval
isExponential = {!CatExp.isExponential!}
G : Functor ℂ 𝔻
G = proj₁ cod
B : Object ℂ
B = proj₂ cod
:func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
→ 𝔻 [ func* F A , func* G B ]
:func→: ((θ , θNat) , f) = result
where
θA : 𝔻 [ func* F A , func* G A ]
θA = θ A
θB : 𝔻 [ func* F B , func* G B ]
θB = θ B
F→f : 𝔻 [ func* F A , func* F B ]
F→f = func→ F f
G→f : 𝔻 [ func* G A , func* G B ]
G→f = func→ G f
l : 𝔻 [ func* F A , func* G B ]
l = 𝔻 [ θB ∘ F→f ]
r : 𝔻 [ func* F A , func* G B ]
r = 𝔻 [ G→f ∘ θA ]
-- There are two choices at this point,
-- but I suppose the whole point is that
-- by `θNat f` we have `l ≡ r`
-- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
-- lem = θNat f
result : 𝔻 [ func* F A , func* G B ]
result = l
_×p_ = product unprovable
module _ {c : Functor ℂ 𝔻 × Object ℂ} where
private
F : Functor ℂ 𝔻
F = proj₁ c
C : Object ℂ
C = proj₂ c
-- NaturalTransformation F G × ℂ .Arrow A B
-- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
-- where
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
-- Unfortunately the equational version has some ambigous arguments.
:ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
:ident: = begin
:func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
:func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩
𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩
𝟙 𝔻 ∎
where
open module 𝔻 = Category 𝔻
open module F = Functor F
module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
F = F×A .proj₁
A = F×A .proj₂
G = G×B .proj₁
B = G×B .proj₂
H = H×C .proj₁
C = H×C .proj₂
-- Not entirely clear what this is at this point:
_P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C}
module _
-- NaturalTransformation F G × ℂ .Arrow A B
{θ×f : NaturalTransformation F G × ℂ [ A , B ]}
{η×g : NaturalTransformation G H × ℂ [ B , C ]} where
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
:isDistributive: :
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ]
:isDistributive: = begin
𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ]
≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ]
≡⟨ sym isAssociative ⟩
𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩
𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ]
≡⟨ isAssociative ⟩
𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎
where
open Category 𝔻
module H = Functor H
:eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
:eval: = record
{ raw = record
{ func* = :func*:
; func→ = λ {dom} {cod} → :func→: {dom} {cod}
}
; isFunctor = record
{ isIdentity = λ {o} → :ident: {o}
; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y}
}
}
module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
postulate
transpose : Functor 𝔸 :obj:
eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F
-- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
-- eq' : (Catℓ [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
-- (𝟙 Catℓ)
-- ])
-- ≡ F
-- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
-- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
-- transpose , eq
postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-- :isExponential: = {!catTranspose!}
-- where
-- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_)
-- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F
-- :exponent: : Exponential (Cat ℓ ℓ) A B
:exponent: : Exponential Catℓ ℂ 𝔻
:exponent: = record
{ obj = :obj:
; eval = :eval:
; isExponential = :isExponential:
exponent : Exponential Catℓ ℂ 𝔻
exponent = record
{ obj = CatExp.object
; eval = eval
; isExponential = isExponential
}
hasExponentials : HasExponentials Catℓ
hasExponentials = record { exponent = :exponent: }
hasExponentials = record { exponent = exponent }

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

@ -26,24 +26,24 @@ open Category hiding (_∘_)
open Functor
module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
-- Ns is the "namespace"
ℓo = (suc zero ⊔ ℓ)
private
-- Ns is the "namespace"
ℓo = (suc zero ⊔ ℓ)
FiniteDecidableSubset : Set ℓ
FiniteDecidableSubset = Ns → Dec ⊤
FiniteDecidableSubset : Set ℓ
FiniteDecidableSubset = Ns → Dec ⊤
isTrue : Bool → Set
isTrue false = ⊥
isTrue true = ⊤
isTrue : Bool → Set
isTrue false = ⊥
isTrue true = ⊤
elmsof : FiniteDecidableSubset → Set ℓ
elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
elmsof : FiniteDecidableSubset → Set ℓ
elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
𝟚 : Set
𝟚 = Bool
𝟚 : Set
𝟚 = Bool
module _ (I J : FiniteDecidableSubset) where
private
module _ (I J : FiniteDecidableSubset) where
Hom' : Set ℓ
Hom' = elmsof I → elmsof J ⊎ 𝟚
isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set
@ -63,18 +63,18 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
; (inj₂ _) → Lift ⊤
}
Hom = Σ Hom' rules
Hom = Σ Hom' rules
module Raw = RawCategory
-- The category of names and substitutions
Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
Raw.Object Rawℂ = FiniteDecidableSubset
Raw.Arrow Rawℂ = Hom
Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
Raw._∘_ Rawℂ = {!!}
module Raw = RawCategory
-- The category of names and substitutions
Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
Raw.Object Rawℂ = FiniteDecidableSubset
Raw.Arrow Rawℂ = Hom
Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
Raw._∘_ Rawℂ = {!!}
postulate IsCategoryℂ : IsCategory Rawℂ
postulate IsCategoryℂ : IsCategory Rawℂ
ℂ : Category ℓ ℓ
raw ℂ = Rawℂ
isCategory ℂ = IsCategoryℂ
ℂ : Category ℓ ℓ
raw ℂ = Rawℂ
isCategory ℂ = IsCategoryℂ

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

@ -28,20 +28,20 @@ module _ {ℓa ℓb : Level} where
private
module T = Functor T
Type : (Γ : Object ℂ) → Set ℓa
Type Γ = proj₁ (proj₁ (T.func* Γ))
Type Γ = proj₁ (proj₁ (T.omap Γ))
module _ {Γ : Object ℂ} {A : Type Γ} where
-- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-- k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
-- k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
-- (λ f →
-- {x : proj₁ (func* T B)} →
-- proj₂ (func* T B) x → proj₂ (func* T A) (f x))
-- k = T.func→ γ
-- k₁ : proj₁ (func* T B) → proj₁ (func* T A)
-- {x : proj₁ (omap T B)} →
-- proj₂ (omap T B) x → proj₂ (omap T A) (f x))
-- k = T.fmap γ
-- k₁ : proj₁ (omap T B) → proj₁ (omap T A)
-- k₁ = proj₁ k
-- k₂ : ({x : proj₁ (func* T B)} →
-- proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
-- k₂ : ({x : proj₁ (omap T B)} →
-- proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
-- k₂ = proj₂ k
record ContextComprehension : Set (ℓa ⊔ ℓb) where
@ -51,7 +51,7 @@ module _ {ℓa ℓb : Level} where
-- proj2 : ????
-- if γ : ℂ [ A , B ]
-- then T .func→ γ (written T[γ]) interpret substitutions in types and terms respectively.
-- then T .fmap γ (written T[γ]) interpret substitutions in types and terms respectively.
-- field
-- ump : {Δ : ℂ .Object} → (γ : ℂ [ Δ , Γ ])
-- → (a : {!!}) → {!!}

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

@ -20,10 +20,10 @@ singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {
singleton f = cons f empty
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
module ℂ = Category ℂ
open Category ℂ
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}
→ p ++ (q ++ r) ≡ (p ++ q) ++ r
p-isAssociative {r = r} {q} {empty} = refl

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

@ -4,50 +4,24 @@ module Cat.Categories.Fun where
open import Agda.Primitive
open import Data.Product
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
module Nat = Data.Nat
open import Data.Product
open import Cubical
open import Cubical.Sigma
open import Cubical.GradLemma
open import Cubical.NType.Properties
open import Cat.Category
open import Cat.Category.Functor hiding (identity)
open import Cat.Category.NaturalTransformation
open import Cat.Wishlist
open import Cat.Equality
import Cat.Category.NaturalTransformation
open Equality.Data.Product
module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙)
module NT = NaturalTransformation ℂ 𝔻
open NT public
private
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
module _ {F G : Functor ℂ 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
λ θ → ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)
module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
private
private
module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
@ -58,13 +32,11 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζ' η') θ')
_g⊕f_ = NT[_∘_] {A} {B} {C}
_h⊕g_ = NT[_∘_] {B} {C} {D}
:isAssociative: : L ≡ R
:isAssociative: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → isAssociative))
where
open Category 𝔻
_g⊕f_ = NT[_∘_] {A} {B} {C}
_h⊕g_ = NT[_∘_] {B} {C} {D}
isAssociative : L ≡ R
isAssociative = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → 𝔻.isAssociative))
private
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
@ -94,27 +66,120 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
}
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)
coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ]
coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP
-- 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 𝔻.𝟙
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 ]) ∎
transs : (i : I) → Transformation A (p i)
transs = {!!}
natt : (i : I) → Natural A (p i) {!!}
natt = {!!}
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)!}) {!!}
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 = {!!}
nat : Natural A B coe𝟙
nat = nat'
fromEq : NaturalTransformation A B
fromEq = coe𝟙 , nat
module _ {A B : Functor ℂ 𝔻} where
obverse : A ≡ B → A ≅ B
obverse p = res
where
ob : Arrow A B
ob = fromEq p
re : Arrow B A
re = fromEq (sym p)
vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
vr = {!!}
rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
rv = {!!}
isInverse : IsInverseOf {A} {B} ob re
isInverse = vr , rv
iso : Isomorphism {A} {B} ob
iso = re , isInverse
res : A ≅ B
res = ob , iso
reverse : A ≅ B → A ≡ B
reverse iso = {!!}
ve-re : (y : A ≅ B) → obverse (reverse y) ≡ y
ve-re = {!!}
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 = {!gradLemma obverse reverse ve-re re-ve!}
univalent : Univalent (λ{ {A} {B} → isIdentity {A} {B}})
univalent = done
instance
:isCategory: : IsCategory RawFun
:isCategory: = record
{ isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
isCategory : IsCategory RawFun
isCategory = record
{ isAssociative = λ {A B C D} → isAssociative {A} {B} {C} {D}
; isIdentity = λ {A B} → isIdentity {A} {B}
; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
; univalent = {!!}
; arrowsAreSets = λ {F} {G} → naturalTransformationIsSet {F} {G}
; univalent = univalent
}
Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
Category.raw Fun = RawFun
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open import Cat.Categories.Sets
open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
private
open import Cat.Categories.Sets
open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
-- Restrict the functors to Presheafs.
RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
RawPresh = record
{ Object = Presheaf ℂ
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identity F
; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
}
-- Restrict the functors to Presheafs.
rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
rawPresh = record
{ Object = Presheaf ℂ
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identity F
; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
}
instance
isCategory : IsCategory rawPresh
isCategory = Fun.isCategory _ _
Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
Category.raw Presh = rawPresh
Category.isCategory Presh = isCategory

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

@ -56,7 +56,6 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
backwards (a' , (a=a' , a'b∈S)) = subst (sym a=a') a'b∈S
fwd-bwd : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x
-- isbijective x = pathJ (λ y x₁ → (backwards ∘ forwards) x ≡ x) {!!} {!!} {!!}
fwd-bwd x = pathJprop (λ y _ → y) x
bwd-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)

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

@ -1,35 +1,172 @@
-- | The category of homotopy sets
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Categories.Sets where
open import Cubical
open import Agda.Primitive
open import Data.Product
import Function
open import Function using (_∘_)
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 Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Wishlist
module _ (ℓ : Level) where
private
open RawCategory
open IsCategory
open import Cubical.Univalence
open import Cubical.NType.Properties
open import Cubical.Universe
SetsRaw : RawCategory (lsuc ℓ) ℓ
Object SetsRaw = hSet
Arrow SetsRaw (T , _) (U , _) = T → U
𝟙 SetsRaw = Function.id
_∘_ SetsRaw = Function._∘′_
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
arrowsAreSets : ArrowsAreSets
arrowsAreSets {B = (_ , s)} = setPi λ _ → s
module _ {hA hB : Object} where
private
A = proj₁ hA
isSetA : isSet A
isSetA = proj₂ hA
B = proj₁ hB
isSetB : isSet B
isSetB = proj₂ hB
toIsomorphism : A ≃ B → hA ≅ hB
toIsomorphism e = obverse , inverse , verso-recto , recto-verso
where
open _≃_ e
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
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
obverse : hA ≡ hB → hA ≅ hB
obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
-- 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 }
-- 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
-- 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!}
SetsIsCategory : IsCategory SetsRaw
isAssociative SetsIsCategory = refl
proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
univalent SetsIsCategory = {!!}
IsCategory.isAssociative SetsIsCategory = refl
IsCategory.isIdentity SetsIsCategory {A} {B} = isIdentity {A} {B}
IsCategory.arrowsAreSets SetsIsCategory {A} {B} = arrowsAreSets {A} {B}
IsCategory.univalent SetsIsCategory = univalent
𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
Category.raw 𝓢𝓮𝓽 = SetsRaw
@ -64,58 +201,57 @@ module _ {ℓ : Level} where
lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
proj₁ lem = refl
proj₂ lem = refl
instance
isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
product : Product {ℂ = 𝓢} 0A 0B
product = record
{ obj = 0A×0B
; proj₁ = Data.Product.proj₁
; proj₂ = Data.Product.proj₂
; isProduct = λ { {X} → isProduct {X = X}}
}
rawProduct : RawProduct 𝓢 0A 0B
RawProduct.object rawProduct = 0A×0B
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
product : Product 𝓢 0A 0B
Product.raw product = rawProduct
Product.isProduct product = isProduct
instance
SetsHasProducts : HasProducts 𝓢
SetsHasProducts = record { product = product }
module _ {ℓa ℓb : Level} where
module _ (ℂ : Category ℓa ℓb) where
-- Covariant Presheaf
Representable : Set (ℓa ⊔ lsuc ℓb)
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-- Covariant Presheaf
Representable : Set (ℓa ⊔ lsuc ℓb)
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
-- Contravariant Presheaf
Presheaf : Set (ℓa ⊔ lsuc ℓb)
Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
-- Contravariant Presheaf
Presheaf : Set (ℓa ⊔ lsuc ℓb)
Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
open Category ℂ
-- The "co-yoneda" embedding.
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
representable : Category.Object ℂ → Representable
representable A = record
{ raw = record
{ func* = λ B → ℂ [ A , B ] , arrowsAreSets
; func→ = ℂ [_∘_]
{ omap = λ B → ℂ [ A , B ] , arrowsAreSets
; fmap = ℂ [_∘_]
}
; isFunctor = record
{ isIdentity = funExt λ _ → proj₂ isIdentity
; isDistributive = funExt λ x → sym isAssociative
}
}
where
open Category ℂ
-- Alternate name: `yoneda`
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
presheaf : Category.Object (opposite ℂ) → Presheaf
presheaf B = record
{ raw = record
{ func* = λ A → ℂ [ A , B ] , arrowsAreSets
; func→ = λ f g → ℂ [ g ∘ f ]
{ omap = λ A → ℂ [ A , B ] , arrowsAreSets
; fmap = λ f g → ℂ [ g ∘ f ]
}
; isFunctor = record
{ isIdentity = funExt λ x → proj₁ isIdentity
; isDistributive = funExt λ x → isAssociative
}
}
where
open Category ℂ

124
src/Cat/Category.agda
View file

@ -24,9 +24,6 @@
-- ------
--
-- Propositionality for all laws about the category.
--
-- TODO: An equality principle for categories that focuses on the pure data-part.
--
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category where
@ -41,7 +38,7 @@ open import Data.Product renaming
open import Data.Empty
import Function
open import Cubical
open import Cubical.NType.Properties using ( propIsEquiv )
open import Cubical.NType.Properties using ( propIsEquiv ; lemPropF )
open import Cat.Wishlist
@ -76,7 +73,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
𝟙 : {A : Object} → Arrow A A
_∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
infixl 10 _∘_
infixl 10 _∘_ _>>>_
-- | Operations on data
@ -86,9 +83,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
codomain : { a b : Object } → Arrow a b → Object
codomain {b = b} _ = b
_>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C
f >>> g = g ∘ f
-- | Laws about the data
-- TODO: It seems counter-intuitive that the normal-form is on the
-- FIXME It seems counter-intuitive that the normal-form is on the
-- right-hand-side.
IsAssociative : Set (ℓa ⊔ ℓb)
IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
@ -129,7 +129,9 @@ 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.
-- | 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
@ -150,9 +152,11 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
-- iso-is-epi : Isomorphism f → Epimorphism {X = X} f
-- iso-is-mono : Isomorphism f → Monomorphism {X = X} f
--
-- Sans `univalent` this would be what is referred to as a pre-category in
-- [HoTT].
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
open RawCategory ℂ public
open Univalence ℂ public
open Univalence ℂ public
field
isAssociative : IsAssociative
isIdentity : IsIdentity 𝟙
@ -191,9 +195,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
--
-- Proves that all projections of `IsCategory` are mere propositions as well as
-- `IsCategory` itself being a mere proposition.
module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
open RawCategory C
module _ (ℂ : IsCategory C) where
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
@ -237,52 +241,71 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
private
module _ (x y : IsCategory C) where
module _ (x y : IsCategory ℂ) where
module IC = IsCategory
module X = IsCategory x
module Y = IsCategory y
open Univalence C
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
-- result from `x : IsCategory C`. I don't know which (if any) possibly
-- adverse effects this may have.
isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
done : x ≡ y
U : ∀ {a : IsIdentity 𝟙}
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
→ (b : Univalent a)
→ Set _
U eqwal bbb =
U eqwal univ =
(λ i → Univalent (eqwal i))
[ X.univalent ≡ bbb ]
[ X.univalent ≡ univ ]
P : (y : IsIdentity 𝟙)
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
P y eq = ∀ (b' : Univalent y) → U eq b'
helper : ∀ (b' : Univalent X.isIdentity)
P y eq = ∀ (univ : Univalent y) → U eq univ
p : ∀ (b' : Univalent X.isIdentity)
→ (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.isIdentity isIdentity
p univ = propUnivalent x X.univalent univ
helper : P Y.isIdentity isIdentity
helper = pathJ P p Y.isIdentity isIdentity
eqUni : U isIdentity Y.univalent
eqUni = foo Y.univalent
IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
IC.isIdentity (done i) = isIdentity i
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
IC.univalent (done i) = eqUni i
propIsCategory : isProp (IsCategory C)
propIsCategory : isProp (IsCategory ℂ)
propIsCategory = done
-- | Univalent categories
--
-- Just bundles up the data with witnesses inhabting the propositions.
-- Just bundles up the data with witnesses inhabiting the propositions.
record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
field
raw : RawCategory ℓa ℓb
raw : RawCategory ℓa ℓb
{{isCategory}} : IsCategory raw
open IsCategory isCategory public
-- The fact that being a category is a mere proposition gives rise to this
-- equality principle for categories.
module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where
private
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where
private
isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ]
isCategoryEq = lemPropF Propositionality.propIsCategory rawEq
Category≡ : ℂ ≡ 𝔻
Category≡ i = record
{ raw = rawEq i
; isCategory = isCategoryEq i
}
-- | Syntax for arrows- and composition in a given category.
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Category ℂ
@ -298,23 +321,42 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-- flipped.
module Opposite {ℓa ℓb : Level} where
module _ (ℂ : Category ℓa ℓb) where
open Category ℂ
private
module ℂ = Category ℂ
opRaw : RawCategory ℓa ℓb
RawCategory.Object opRaw = Object
RawCategory.Arrow opRaw = Function.flip Arrow
RawCategory.𝟙 opRaw = 𝟙
RawCategory._∘_ opRaw = Function.flip _∘_
RawCategory.Object opRaw = ℂ.Object
RawCategory.Arrow opRaw = Function.flip ℂ.Arrow
RawCategory.𝟙 opRaw = ℂ.𝟙
RawCategory._∘_ opRaw = Function.flip ℂ._∘_
opIsCategory : IsCategory opRaw
IsCategory.isAssociative opIsCategory = sym isAssociative
IsCategory.isIdentity opIsCategory = swap isIdentity
IsCategory.arrowsAreSets opIsCategory = arrowsAreSets
IsCategory.univalent opIsCategory = {!!}
open RawCategory opRaw
open Univalence opRaw
isIdentity : IsIdentity 𝟙
isIdentity = swap ℂ.isIdentity
module _ {A B : ℂ.Object} where
univalent : isEquiv (A ≡ B) (A ≅ B)
(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
flipFiber (eq , eqIso) = sym eq , {!!}
snd (univalent iso) = {!!}
isCategory : IsCategory opRaw
IsCategory.isAssociative isCategory = sym ℂ.isAssociative
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = ℂ.arrowsAreSets
IsCategory.univalent isCategory = univalent
opposite : Category ℓa ℓb
raw opposite = opRaw
Category.isCategory opposite = opIsCategory
Category.raw opposite = opRaw
Category.isCategory opposite = isCategory
-- As demonstrated here a side-effect of having no-eta-equality on constructors
-- means that we need to pick things apart to show that things are indeed
@ -331,9 +373,7 @@ module Opposite {ℓa ℓb : Level} where
RawCategory.𝟙 (rawInv _) = 𝟙
RawCategory._∘_ (rawInv _) = _∘_
-- TODO: Define and use Monad≡
oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
Category.raw (oppositeIsInvolution i) = rawInv i
Category.isCategory (oppositeIsInvolution x) = {!!}
oppositeIsInvolution = Category≡ rawInv
open Opposite public

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

@ -1,40 +1,44 @@
module Cat.Category.Exponential where
open import Agda.Primitive
open import Data.Product
open import Data.Product hiding (_×_)
open import Cubical
open import Cat.Category
open import Cat.Category.Product
open Category
module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
open HasProducts hasProducts
open Product hiding (obj)
private
_×p_ : (A B : Object ℂ) → Object ℂ
_×p_ A B = Product.obj (product A B)
open Category ℂ
open HasProducts hasProducts public
module _ (B C : Object ℂ) where
IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ])
module _ (B C : Object) where
record IsExponential'
(Cᴮ : Object)
(eval : ℂ [ Cᴮ × B , C ]) : Set (ℓ ⊔ ℓ') where
field
uniq
: ∀ (A : Object) (f : ℂ [ A × B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
record Exponential : Set (ℓ ⊔ ℓ') where
field
-- obj ≡ Cᴮ
obj : Object ℂ
eval : ℂ [ obj ×p B , C ]
obj : Object
eval : ℂ [ obj × B , C ]
{{isExponential}} : IsExponential obj eval
-- If I make this an instance-argument then the instance resolution
-- algorithm goes into an infinite loop. Why?
exponentialsHaveProducts : HasProducts ℂ
exponentialsHaveProducts = hasProducts
transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ]
transpose A f = proj₁ (isExponential A f)
record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
open Category ℂ
open Exponential public
field
exponent : (A B : Object ℂ) → Exponential ℂ A B
exponent : (A B : Object) → Exponential ℂ A B
_⇑_ : (A B : Object) → Object
A ⇑ B = (exponent A B) .obj

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

@ -18,21 +18,50 @@ module _ {ℓc ℓc' ℓd ℓd'}
ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd'
𝓤 = Set ℓ
Omap = Object ℂ → Object 𝔻
Fmap : Omap → Set _
Fmap omap = ∀ {A B}
→ ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
record RawFunctor : 𝓤 where
field
func* : Object ℂ → Object 𝔻
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
omap : Object ℂ → Object 𝔻
fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
IsIdentity : Set _
IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}
IsIdentity = {A : Object ℂ} → fmap (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {omap A}
IsDistributive : Set _
IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
→ func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
→ fmap (ℂ [ g ∘ f ]) ≡ 𝔻 [ fmap g ∘ fmap f ]
-- | Equality principle for raw functors
--
-- The type of `fmap` depend on the value of `omap`. We can wrap this up
-- into an equality principle for this type like is done for e.g. `Σ` using
-- `pathJ`.
module _ {x y : RawFunctor} where
open RawFunctor
private
P : (omap' : Omap) → (eq : omap x ≡ omap') → Set _
P y eq = (fmap' : Fmap y) → (λ i → Fmap (eq i))
[ fmap x ≡ fmap' ]
module _
(eq : (λ i → Omap) [ omap x ≡ omap y ])
(kk : P (omap x) refl)
where
private
p : P (omap y) eq
p = pathJ P kk (omap y) eq
eq→ : (λ i → Fmap (eq i)) [ fmap x ≡ fmap y ]
eq→ = p (fmap y)
RawFunctor≡ : x ≡ y
omap (RawFunctor≡ i) = eq i
fmap (RawFunctor≡ i) = eq→ i
record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F public
field
-- FIXME Really ought to be preserves identity or something like this.
isIdentity : IsIdentity
isDistributive : IsDistributive
@ -45,6 +74,9 @@ module _ {ℓc ℓc' ℓd ℓd'}
open Functor
EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _
EndoFunctor ℂ = Functor ℂ ℂ
module _
{ℓa ℓb : Level}
{ℂ 𝔻 : Category ℓa ℓb}
@ -81,26 +113,21 @@ module _
module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
Functor≡ : {F G : Functor ℂ 𝔻}
→ (eq* : func* F ≡ func* G)
→ (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
[ func→ F ≡ func→ G ])
→ raw F ≡ raw G
→ F ≡ G
Functor≡ {F} {G} eq* eq→ i = record
{ raw = eqR i
; isFunctor = eqIsF i
}
raw (Functor≡ eq i) = eq i
isFunctor (Functor≡ {F} {G} eq i)
= res i
where
eqR : raw F ≡ raw G
eqR i = record { func* = eq* i ; func→ = eq→ i }
eqIsF : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
res : (λ i → IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ]
res = IsFunctorIsProp' (isFunctor F) (isFunctor G)
module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
private
F* = func* F
F→ = func→ F
G* = func* G
G→ = func→ G
F* = omap F
F→ = fmap F
G* = omap G
G→ = fmap 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 ]
@ -111,8 +138,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
_∘fr_ : RawFunctor A C
RawFunctor.func* _∘fr_ = F* ∘ G*
RawFunctor.func→ _∘fr_ = F→ ∘ G→
RawFunctor.omap _∘fr_ = F* ∘ G*
RawFunctor.fmap _∘fr_ = F→ ∘ G→
instance
isFunctor' : IsFunctor A C _∘fr_
isFunctor' = record
@ -131,8 +158,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
identity = record
{ raw = record
{ func* = λ x → x
; func→ = λ x → x
{ omap = λ x → x
; fmap = λ x → x
}
; isFunctor = record
{ isIdentity = refl

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

@ -1,3 +1,22 @@
{---
Monads
This module presents two formulations of monads:
* The standard monoidal presentation
* Kleisli's presentation
The first one defines a monad in terms of an endofunctor and two natural
transformations. The second defines it in terms of a function on objects and a
pair of arrows.
These two formulations are proven to be equivalent:
Monoidal.Monad ≃ Kleisli.Monad
The monoidal representation is exposed by default from this module.
---}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Category.Monad where
@ -6,326 +25,185 @@ 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.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
open import Cat.Categories.Fun
-- "A monad in the monoidal form" [voe]
module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
open NaturalTransformation ℂ ℂ
record RawMonad : Set ℓ where
field
-- R ~ m
R : Functor ℂ ℂ
-- η ~ pure
ηNat : NaturalTransformation F.identity R
-- μ ~ join
μNat : NaturalTransformation F[ R ∘ R ] R
η : Transformation F.identity R
η = proj₁ ηNat
μ : Transformation F[ R ∘ R ] R
μ = proj₁ μNat
private
module R = Functor R
module RR = Functor F[ R ∘ R ]
module _ {X : Object} where
IsAssociative' : Set _
IsAssociative' = μ X ∘ R.func→ (μ X) ≡ μ X ∘ μ (R.func* X)
IsInverse' : Set _
IsInverse'
= μ X ∘ η (R.func* X) ≡ 𝟙
× μ X ∘ R.func→ (η X) ≡ 𝟙
-- We don't want the objects to be indexes of the type, but rather just
-- universally quantify over *all* objects of the category.
IsAssociative = {X : Object} → IsAssociative' {X}
IsInverse = {X : Object} → IsInverse' {X}
record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public
field
isAssociative : IsAssociative
isInverse : IsInverse
record Monad : Set ℓ where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
Monad.raw (Monad≡ eq i) = eq i
Monad.isMonad (Monad≡ {m} {n} eq i) = res i
where
-- TODO: PathJ nightmare + `propIsMonad`.
res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
res = {!!}
-- "A monad in the Kleisli form" [voe]
module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_)
record RawMonad : Set ℓ where
field
RR : Object → Object
-- Note name-change from [voe]
ζ : {X : Object} → ℂ [ X , RR X ]
rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-- Note the correspondance with Haskell:
--
-- RR ~ m
-- ζ ~ pure
-- rr ~ flip (>>=)
--
-- Where those things have these types:
--
-- m : 𝓤 → 𝓤
-- pure : x → m x
-- flip (>>=) :: (a → m b) → m a → m b
--
pure : {X : Object} → ℂ [ X , RR X ]
pure = ζ
fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
fmap f = rr (ζ ∘ f)
-- Why is (>>=) not implementable?
--
-- (>>=) : m a -> (a -> m b) -> m b
-- (>=>) : (a -> m b) -> (b -> m c) -> a -> m c
_>=>_ : {A B C : Object} → ℂ [ A , RR B ] → ℂ [ B , RR C ] → ℂ [ A , RR C ]
f >=> g = rr g ∘ f
-- fmap id ≡ id
IsIdentity = {X : Object}
→ rr ζ ≡ 𝟙 {RR X}
IsNatural = {X Y : Object} (f : ℂ [ X , RR Y ])
→ rr f ∘ ζ ≡ f
IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
→ rr g ∘ rr f ≡ rr (rr g ∘ f)
Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
→ fmap (g ∘ f) ≡ fmap g ∘ fmap f
record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public
field
isIdentity : IsIdentity
isNatural : IsNatural
isDistributive : IsDistributive
fusion : Fusion
fusion {g = g} {f} = begin
fmap (g ∘ f) ≡⟨⟩
rr (ζ ∘ (g ∘ f)) ≡⟨ {!!} ⟩
rr (rr (ζ ∘ g) ∘ (ζ ∘ f)) ≡⟨ sym lem ⟩
rr (ζ ∘ g) ∘ rr (ζ ∘ f) ≡⟨⟩
fmap g ∘ fmap f ∎
where
lem : rr (ζ ∘ g) ∘ rr (ζ ∘ f) ≡ rr (rr (ζ ∘ g) ∘ (ζ ∘ f))
lem = isDistributive (ζ ∘ g) (ζ ∘ f)
record Monad : Set ℓ where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
Monad.raw (Monad≡ eq i) = eq i
Monad.isMonad (Monad≡ {m} {n} eq i) = res i
where
-- TODO: PathJ nightmare + `propIsMonad`.
res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
res = {!!}
-- Problem 2.3
-- | The monoidal- and kleisli presentation of monads are equivalent.
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
private
open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
open Functor using (func* ; func→)
module ℂ = Category ℂ
open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
module M = Monoidal ℂ
module K = Kleisli ℂ
module K = Kleisli ℂ
-- Note similarity with locally defined things in Kleisly.RawMonad!!
module _ (m : M.RawMonad) where
private
open M.RawMonad m
module Kraw = K.RawMonad
RR : Object → Object
RR = func* R
ζ : {X : Object} → ℂ [ X , RR X ]
ζ {X} = η X
rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
rr {X} {Y} f = μ Y ∘ func→ R f
open M.RawMonad m
forthRaw : K.RawMonad
Kraw.RR forthRaw = RR
Kraw.ζ forthRaw = ζ
Kraw.rr forthRaw = rr
K.RawMonad.omap forthRaw = Romap
K.RawMonad.pure forthRaw = pureT _
K.RawMonad.bind forthRaw = bind
module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
private
open M.IsMonad m
open K.RawMonad (forthRaw raw)
module Kis = K.IsMonad
isIdentity : IsIdentity
isIdentity {X} = begin
rr ζ ≡⟨⟩
rr (η X) ≡⟨⟩
μ X ∘ func→ R (η X) ≡⟨ proj₂ isInverse ⟩
𝟙 ∎
module R = Functor R
isNatural : IsNatural
isNatural {X} {Y} f = begin
rr f ∘ ζ ≡⟨⟩
rr f ∘ η X ≡⟨⟩
μ Y ∘ R.func→ f ∘ η X ≡⟨ sym ℂ.isAssociative ⟩
μ Y ∘ (R.func→ f ∘ η X) ≡⟨ cong (λ φ → μ Y ∘ φ) (sym (ηN f)) ⟩
μ Y ∘ (η (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
μ Y ∘ η (R.func* Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩
f ∎
where
open NaturalTransformation
module ℂ = Category ℂ
ηN : Natural ℂ ℂ F.identity R η
ηN = proj₂ ηNat
isDistributive : IsDistributive
isDistributive {X} {Y} {Z} g f = begin
rr g ∘ rr f ≡⟨⟩
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ sym lem2 ⟩
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
μ Z ∘ R.func→ (rr g ∘ f) ∎
where
-- Proved it in reverse here... otherwise it could be neatly inlined.
lem2
: μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
lem2 = begin
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
μ Z ∘ (R.func→ (μ Z) ∘ RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
(μ Z ∘ R.func→ (μ Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ cong (λ φ → φ ∘ (RR.func→ g ∘ R.func→ f)) lemmm ⟩
(μ Z ∘ μ (R.func* Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
μ Z ∘ μ (R.func* Z) ∘ RR.func→ g ∘ R.func→ f ≡⟨ {!!} ⟩ -- ●-solver + lem4
μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f ≡⟨ sym (Category.isAssociative ℂ) ⟩
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
where
module RR = Functor F[ R ∘ R ]
distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
→ R.func→ (a ∘ b ∘ c)
≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
distrib = {!!}
comm : ∀ {A B C D E}
→ {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
→ a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
comm = {!!}
μN = proj₂ μNat
lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
lemmm = isAssociative
lem4 : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
lem4 = μN g
module MI = M.IsMonad m
forthIsMonad : K.IsMonad (forthRaw raw)
Kis.isIdentity forthIsMonad = isIdentity
Kis.isNatural forthIsMonad = isNatural
Kis.isDistributive forthIsMonad = isDistributive
K.IsMonad.isIdentity forthIsMonad = proj₂ MI.isInverse
K.IsMonad.isNatural forthIsMonad = MI.isNatural
K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
forth : M.Monad → K.Monad
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
module _ (m : K.Monad) where
private
module ℂ = Category ℂ
open K.Monad m
module Mraw = M.RawMonad
open NaturalTransformation ℂ ℂ
rawR : RawFunctor ℂ ℂ
RawFunctor.func* rawR = RR
RawFunctor.func→ rawR f = rr (ζ ∘ f)
isFunctorR : IsFunctor ℂ ℂ rawR
IsFunctor.isIdentity isFunctorR = begin
rr (ζ ∘ 𝟙) ≡⟨ cong rr (proj₁ ℂ.isIdentity) ⟩
rr ζ ≡⟨ isIdentity ⟩
𝟙 ∎
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
rr (ζ ∘ (g ∘ f)) ≡⟨⟩
fmap (g ∘ f) ≡⟨ fusion ⟩
fmap g ∘ fmap f ≡⟨⟩
rr (ζ ∘ g) ∘ rr (ζ ∘ f) ∎
R : Functor ℂ ℂ
Functor.raw R = rawR
Functor.isFunctor R = isFunctorR
R2 : Functor ℂ ℂ
R2 = F[ R ∘ R ]
ηNat : NaturalTransformation F.identity R
ηNat = {!!}
μNat : NaturalTransformation R2 R
μNat = {!!}
open K.Monad m
backRaw : M.RawMonad
Mraw.R backRaw = R
Mraw.ηNat backRaw = ηNat
Mraw.μNat backRaw = μNat
M.RawMonad.R backRaw = R
M.RawMonad.pureNT backRaw = pureNT
M.RawMonad.joinNT backRaw = joinNT
module _ (m : K.Monad) where
open K.Monad m
open M.RawMonad (backRaw m)
module Mis = M.IsMonad
private
open M.RawMonad backRaw
module R = Functor (M.RawMonad.R backRaw)
backIsMonad : M.IsMonad (backRaw m)
backIsMonad = {!!}
backIsMonad : M.IsMonad backRaw
M.IsMonad.isAssociative backIsMonad {X} = begin
joinT X ∘ R.fmap (joinT X) ≡⟨⟩
join ∘ fmap (joinT X) ≡⟨⟩
join ∘ fmap join ≡⟨ isNaturalForeign ⟩
join ∘ join ≡⟨⟩
joinT X ∘ joinT (R.omap X) ∎
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
where
inv-l = begin
joinT X ∘ pureT (R.omap X) ≡⟨⟩
join ∘ pure ≡⟨ proj₁ isInverse ⟩
𝟙 ∎
inv-r = begin
joinT X ∘ R.fmap (pureT X) ≡⟨⟩
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
𝟙 ∎
back : K.Monad → M.Monad
Monoidal.Monad.raw (back m) = backRaw m
Monoidal.Monad.isMonad (back m) = backIsMonad m
-- I believe all the proofs here should be `refl`.
module _ (m : K.Monad) where
open K.RawMonad (K.Monad.raw m)
private
open K.Monad m
bindEq : ∀ {X Y}
→ K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y}
≡ K.RawMonad.bind (K.Monad.raw m)
bindEq {X} {Y} = begin
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
(λ f → join ∘ fmap f) ≡⟨⟩
(λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩
(λ f → bind f) ≡⟨⟩
bind ∎
where
lem : (f : Arrow X (omap Y))
→ bind (f >>> pure) >>> bind 𝟙
≡ bind f
lem f = begin
bind (f >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _ ⟩
bind ((f >>> pure) >>> bind 𝟙)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (f >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩
bind (f >>> 𝟙)
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
bind f ∎
forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
K.RawMonad.RR (forthRawEq _) = RR
K.RawMonad.ζ (forthRawEq _) = ζ
-- stuck
K.RawMonad.rr (forthRawEq i) = {!!}
K.RawMonad.omap (forthRawEq _) = omap
K.RawMonad.pure (forthRawEq _) = pure
K.RawMonad.bind (forthRawEq i) = bindEq i
fortheq : (m : K.Monad) → forth (back m) ≡ m
fortheq m = K.Monad≡ (forthRawEq m)
module _ (m : M.Monad) where
open M.RawMonad (M.Monad.raw m)
private
open M.Monad m
module KM = K.Monad (forth m)
module R = Functor R
omapEq : KM.omap ≡ Romap
omapEq = refl
bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f
bindEq {X} {Y} {f} = begin
KM.bind f ≡⟨⟩
joinT Y ∘ Rfmap f ≡⟨⟩
bind f ∎
joinEq : ∀ {X} → KM.join ≡ joinT X
joinEq {X} = begin
KM.join ≡⟨⟩
KM.bind 𝟙 ≡⟨⟩
bind 𝟙 ≡⟨⟩
joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩
joinT X ∎
fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap
fmapEq {A} {B} = funExt (λ f → begin
KM.fmap f ≡⟨⟩
KM.bind (f >>> KM.pure) ≡⟨⟩
bind (f >>> pureT _) ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩
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 ∎
)
rawEq : Functor.raw KM.R ≡ Functor.raw R
RawFunctor.omap (rawEq i) = omapEq i
RawFunctor.fmap (rawEq i) = fmapEq i
Req : M.RawMonad.R (backRaw (forth m)) ≡ R
Req = Functor≡ rawEq
open NaturalTransformation ℂ ℂ
pureTEq : M.RawMonad.pureT (backRaw (forth m)) ≡ pureT
pureTEq = funExt (λ X → refl)
pureNTEq : (λ i → NaturalTransformation F.identity (Req i))
[ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
pureNTEq = lemSigP (λ i → propIsNatural F.identity (Req i)) _ _ pureTEq
joinTEq : M.RawMonad.joinT (backRaw (forth m)) ≡ joinT
joinTEq = funExt (λ X → begin
M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
KM.join ≡⟨⟩
joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩
joinT X ∎)
joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))
[ M.RawMonad.joinNT (backRaw (forth m)) ≡ joinNT ]
joinNTEq = lemSigP (λ i → propIsNatural F[ Req i ∘ Req i ] (Req i)) _ _ joinTEq
backRawEq : backRaw (forth m) ≡ M.Monad.raw m
-- stuck
M.RawMonad.R (backRawEq i) = {!!}
M.RawMonad.ηNat (backRawEq i) = {!!}
M.RawMonad.μNat (backRawEq i) = {!!}
M.RawMonad.R (backRawEq i) = Req i
M.RawMonad.pureNT (backRawEq i) = pureNTEq i
M.RawMonad.joinNT (backRawEq i) = joinNTEq i
backeq : (m : M.Monad) → back (forth m) ≡ m
backeq m = M.Monad≡ (backRawEq m)
open import Cubical.GradLemma
eqv : isEquiv M.Monad K.Monad forth
eqv = gradLemma forth back fortheq backeq

253
src/Cat/Category/Monad/Kleisli.agda Normal file
View file

@ -0,0 +1,253 @@
{---
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.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
-- "A monad in the Kleisli form" [voe]
module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
module ℂ = Category ℂ
open ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
-- | Data for a monad.
--
-- Note that (>>=) is not expressible in a general category because objects
-- are not generally types.
record RawMonad : Set ℓ where
field
omap : Object → Object
pure : {X : Object} → ℂ [ X , omap X ]
bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ]
-- | functor map
--
-- This should perhaps be defined in a "Klesli-version" of functors as well?
fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ]
fmap f = bind (pure ∘ f)
-- | Composition of monads aka. the kleisli-arrow.
_>=>_ : {A B C : Object} → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ]
f >=> g = f >>> (bind g)
-- | Flattening nested monads.
join : {A : Object} → ℂ [ omap (omap A) , omap A ]
join = bind 𝟙
------------------
-- * Monad laws --
------------------
-- There may be better names than what I've chosen here.
IsIdentity = {X : Object}
→ bind pure ≡ 𝟙 {omap X}
IsNatural = {X Y : Object} (f : ℂ [ X , omap Y ])
→ pure >>> (bind f) ≡ f
IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ])
→ (bind f) >>> (bind g) ≡ bind (f >=> g)
-- | Functor map fusion.
--
-- This is really a functor law. Should we have a kleisli-representation of
-- functors as well and make them a super-class?
Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
→ fmap (g ∘ f) ≡ fmap g ∘ fmap f
-- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be:
IsNaturalForeign : Set _
IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join
IsInverse : Set _
IsInverse = {X : Object} → join {X} ∘ pure ≡ 𝟙 × join {X} ∘ fmap pure ≡ 𝟙
record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public
field
isIdentity : IsIdentity
isNatural : IsNatural
isDistributive : IsDistributive
-- | Map fusion is admissable.
fusion : Fusion
fusion {g = g} {f} = begin
fmap (g ∘ f) ≡⟨⟩
bind ((f >>> g) >>> pure) ≡⟨ cong bind ℂ.isAssociative ⟩
bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩
bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩
bind (f >>> (pure >>> fmap g)) ≡⟨⟩
bind ((fmap g ∘ pure) ∘ f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩
bind (fmap g ∘ (pure ∘ f)) ≡⟨ sym distrib ⟩
bind (pure ∘ g) ∘ bind (pure ∘ f) ≡⟨⟩
fmap g ∘ fmap f ∎
where
distrib : fmap g ∘ fmap f ≡ bind (fmap g ∘ (pure ∘ f))
distrib = isDistributive (pure ∘ g) (pure ∘ f)
-- | This formulation gives rise to the following endo-functor.
private
rawR : RawFunctor ℂ ℂ
RawFunctor.omap rawR = omap
RawFunctor.fmap rawR = fmap
isFunctorR : IsFunctor ℂ ℂ rawR
IsFunctor.isIdentity isFunctorR = begin
bind (pure ∘ 𝟙) ≡⟨ cong bind (proj₁ ℂ.isIdentity) ⟩
bind pure ≡⟨ isIdentity ⟩
𝟙 ∎
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
bind (pure ∘ (g ∘ f)) ≡⟨⟩
fmap (g ∘ f) ≡⟨ fusion ⟩
fmap g ∘ fmap f ≡⟨⟩
bind (pure ∘ g) ∘ bind (pure ∘ f) ∎
-- FIXME Naming!
R : EndoFunctor ℂ
Functor.raw R = rawR
Functor.isFunctor R = isFunctorR
private
open NaturalTransformation ℂ ℂ
R⁰ : EndoFunctor ℂ
R⁰ = F.identity
R² : EndoFunctor ℂ
R² = F[ R ∘ R ]
module R = Functor R
module R⁰ = Functor R⁰
module R² = Functor R²
pureT : Transformation R⁰ R
pureT A = pure
pureN : Natural R⁰ R pureT
pureN {A} {B} f = begin
pureT B ∘ R⁰.fmap f ≡⟨⟩
pure ∘ f ≡⟨ sym (isNatural _) ⟩
bind (pure ∘ f) ∘ pure ≡⟨⟩
fmap f ∘ pure ≡⟨⟩
R.fmap f ∘ pureT A ∎
joinT : Transformation R² R
joinT C = join
joinN : Natural R² R joinT
joinN f = begin
join ∘ R².fmap f ≡⟨⟩
bind 𝟙 ∘ R².fmap f ≡⟨⟩
R².fmap f >>> bind 𝟙 ≡⟨⟩
fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _ ⟩
bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
≡⟨⟩
bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩
bind (bind (f >>> pure) >>> 𝟙)
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
bind (bind (f >>> pure))
≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩
bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
bind (𝟙 >=> (f >>> pure))
≡⟨ sym (isDistributive _ _) ⟩
bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩
bind 𝟙 >>> fmap f ≡⟨⟩
bind 𝟙 >>> R.fmap f ≡⟨⟩
R.fmap f ∘ bind 𝟙 ≡⟨⟩
R.fmap f ∘ join ∎
pureNT : NaturalTransformation R⁰ R
proj₁ pureNT = pureT
proj₂ pureNT = pureN
joinNT : NaturalTransformation R² R
proj₁ joinNT = joinT
proj₂ joinNT = joinN
isNaturalForeign : IsNaturalForeign
isNaturalForeign = begin
fmap join >>> join ≡⟨⟩
bind (join >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _ ⟩
bind ((join >>> pure) >>> bind 𝟙)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (join >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩
bind (join >>> 𝟙)
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
bind join ≡⟨⟩
bind (bind 𝟙)
≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩
bind (𝟙 >>> bind 𝟙) ≡⟨⟩
bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _) ⟩
bind 𝟙 >>> bind 𝟙 ≡⟨⟩
join >>> join ∎
isInverse : IsInverse
isInverse = inv-l , inv-r
where
inv-l = begin
pure >>> join ≡⟨⟩
pure >>> bind 𝟙 ≡⟨ isNatural _ ⟩
𝟙 ∎
inv-r = begin
fmap pure >>> join ≡⟨⟩
bind (pure >>> pure) >>> bind 𝟙
≡⟨ isDistributive _ _ ⟩
bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
bind ((pure >>> pure) >>> bind 𝟙)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (pure >>> (pure >>> bind 𝟙))
≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩
bind (pure >>> 𝟙)
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
bind pure ≡⟨ isIdentity ⟩
𝟙 ∎
record Monad : Set ℓ where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
private
module _ (raw : RawMonad) where
open RawMonad raw
propIsIdentity : isProp IsIdentity
propIsIdentity x y i = ℂ.arrowsAreSets _ _ x y i
propIsNatural : isProp IsNatural
propIsNatural x y i = λ f
→ ℂ.arrowsAreSets _ _ (x f) (y f) i
propIsDistributive : isProp IsDistributive
propIsDistributive x y i = λ g f
→ ℂ.arrowsAreSets _ _ (x g f) (y g f) i
open IsMonad
propIsMonad : (raw : _) → isProp (IsMonad raw)
IsMonad.isIdentity (propIsMonad raw x y i)
= propIsIdentity raw (isIdentity x) (isIdentity y) i
IsMonad.isNatural (propIsMonad raw x y i)
= propIsNatural raw (isNatural x) (isNatural y) i
IsMonad.isDistributive (propIsMonad raw x y i)
= propIsDistributive raw (isDistributive x) (isDistributive y) i
module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
private
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
Monad≡ : m ≡ n
Monad.raw (Monad≡ i) = eq i
Monad.isMonad (Monad≡ i) = eqIsMonad i

154
src/Cat/Category/Monad/Monoidal.agda Normal file
View file

@ -0,0 +1,154 @@
{---
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.Category
open import Cat.Category.Functor as F
open import Cat.Category.NaturalTransformation
open import Cat.Categories.Fun
module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-- "A monad in the monoidal form" [voe]
private
ℓ = ℓa ⊔ ℓb
open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
open NaturalTransformation ℂ ℂ
record RawMonad : Set ℓ where
field
R : EndoFunctor ℂ
pureNT : NaturalTransformation F.identity R
joinNT : NaturalTransformation F[ R ∘ R ] R
-- Note that `pureT` and `joinT` differs from their definition in the
-- kleisli formulation only by having an explicit parameter.
pureT : Transformation F.identity R
pureT = proj₁ pureNT
pureN : Natural F.identity R pureT
pureN = proj₂ pureNT
joinT : Transformation F[ R ∘ R ] R
joinT = proj₁ joinNT
joinN : Natural F[ R ∘ R ] R joinT
joinN = proj₂ joinNT
Romap = Functor.omap R
Rfmap = Functor.fmap R
bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ]
bind {X} {Y} f = joinT Y ∘ Rfmap f
IsAssociative : Set _
IsAssociative = {X : Object}
→ joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X)
IsInverse : Set _
IsInverse = {X : Object}
→ joinT X ∘ pureT (Romap X) ≡ 𝟙
× joinT X ∘ Rfmap (pureT X) ≡ 𝟙
IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f
IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
→ joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f)
≡ joinT Z ∘ Rfmap (joinT Z ∘ Rfmap g ∘ f)
record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public
field
isAssociative : IsAssociative
isInverse : IsInverse
private
module R = Functor R
module ℂ = Category ℂ
isNatural : IsNatural
isNatural {X} {Y} f = begin
joinT Y ∘ R.fmap f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩
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 ∎
isDistributive : IsDistributive
isDistributive {X} {Y} {Z} g f = sym aux
where
module R² = Functor F[ R ∘ R ]
distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
→ R.fmap (a ∘ b ∘ c)
≡ R.fmap a ∘ R.fmap b ∘ R.fmap c
distrib3 {a = a} {b} {c} = begin
R.fmap (a ∘ b ∘ c) ≡⟨ R.isDistributive ⟩
R.fmap (a ∘ b) ∘ R.fmap c ≡⟨ cong (_∘ _) R.isDistributive ⟩
R.fmap a ∘ R.fmap b ∘ R.fmap c ∎
aux = begin
joinT Z ∘ R.fmap (joinT Z ∘ R.fmap g ∘ f)
≡⟨ cong (λ φ → joinT Z ∘ φ) distrib3 ⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ R.fmap (R.fmap g) ∘ R.fmap f)
≡⟨⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ R².fmap g ∘ R.fmap f)
≡⟨ cong (_∘_ (joinT Z)) (sym ℂ.isAssociative) ⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ (R².fmap g ∘ R.fmap f))
≡⟨ ℂ.isAssociative ⟩
(joinT Z ∘ R.fmap (joinT Z)) ∘ (R².fmap g ∘ R.fmap f)
≡⟨ cong (λ φ → φ ∘ (R².fmap g ∘ R.fmap f)) isAssociative ⟩
(joinT Z ∘ joinT (R.omap Z)) ∘ (R².fmap g ∘ R.fmap f)
≡⟨ ℂ.isAssociative ⟩
joinT Z ∘ joinT (R.omap Z) ∘ R².fmap g ∘ R.fmap f
≡⟨⟩
((joinT Z ∘ joinT (R.omap Z)) ∘ R².fmap g) ∘ R.fmap f
≡⟨ cong (_∘ R.fmap f) (sym ℂ.isAssociative) ⟩
(joinT Z ∘ (joinT (R.omap Z) ∘ R².fmap g)) ∘ R.fmap f
≡⟨ cong (λ φ → φ ∘ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩
(joinT Z ∘ (R.fmap g ∘ joinT Y)) ∘ R.fmap f
≡⟨ cong (_∘ R.fmap f) ℂ.isAssociative ⟩
joinT Z ∘ R.fmap g ∘ joinT Y ∘ R.fmap f
≡⟨ sym (Category.isAssociative ℂ) ⟩
joinT Z ∘ R.fmap g ∘ (joinT Y ∘ R.fmap f)
∎
record Monad : Set ℓ where
field
raw : RawMonad
isMonad : IsMonad raw
open IsMonad isMonad public
private
module _ {m : RawMonad} where
open RawMonad m
propIsAssociative : isProp IsAssociative
propIsAssociative x y i {X}
= Category.arrowsAreSets ℂ _ _ (x {X}) (y {X}) i
propIsInverse : isProp IsInverse
propIsInverse x y i {X} = e1 i , e2 i
where
xX = x {X}
yX = y {X}
e1 = Category.arrowsAreSets ℂ _ _ (proj₁ xX) (proj₁ yX)
e2 = Category.arrowsAreSets ℂ _ _ (proj₂ xX) (proj₂ yX)
open IsMonad
propIsMonad : (raw : _) → isProp (IsMonad raw)
IsMonad.isAssociative (propIsMonad raw a b i) j
= propIsAssociative {raw}
(isAssociative a) (isAssociative b) i j
IsMonad.isInverse (propIsMonad raw a b i)
= propIsInverse {raw}
(isInverse a) (isInverse b) i
module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
private
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
Monad≡ : m ≡ n
Monad.raw (Monad≡ i) = eq i
Monad.isMonad (Monad≡ i) = eqIsMonad i

211
src/Cat/Category/Monad/Voevodsky.agda Normal file
View file

@ -0,0 +1,211 @@
{-
This module provides construction 2.3 in [voe]
-}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
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.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.Categories.Fun
module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
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
record §1 : Set ℓ where
open M
field
fmap : Fmap ℂ ℂ omap
join : {A : Object} → ℂ [ omap (omap A) , omap A ]
Rraw : RawFunctor ℂ ℂ
Rraw = record
{ omap = omap
; fmap = fmap
}
field
RisFunctor : IsFunctor ℂ ℂ Rraw
R : EndoFunctor ℂ
R = record
{ raw = Rraw
; isFunctor = RisFunctor
}
pureT : (X : Object) → Arrow X (omap X)
pureT X = pure {X}
field
pureN : Natural F.identity R pureT
pureNT : NaturalTransformation F.identity R
pureNT = pureT , pureN
joinT : (A : Object) → ℂ [ omap (omap A) , omap A ]
joinT A = join {A}
field
joinN : Natural F[ R ∘ R ] R joinT
joinNT : NaturalTransformation F[ R ∘ R ] R
joinNT = joinT , joinN
rawMnd : RawMonad
rawMnd = record
{ R = R
; pureNT = pureNT
; joinNT = joinNT
}
field
isMnd : IsMonad rawMnd
toMonad : Monad
toMonad = record
{ raw = rawMnd
; isMonad = isMnd
}
record §2 : Set ℓ where
open K
field
bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ]
rawMnd : RawMonad
rawMnd = record
{ omap = omap
; pure = pure
; bind = bind
}
field
isMnd : IsMonad rawMnd
toMonad : Monad
toMonad = record
{ raw = rawMnd
; isMonad = isMnd
}
§1-fromMonad : (m : M.Monad) → §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
-- voe-2-3-1-fromMonad : (m : M.Monad) → voe.§2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
§1-fromMonad m = record
{ fmap = Functor.fmap R
; RisFunctor = Functor.isFunctor R
; pureN = pureN
; join = λ {X} → joinT X
; joinN = joinN
; isMnd = M.Monad.isMonad m
}
where
raw = M.Monad.raw m
R = M.RawMonad.R raw
pureT = M.RawMonad.pureT raw
pureN = M.RawMonad.pureN raw
joinT = M.RawMonad.joinT raw
joinN = M.RawMonad.joinN raw
§2-fromMonad : (m : K.Monad) → §2-3.§2 (K.Monad.omap m) (K.Monad.pure m)
§2-fromMonad m = record
{ bind = K.Monad.bind m
; isMnd = K.Monad.isMonad m
}
module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
private
Monoidal→Kleisli : M.Monad → K.Monad
Monoidal→Kleisli = proj₁ Monoidal≃Kleisli
Kleisli→Monoidal : K.Monad → M.Monad
Kleisli→Monoidal = inverse Monoidal≃Kleisli
forth : §2-3.§1 omap pure → §2-3.§2 omap pure
forth = §2-fromMonad ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad
back : §2-3.§2 omap pure → §2-3.§1 omap pure
back = §1-fromMonad ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad
forthEq : ∀ m → _ ≡ _
forthEq m = begin
(forth ∘ back) m ≡⟨⟩
-- In full gory detail:
( §2-fromMonad
∘ Monoidal→Kleisli
∘ §2-3.§1.toMonad
∘ §1-fromMonad
∘ Kleisli→Monoidal
∘ §2-3.§2.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( §2-fromMonad
∘ Monoidal→Kleisli
∘ Kleisli→Monoidal
∘ §2-3.§2.toMonad
) m ≡⟨ u ⟩
-- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-- I should be able to prove this using congruence and `lem` below.
( §2-fromMonad
∘ §2-3.§2.toMonad
) m ≡⟨⟩
( §2-fromMonad
∘ §2-3.§2.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m ∎
where
lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
lem = {!!} -- verso-recto Monoidal≃Kleisli
t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad)
≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
t = cong (λ φ → §2-fromMonad ∘ (λ{ {ω} → φ {{!????!}}}) ∘ §2-3.§2.toMonad) {!lem!}
u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
u = cong (λ φ → φ m) t
backEq : ∀ m → (back ∘ forth) m ≡ m
backEq m = begin
(back ∘ forth) m ≡⟨⟩
( §1-fromMonad
∘ Kleisli→Monoidal
∘ §2-3.§2.toMonad
∘ §2-fromMonad
∘ Monoidal→Kleisli
∘ §2-3.§1.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( §1-fromMonad
∘ Kleisli→Monoidal
∘ Monoidal→Kleisli
∘ §2-3.§1.toMonad
) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
( §1-fromMonad
∘ §2-3.§1.toMonad
) 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)
voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
voe-isEquiv = gradLemma forth back forthEq backEq
equiv-2-3 : §2-3.§1 omap pure ≃ §2-3.§2 omap pure
equiv-2-3 = forth , voe-isEquiv

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

@ -12,10 +12,14 @@ module _ (ℓa ℓb : Level) where
private
ℓ = lsuc (ℓa ⊔ ℓb)
-- Might not need this to be able to form products of categories!
postulate unprovable : IsCategory (Cat.RawCat ℓa ℓb)
open HasProducts (Cat.hasProducts unprovable)
-- *If* the category of categories existed `_×_` would be equivalent to the
-- one brought into scope by doing:
--
-- open HasProducts (Cat.hasProducts unprovable) using (_×_)
--
-- 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 ℂ 𝔻
record RawMonoidalCategory : Set ℓ where
field
@ -23,9 +27,10 @@ module _ (ℓa ℓb : Level) where
open Category category public
field
{{hasProducts}} : HasProducts category
mempty : Object
empty : Object
-- aka. tensor product, monoidal product.
mappend : Functor (category × category) category
append : Functor (category × category) category
open HasProducts hasProducts public
record MonoidalCategory : Set ℓ where
field
@ -36,10 +41,10 @@ module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
module MC = MonoidalCategory ℂ
open HasProducts MC.hasProducts
open MonoidalCategory ℂ public
record Monoid : Set ℓ where
field
carrier : MC.Object
mempty : MC.Arrow (carrier × carrier) carrier
mappend : MC.Arrow MC.mempty carrier
carrier : Object
mempty : Arrow empty carrier
mappend : Arrow (carrier × carrier) carrier

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

@ -21,15 +21,24 @@
module Cat.Category.NaturalTransformation where
open import Agda.Primitive
open import Data.Product
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
module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
(ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙)
private
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
module _ (F G : Functor ℂ 𝔻) where
private
@ -37,28 +46,25 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
module G = Functor G
-- What do you call a non-natural tranformation?
Transformation : Set (ℓc ⊔ ℓd')
Transformation = (C : Object ℂ) → 𝔻 [ F.func* C , G.func* C ]
Transformation = (C : Object ℂ) → 𝔻 [ F.omap C , G.omap C ]
Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
Natural θ
= {A B : Object ℂ}
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
→ 𝔻 [ θ B ∘ F.fmap f ] ≡ 𝔻 [ G.fmap f ∘ θ A ]
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
-- TODO: Since naturality is a mere proposition this principle can be
-- simplified.
-- Think I need propPi and that arrows are sets
propIsNatural : (θ : _) → isProp (Natural θ)
propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
NaturalTransformation≡ : {α β : NaturalTransformation}
→ (eq₁ : α .proj₁ ≡ β .proj₁)
→ (eq₂ : PathP
(λ i → {A B : Object ℂ} (f : ℂ [ A , B ])
→ 𝔻 [ eq₁ i B ∘ F.func→ f ]
≡ 𝔻 [ G.func→ f ∘ eq₁ i A ])
(α .proj₂) (β .proj₂))
→ α ≡ β
NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝟙 𝔻
@ -72,8 +78,7 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
module F = Functor F
F→ = F.func→
module 𝔻 = Category 𝔻
F→ = F.fmap
identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
identity F = identityTrans F , identityNatural F
@ -89,13 +94,27 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
𝔻 [ T[ θ ∘ η ] B ∘ F.func→ f ] ≡⟨⟩
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩
𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩
𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ] ∎
𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ] ≡⟨⟩
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
𝔻 [ θ B ∘ 𝔻 [ G.fmap f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
𝔻 [ 𝔻 [ θ B ∘ G.fmap f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
𝔻 [ 𝔻 [ H.fmap f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
𝔻 [ H.fmap f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H.fmap f ∘ T[ θ ∘ η ] A ] ∎
module _ {F G : Functor ℂ 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
open Category 𝔻
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
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)

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

@ -1,54 +1,68 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Category.Product where
open import Agda.Primitive
open import Cubical
open import Data.Product as P hiding (_×_)
open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂)
open import Cat.Category
open import Cat.Category hiding (module Propositionality)
open Category
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
IsProduct π₁ π₂
= ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
→ ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
open Category ℂ
-- Tip from Andrea; Consider this style for efficiency:
-- record IsProduct {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
-- {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) : Set (ℓa ⊔ ℓb) where
-- field
-- issProduct : ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
-- → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ P.× ℂ [ π₂ ∘ x ] ≡ x₂)
module _ (A B : Object) where
record RawProduct : Set (ℓa ⊔ ℓb) where
no-eta-equality
field
object : Object
proj₁ : ℂ [ object , A ]
proj₂ : ℂ [ object , B ]
-- open IsProduct
-- FIXME Not sure this is actually a proposition - so this name is
-- misleading.
record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
open RawProduct raw public
field
isProduct : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
→ ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g)
record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where
no-eta-equality
field
obj : Object ℂ
proj₁ : ℂ [ obj , A ]
proj₂ : ℂ [ obj , B ]
{{isProduct}} : IsProduct ℂ proj₁ proj₂
-- | Arrow product
_P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
→ ℂ [ X , object ]
_P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
_P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
→ ℂ [ X , obj ]
_P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂)
record Product : Set (ℓa ⊔ ℓb) where
field
raw : RawProduct
isProduct : IsProduct raw
record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
field
product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
open IsProduct isProduct public
open Product
record HasProducts : Set (ℓa ⊔ ℓb) where
field
product : ∀ (A B : Object) → Product A B
_×_ : (A B : Object ℂ) → Object ℂ
A × B = Product.obj (product A B)
-- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
-- It's a "parallel" product
_|×|_ : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
→ ℂ [ A × B , A' × B' ]
_|×|_ {A = A} {A' = A'} {B = B} {B' = B'} a b
= product A' B'
P[ ℂ [ a ∘ (product A B) .proj₁ ]
× ℂ [ b ∘ (product A B) .proj₂ ]
]
_×_ : Object → Object → Object
A × B = Product.object (product A B)
-- | Parallel product of arrows
--
-- The product mentioned in awodey in Def 6.1 is not the regular product of
-- arrows. It's a "parallel" product
module _ {A A' B B' : Object} where
open Product
open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
_|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
f |×| g = product A' B'
P[ ℂ [ f ∘ fst ]
× ℂ [ 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 = {!!}
propHasProducts : isProp (HasProducts ℂ)
propHasProducts = {!!}

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

@ -5,60 +5,76 @@ module Cat.Category.Yoneda where
open import Agda.Primitive
open import Data.Product
open import Cubical
open import Cubical.NType.Properties
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Equality
open Equality.Data.Product
-- TODO: We want to avoid defining the yoneda embedding going through the
-- category of categories (since it doesn't exist).
open import Cat.Categories.Cat using (RawCat)
open import Cat.Categories.Fun
open import Cat.Categories.Sets
open import Cat.Categories.Cat
module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where
open import Cat.Categories.Fun
open import Cat.Categories.Sets
module Cat = Cat.Categories.Cat
open import Cat.Category.Exponential
open Functor
𝓢 = Sets ℓ
open Fun (opposite ℂ) 𝓢
module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
private
Catℓ : Category _ _
Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
prshf = presheaf {ℂ = ℂ}
𝓢 = Sets ℓ
open Fun (opposite ℂ) 𝓢
prshf = presheaf ℂ
module ℂ = Category ℂ
_⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ
A ⇑ B = (exponent A B) .obj
where
open HasExponentials (Cat.hasExponentials ℓ unprovable)
-- 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
module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
:func→: : NaturalTransformation (prshf A) (prshf B)
:func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
fmap : Transformation (prshf A) (prshf B)
fmap C x = ℂ [ f ∘ x ]
module _ {c : Category.Object ℂ} where
eqTrans : (λ _ → Transformation (prshf c) (prshf c))
[ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
fmapNatural : Natural (prshf A) (prshf B) fmap
fmapNatural g = funExt λ _ → ℂ.isAssociative
open import Cubical.NType.Properties
open import Cat.Categories.Fun
:ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c}
:ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
fmapNT : NaturalTransformation (prshf A) (prshf B)
fmapNT = fmap , fmapNatural
rawYoneda : RawFunctor ℂ Fun
RawFunctor.omap rawYoneda = prshf
RawFunctor.fmap rawYoneda = fmapNT
open RawFunctor rawYoneda hiding (fmap)
isIdentity : IsIdentity
isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
isDistributive : IsDistributive
isDistributive {A} {B} {C} {f = f} {g}
= lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq
where
T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C}
eqq : (X : ℂ.Object) → (x : ℂ [ X , A ])
→ fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x
eqq X x = begin
fmap (ℂ [ g ∘ f ]) X x ≡⟨⟩
ℂ [ ℂ [ g ∘ f ] ∘ x ] ≡⟨ sym ℂ.isAssociative ⟩
ℂ [ g ∘ ℂ [ f ∘ x ] ] ≡⟨⟩
ℂ [ g ∘ fmap f X x ] ≡⟨⟩
T[ fmap g ∘ fmap f ]' X x ∎
eq : fmap (ℂ [ g ∘ f ]) ≡ T[ fmap g ∘ fmap f ]'
eq = begin
fmap (ℂ [ g ∘ f ]) ≡⟨ funExt (λ X → funExt λ α → eqq X α) ⟩
T[ fmap g ∘ fmap f ]' ∎
instance
isFunctor : IsFunctor ℂ Fun rawYoneda
IsFunctor.isIdentity isFunctor = isIdentity
IsFunctor.isDistributive isFunctor = isDistributive
yoneda : Functor ℂ Fun
yoneda = record
{ raw = record
{ func* = prshf
; func→ = :func→:
}
; isFunctor = record
{ isIdentity = :ident:
; isDistributive = {!!}
}
}
Functor.raw yoneda = rawYoneda
Functor.isFunctor yoneda = isFunctor

44
src/Cat/Wishlist.agda
View file

@ -1,15 +1,41 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Wishlist where
open import Level
open import Level hiding (suc)
open import Cubical
open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
open import Data.Nat using (_≤_ ; z≤n ; s≤s ; zero ; suc)
open import Agda.Builtin.Sigma
postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
open import Cubical.NType.Properties
step : ∀ {ℓ} {A : Set ℓ} → isContr A → (x y : A) → isContr (x ≡ y)
step (a , contr) x y = {!p , c!}
-- where
-- p : x ≡ y
-- p = begin
-- x ≡⟨ sym (contr x) ⟩
-- a ≡⟨ contr y ⟩
-- y ∎
-- c : (q : x ≡ y) → p ≡ q
-- c q i j = contr (p {!!}) {!!}
-- Contractible types have any given homotopy level.
contrInitial : {ℓ : Level} {A : Set ℓ} → ∀ n → isContr A → HasLevel n A
contrInitial ⟨-2⟩ contr = contr
-- lem' (S ⟨-2⟩) (a , contr) = {!step!}
contrInitial (S ⟨-2⟩) (a , contr) x y = begin
x ≡⟨ sym (contr x) ⟩
a ≡⟨ contr y ⟩
y ∎
contrInitial (S (S n)) contr x y = {!lvl!} -- Why is this not well-founded?
where
c : isContr (x ≡ y)
c = step contr x y
lvl : HasLevel (S n) (x ≡ y)
lvl = contrInitial {A = x ≡ y} (S n) c
module _ {ℓ : Level} {A : Set ℓ} where
-- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I
-- can't find it.
postulate propHasLevel : ∀ n → isProp (HasLevel n A)
isSetIsProp : isProp (isSet A)
isSetIsProp = propHasLevel (S (S ⟨-2⟩))
ntypeCommulative : ∀ {n m} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
ntypeCommulative {n = zero} {m} z≤n lvl = {!contrInitial ⟨ m ⟩₋₂ lvl!}
ntypeCommulative {n = .(suc _)} {.(suc _)} (s≤s x) lvl = {!!}