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-02-25 15:38:23 +01:00
parent 29e9ef689a 7518a642f6
commit 9c8bc1b1f4
17 changed files with 746 additions and 332 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
BACKLOG.md
View file

@ -4,3 +4,11 @@ Backlog
Prove univalence for various categories
Prove postulates in `Cat.Wishlist`
* Functor ✓
* Applicative Functor ✗
* Lax monoidal functor ✗
* Monoidal functor ✗
* Tensorial strength ✗
* Category ✓
* Monoidal category ✗

21
CHANGELOG.md
View file

@ -1,6 +1,27 @@
Changelog
=========
Version 1.3.0
-------------
Removed unused modules and streamlined things more: All specific categories are
in the namespace `Cat.Categories`.
Lemmas about categories are now in the appropriate record e.g. `IsCategory`.
Also changed how category reexports stuff.
Rename the module Properties to Yoneda - because that's all it talks about now.
Rename Opposite to opposite
Add documentation in Category-module
Formulation of monads in two ways; the "monoidal-" and "kleisli-" form.
WIP: Equivalence of these two formulations
Also use hSets in a few concrete categories rather than just pure `Set`.
Version 1.2.0
-------------
This version is mainly a huge refactor.

10
src/Cat.agda
View file

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

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

@ -12,6 +12,7 @@ open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Category.Exponential
open import Cat.Category.NaturalTransformation
open import Cat.Equality
open Equality.Data.Product
@ -23,14 +24,14 @@ open Category using (Object ; 𝟙)
module _ (ℓ ℓ' : Level) where
private
module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
assc = Functor≡ refl refl
module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
ident-r : F ∘f identity ≡ F
ident-r : F[ F ∘ identity ] ≡ F
ident-r = Functor≡ refl refl
ident-l : identity ∘f F ≡ F
ident-l : F[ identity ∘ F ] ≡ F
ident-l = Functor≡ refl refl
RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
@ -39,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
{ Object = Category ℓ ℓ'
; Arrow = Functor
; 𝟙 = identity
; _∘_ = _∘f_
; _∘_ = F[_∘_]
}
private
open RawCategory RawCat
@ -176,9 +177,10 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
Catℓ = Cat ℓ ℓ unprovable
module _ (ℂ 𝔻 : Category ℓ ℓ) where
open Fun ℂ 𝔻 renaming (identity to idN)
private
:obj: : Object Catℓ
:obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
:obj: = Fun
:func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
:func*: (F , A) = func* F A
@ -234,10 +236,11 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
-- where
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
-- Unfortunately the equational version has some ambigous arguments.
:ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
:ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
:ident: = begin
:func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
:func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩
:func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩
𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩

28
src/Cat/CwF.agda → src/Cat/Categories/CwF.agda
View file

@ -1,4 +1,4 @@
module Cat.CwF where
module Cat.Categories.CwF where
open import Agda.Primitive
open import Data.Product
@ -22,27 +22,27 @@ module _ {ℓa ℓb : Level} where
Substitutions = Arrow ℂ
field
-- A functor T
T : Functor (Opposite ℂ) (Fam ℓa ℓb)
T : Functor (opposite ℂ) (Fam ℓa ℓb)
-- Empty context
[] : Terminal ℂ
private
module T = Functor T
Type : (Γ : Object ℂ) → Set ℓa
Type Γ = proj₁ (T.func* Γ)
Type Γ = proj₁ (proj₁ (T.func* Γ))
module _ {Γ : Object ℂ} {A : Type Γ} where
module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
k : Σ (proj₁ (func* T B) → proj₁ (func* 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)
k₁ = proj₁ k
k₂ : ({x : proj₁ (func* T B)} →
proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
k₂ = proj₂ k
-- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-- k : Σ (proj₁ (func* T B) → proj₁ (func* 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)
-- k₁ = proj₁ k
-- k₂ : ({x : proj₁ (func* T B)} →
-- proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
-- k₂ = proj₂ k
record ContextComprehension : Set (ℓa ⊔ ℓb) where
field

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

@ -3,9 +3,11 @@ module Cat.Categories.Fam where
open import Agda.Primitive
open import Data.Product
open import Cubical
import Function
open import Cubical
open import Cubical.Universe
open import Cat.Category
open import Cat.Equality
@ -13,40 +15,54 @@ open Equality.Data.Product
module _ (ℓa ℓb : Level) where
private
Obj' = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
Arr : Obj' → Obj' → Set (ℓa ⊔ ℓb)
Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x))
one : {o : Obj'} → Arr o o
proj₁ one = λ x → x
proj₂ one = λ b → b
_∘_ : {a b c : Obj'} → Arr b c → Arr a b → Arr a c
Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb})
Arr : Object → Object → Set (ℓa ⊔ ℓb)
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
𝟙 : {A : Object} → Arr A A
proj₁ 𝟙 = λ x → x
proj₂ 𝟙 = λ b → b
_∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
(g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
_⟨_∘_⟩ : {a b : Obj'} → (c : Obj') → Arr b c → Arr a b → Arr a c
c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
isAssociative = Σ≡ refl refl
module _ {A B : Obj'} {f : Arr A B} where
isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
RawFam = record
{ Object = Obj'
{ Object = Object
; Arrow = Arr
; 𝟙 = one
; 𝟙 = λ { {A} → 𝟙 {A = A}}
; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
}
open RawCategory RawFam hiding (Object ; 𝟙)
isAssociative : IsAssociative
isAssociative = Σ≡ refl refl
isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
open import Cubical.NType.Properties
open import Cubical.Sigma
instance
isCategory : IsCategory RawFam
isCategory = record
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {A} {B} {C} {D} {f} {g} {h}
; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
; arrowsAreSets = {!!}
; arrowsAreSets = λ {
{((A , hA) , famA)}
{((B , hB) , famB)}
→ setSig
{sA = setPi λ _ → hB}
{sB = λ f →
let
helpr : isSet ((a : A) → proj₁ (famA a) → proj₁ (famB (f a)))
helpr = setPi λ a → setPi λ _ → proj₂ (famB (f a))
-- It's almost like above, but where the first argument is
-- implicit.
res : isSet ({a : A} → proj₁ (famA a) → proj₁ (famB (f a)))
res = {!!}
in res
}
}
; univalent = {!!}
}

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

@ -7,8 +7,6 @@ open import Data.Product
open import Cat.Category
open IsCategory
data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
empty : {a : A} → Path R a a
cons : {a b c : A} → R b c → Path R a b → Path R a c

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

@ -2,99 +2,29 @@
module Cat.Categories.Fun where
open import Agda.Primitive
open import Cubical
open import Function
open import Data.Product
import Cubical.GradLemma
module UIP = Cubical.GradLemma
open import Cubical.Sigma
open import Cubical.NType
open import Cubical.NType.Properties
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.NType.Properties
open import Cat.Category
open import Cat.Category.Functor
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 _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙)
open Functor
module _ (F G : Functor ℂ 𝔻) where
private
module F = Functor F
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 ]
Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
Natural θ
= {A B : Object ℂ}
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
-- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
-- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
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
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝟙 𝔻
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
module F = Functor F
F→ = F.func→
module 𝔻 = Category 𝔻
identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
identityNat F = identityTrans F , identityNatural F
module _ {F G H : Functor ℂ 𝔻} where
private
module F = Functor F
module G = Functor G
module H = Functor H
_∘nt_ : Transformation G H → Transformation F G → Transformation F H
(θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]
NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
𝔻 [ (θ ∘nt η) 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 ∘ (θ ∘nt η) A ] ∎
where
open Category 𝔻
NatComp = _:⊕:_
module NT = NaturalTransformation ℂ 𝔻
open NT public
private
module 𝔻 = Category 𝔻
@ -125,11 +55,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
ηNat = proj₂ η'
ζNat = proj₂ ζ'
L : NaturalTransformation A D
L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
L = (NT[_∘_] {A} {C} {D} ζ' (NT[_∘_] {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {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))
@ -147,29 +77,28 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
f' C ∎
eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
eq-l C = proj₂ 𝔻.isIdentity
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
ident-l = lemSig allNatural _ _ (funExt eq-l)
:ident:
: (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
× (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
:ident: = ident-r , ident-l
isIdentity
: (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
× (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
isIdentity = ident-r , ident-l
-- Functor categories. Objects are functors, arrows are natural transformations.
RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
RawFun = record
{ Object = Functor ℂ 𝔻
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identityNat F
; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
; 𝟙 = λ {F} → NT.identity F
; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
}
instance
:isCategory: : IsCategory RawFun
:isCategory: = record
{ isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
; isIdentity = λ {A B} → :ident: {A} {B}
; isIdentity = λ {A B} → isIdentity {A} {B}
; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
; univalent = {!!}
}
@ -179,12 +108,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open import Cat.Categories.Sets
open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
-- Restrict the functors to Presheafs.
RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
RawPresh = record
{ Object = Presheaf ℂ
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identityNat F
; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
; 𝟙 = λ {F} → identity F
; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
}

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

@ -88,7 +88,7 @@ module _ {ℓa ℓb : Level} where
-- Contravariant Presheaf
Presheaf : Set (ℓa ⊔ lsuc ℓb)
Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
-- The "co-yoneda" embedding.
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
@ -106,7 +106,7 @@ module _ {ℓa ℓb : Level} where
open Category ℂ
-- Alternate name: `yoneda`
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ raw = record
{ func* = λ A → ℂ [ A , B ] , arrowsAreSets

179
src/Cat/Category.agda
View file

@ -1,3 +1,32 @@
-- | Univalent categories
--
-- This module defines:
--
-- Categories
-- ==========
--
-- Types
-- ------
--
-- Object, Arrow
--
-- Data
-- ----
-- 𝟙; the identity arrow
-- _∘_; function composition
--
-- Laws
-- ----
--
-- associativity, identity, arrows form sets, univalence.
--
-- Lemmas
-- ------
--
-- 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
@ -16,6 +45,11 @@ open import Cubical.NType.Properties using ( propIsEquiv )
open import Cat.Wishlist
-----------------
-- * Utilities --
-----------------
-- | Unique existensials.
∃! : ∀ {a b} {A : Set a}
→ (A → Set b) → Set (a ⊔ b)
∃! = ∃!≈ _≡_
@ -25,6 +59,15 @@ open import Cat.Wishlist
syntax ∃!-syntax (λ x → B) = ∃![ x ] B
-----------------
-- * Categories --
-----------------
-- | Raw categories
--
-- This record desribes the data that a category consist of as well as some laws
-- about these. The laws defined are the types the propositions - not the
-- witnesses to them!
record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
no-eta-equality
field
@ -35,12 +78,18 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
infixl 10 _∘_
-- | Operations on data
domain : { a b : Object } → Arrow a b → Object
domain {a = a} _ = a
codomain : { a b : Object } → Arrow a b → Object
codomain {b = b} _ = b
-- | Laws about the data
-- TODO: 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}
→ h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
@ -91,14 +140,18 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
id-to-iso : (A B : Object) → A ≡ B → A ≅ B
id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
-- TODO: might want to implement isEquiv
-- differently, there are 3
-- equivalent formulations in the book.
Univalent : Set (ℓa ⊔ ℓb)
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
-- | The mere proposition of being a category.
--
-- Also defines a few lemmas:
--
-- iso-is-epi : Isomorphism f → Epimorphism {X = X} f
-- iso-is-mono : Isomorphism f → Monomorphism {X = X} f
--
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
open RawCategory ℂ
open RawCategory ℂ public
open Univalence ℂ public
field
isAssociative : IsAssociative
@ -106,11 +159,42 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
arrowsAreSets : ArrowsAreSets
univalent : Univalent isIdentity
-- `IsCategory` is a mere proposition.
-- Some common lemmas about categories.
module _ {A B : Object} {X : Object} (f : Arrow A B) where
iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym (fst isIdentity) ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩
g₁ ∘ 𝟙 ≡⟨ fst isIdentity ⟩
g₁ ∎
iso-is-mono : Isomorphism f → Monomorphism {X = X} f
iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
begin
g₀ ≡⟨ sym (snd isIdentity) ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
𝟙 ∘ g₁ ≡⟨ snd isIdentity ⟩
g₁ ∎
iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
-- | Propositionality of being a category
--
-- 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
open IsCategory ℂ
open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
open import Cubical.NType
open import Cubical.NType.Properties
@ -189,14 +273,17 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
propIsCategory : isProp (IsCategory C)
propIsCategory = done
-- | Univalent categories
--
-- Just bundles up the data with witnesses inhabting the propositions.
record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
field
raw : RawCategory ℓa ℓb
{{isCategory}} : IsCategory raw
open RawCategory raw public
open IsCategory isCategory public
-- | Syntax for arrows- and composition in a given category.
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Category ℂ
_[_,_] : (A : Object) → (B : Object) → Set ℓb
@ -205,48 +292,48 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
_[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
_[_∘_] = _∘_
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
-- | The opposite category
--
-- The opposite category is the category where the direction of the arrows are
-- flipped.
module Opposite {ℓa ℓb : Level} where
module _ (ℂ : Category ℓa ℓb) where
open Category ℂ
private
opRaw : RawCategory ℓa ℓb
RawCategory.Object opRaw = Object
RawCategory.Arrow opRaw = Function.flip Arrow
RawCategory.𝟙 opRaw = 𝟙
RawCategory._∘_ opRaw = Function.flip _∘_
OpRaw : RawCategory ℓa ℓb
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 = {!!}
OpIsCategory : IsCategory OpRaw
IsCategory.isAssociative OpIsCategory = sym isAssociative
IsCategory.isIdentity OpIsCategory = swap isIdentity
IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets
IsCategory.univalent OpIsCategory = {!!}
opposite : Category ℓa ℓb
raw opposite = opRaw
Category.isCategory opposite = opIsCategory
Opposite : Category ℓa ℓb
raw Opposite = OpRaw
Category.isCategory Opposite = OpIsCategory
-- 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
-- definitionally equal. I.e; a thing that would normally be provable in one
-- line now takes 13!! Admittedly it's a simple proof.
module _ {ℂ : Category ℓa ℓb} where
open Category ℂ
private
-- Since they really are definitionally equal we just need to pick apart
-- the data-type.
rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
RawCategory.Object (rawInv _) = Object
RawCategory.Arrow (rawInv _) = Arrow
RawCategory.𝟙 (rawInv _) = 𝟙
RawCategory._∘_ (rawInv _) = _∘_
-- 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
-- definitionally equal. I.e; a thing that would normally be provable in one
-- line now takes more than 20!!
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
private
open RawCategory
module C = Category ℂ
rawOp : Category.raw (Opposite (Opposite ℂ)) ≡ Category.raw ℂ
Object (rawOp _) = C.Object
Arrow (rawOp _) = C.Arrow
𝟙 (rawOp _) = C.𝟙
_∘_ (rawOp _) = C._∘_
open Category
open IsCategory
module IsCat = IsCategory (ℂ .isCategory)
rawIsCat : (i : I) → IsCategory (rawOp i)
isAssociative (rawIsCat i) = IsCat.isAssociative
isIdentity (rawIsCat i) = IsCat.isIdentity
arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets
univalent (rawIsCat i) = IsCat.univalent
-- TODO: Define and use Monad≡
oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
Category.raw (oppositeIsInvolution i) = rawInv i
Category.isCategory (oppositeIsInvolution x) = {!!}
Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
raw (Opposite-is-involution i) = rawOp i
isCategory (Opposite-is-involution i) = rawIsCat i
open Opposite public

46
src/Cat/Category/Bij.agda
View file

@ -1,46 +0,0 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Category.Bij where
open import Cubical hiding ( Id )
open import Cubical.FromStdLib
module _ {A : Set} {a : A} {P : A → Set} where
Q : A → Set
Q a = A
t : Σ[ a ∈ A ] P a → Q a
t (a , Pa) = a
u : Q a → Σ[ a ∈ A ] P a
u a = a , {!!}
tu-bij : (a : Q a) → (t ∘ u) a ≡ a
tu-bij a = refl
v : P a → Q a
v x = {!!}
w : Q a → P a
w x = {!!}
vw-bij : (a : P a) → (w ∘ v) a ≡ a
vw-bij a = {!!}
-- tubij a with (t ∘ u) a
-- ... | q = {!!}
data Id {A : Set} (a : A) : Set where
id : A → Id a
data Id' {A : Set} (a : A) : Set where
id' : A → Id' a
T U : Set
T = Id a
U = Id' a
f : T → U
f (id x) = id' x
g : U → T
g (id' x) = id x
fg-bij : (x : U) → (f ∘ g) x ≡ x
fg-bij (id' x) = {!!}

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

@ -51,7 +51,7 @@ module _
(F : RawFunctor ℂ 𝔻)
where
private
module 𝔻 = IsCategory (isCategory 𝔻)
module 𝔻 = Category 𝔻
propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record
@ -69,7 +69,7 @@ module _
{F : I → RawFunctor ℂ 𝔻}
where
private
module 𝔻 = IsCategory (isCategory 𝔻)
module 𝔻 = Category 𝔻
IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ
IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ]
@ -124,8 +124,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
; isDistributive = dist
}
_∘f_ : Functor A C
raw _∘f_ = _∘fr_
F[_∘_] : Functor A C
raw F[_∘_] = _∘fr_
-- The identity functor
identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C

333
src/Cat/Category/Monad.agda Normal file
View file

@ -0,0 +1,333 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Category.Monad where
open import Agda.Primitive
open import Data.Product
open import Cubical
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 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
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
private
open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
open Functor using (func* ; func→)
module M = Monoidal ℂ
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
forthRaw : K.RawMonad
Kraw.RR forthRaw = RR
Kraw.ζ forthRaw = ζ
Kraw.rr forthRaw = rr
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
forthIsMonad : K.IsMonad (forthRaw raw)
Kis.isIdentity forthIsMonad = isIdentity
Kis.isNatural forthIsMonad = isNatural
Kis.isDistributive forthIsMonad = isDistributive
forth : M.Monad → K.Monad
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 = {!!}
backRaw : M.RawMonad
Mraw.R backRaw = R
Mraw.ηNat backRaw = ηNat
Mraw.μNat backRaw = μNat
module _ (m : K.Monad) where
open K.Monad m
open M.RawMonad (backRaw m)
module Mis = M.IsMonad
backIsMonad : M.IsMonad (backRaw m)
backIsMonad = {!!}
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)
forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
K.RawMonad.RR (forthRawEq _) = RR
K.RawMonad.ζ (forthRawEq _) = ζ
-- stuck
K.RawMonad.rr (forthRawEq 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)
backRawEq : backRaw (forth m) ≡ M.Monad.raw m
-- stuck
M.RawMonad.R (backRawEq i) = {!!}
M.RawMonad.ηNat (backRawEq i) = {!!}
M.RawMonad.μNat (backRawEq 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
Monoidal≃Kleisli : M.Monad ≃ K.Monad
Monoidal≃Kleisli = forth , eqv

45
src/Cat/Category/Monoid.agda Normal file
View file

@ -0,0 +1,45 @@
module Cat.Category.Monoid where
open import Agda.Primitive
open import Cat.Category
open import Cat.Category.Product
open import Cat.Category.Functor
import Cat.Categories.Cat as Cat
-- TODO: Incorrect!
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)
record RawMonoidalCategory : Set ℓ where
field
category : Category ℓa ℓb
open Category category public
field
{{hasProducts}} : HasProducts category
mempty : Object
-- aka. tensor product, monoidal product.
mappend : Functor (category × category) category
record MonoidalCategory : Set ℓ where
field
raw : RawMonoidalCategory
open RawMonoidalCategory raw public
module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
private
ℓ = ℓa ⊔ ℓb
module MC = MonoidalCategory ℂ
open HasProducts MC.hasProducts
record Monoid : Set ℓ where
field
carrier : MC.Object
mempty : MC.Arrow (carrier × carrier) carrier
mappend : MC.Arrow MC.mempty carrier

101
src/Cat/Category/NaturalTransformation.agda Normal file
View file

@ -0,0 +1,101 @@
-- This module Essentially just provides the data for natural transformations
--
-- This includes:
--
-- The types:
--
-- * Transformation - a family of functors
-- * Natural - naturality condition for transformations
-- * NaturalTransformation - both of the above
--
-- Elements of the above:
--
-- * identityTrans - the identity transformation
-- * identityNatural - naturality for the above
-- * identity - both of the above
--
-- Functions for manipulating the above:
--
-- * A composition operator.
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category.NaturalTransformation where
open import Agda.Primitive
open import Data.Product
open import Cubical
open import Cat.Category
open import Cat.Category.Functor hiding (identity)
module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
(ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙)
module _ (F G : Functor ℂ 𝔻) where
private
module F = Functor F
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 ]
Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
Natural θ
= {A B : Object ℂ}
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
-- TODO: Since naturality is a mere proposition this principle can be
-- simplified.
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
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝟙 𝔻
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
module F = Functor F
F→ = F.func→
module 𝔻 = Category 𝔻
identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
identity F = identityTrans F , identityNatural F
module _ {F G H : Functor ℂ 𝔻} where
private
module F = Functor F
module G = Functor G
module H = Functor H
T[_∘_] : Transformation G H → Transformation F G → Transformation F H
T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]
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 ] ∎
where
open Category 𝔻

53
src/Cat/Category/Pathy.agda
View file

@ -1,53 +0,0 @@
{-# OPTIONS --cubical #-}
module Cat.Category.Pathy where
open import Level
open import Cubical
{-
module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
(P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
pathJ' : (y : A) → (p : x ≡ y) → P y p
pathJ' _ p = transp (λ i → uncurry P (contrSingl p i)) d
pathJprop' : pathJ' _ refl ≡ d
pathJprop' i
= primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d
module _ {ℓ ℓ'} {A : Set ℓ}
(P : (x y : A) → x ≡ y → Set ℓ') (d : (x : A) → P x x refl) where
pathJ'' : (x y : A) → (p : x ≡ y) → P x y p
pathJ'' _ _ p = transp (λ i →
let
P' = uncurry P
q = (contrSingl p i)
in
{!uncurry (uncurry P)!} ) d
-}
module _ {ℓ ℓ'} {A : Set ℓ}
(C : (x y : A) → x ≡ y → Set ℓ')
(c : (x : A) → C x x refl) where
=-ind : (x y : A) → (p : x ≡ y) → C x y p
=-ind x y p = pathJ (C x) (c x) y p
module _ {ℓ ℓ' : Level} {A : Set ℓ} {P : A → Set ℓ} {x y : A} where
private
D : (x y : A) → (x ≡ y) → Set ℓ
D x y p = P x → P y
id : {ℓ : Level} → {A : Set ℓ} → A → A
id x = x
d : (x : A) → D x x refl
d x = id {A = P x}
-- the p refers to the third argument
liftP : x ≡ y → P x → P y
liftP p = =-ind D d x y p
-- lift' : (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , liftP p u)
-- lift' u p = {!!}

35
src/Cat/Category/Properties.agda → src/Cat/Category/Yoneda.agda
View file

@ -1,6 +1,6 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category.Properties where
module Cat.Category.Yoneda where
open import Agda.Primitive
open import Data.Product
@ -8,39 +8,9 @@ open import Cubical
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Categories.Sets
open import Cat.Equality
open Equality.Data.Product
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
open Category ℂ
iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym (proj₁ isIdentity) ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ isIdentity ⟩
g₁ ∎
iso-is-mono : Isomorphism f → Monomorphism {X = X} f
iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
begin
g₀ ≡⟨ sym (proj₂ isIdentity) ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ isIdentity ⟩
g₁ ∎
iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
-- 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)
@ -52,6 +22,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
open import Cat.Category.Exponential
open Functor
𝓢 = Sets ℓ
open Fun (opposite ℂ) 𝓢
private
Catℓ : Category _ _
Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
@ -80,7 +51,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢})
yoneda : Functor ℂ Fun
yoneda = record
{ raw = record
{ func* = prshf