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-21 14:06:24 +01:00
parent b8994b8f4a 7ed99a6bb4
commit 5b2681392c
12 changed files with 368 additions and 240 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
BACKLOG.md Normal file
View file

@ -0,0 +1,6 @@
Backlog
=======
Prove univalence for various categories
Prove postulates in `Cat.Wishlist`

17
CHANGELOG.md Normal file
View file

@ -0,0 +1,17 @@
Changelog
=========
Version 1.1.0
-------------
In this version categories have been refactored - there's now a notion of a raw
category, and a proper category which has the data (raw category) as well as
the laws.
Furthermore the type of arrows must be homotopy sets and they must satisfy univalence.
I've made a module `Cat.Wishlist` where I just postulate things that I hope to
implement upstream in `cubical`.
I have proven that `IsCategory` is a mere proposition.
I've also updated the category of sets to adhere to this new definition.

22
README.md
View file

@ -1,17 +1,29 @@
Description
===========
This project includes code as well as my masters thesis (currently just
consisting of the proposal for the thesis).
This project aims to formalize some parts of category theory using cubical agda
— an extension to agda permitting univalence. To learn more about this
[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
This project draws a lot of inspiration from [the
HoTT-book](https://homotopytypetheory.org/book/).
Installation
============
You probably need a very recent version of the Agda compiler. At the time
of writing the solution has been tested with Agda version 2.6.0-5d84754.
Dependencies
------------
To succesfully compile the following is needed:
* Agda version >= `707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`.
* [Agda Standard Library](https://github.com/agda/agda-stdlib)
* [Cubical](https://github.com/Saizan/cubical-demo/)
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.
I've used git submodules to manage dependencies. Unfortunately Agda does not
allow specifying libraries to be used only as local dependencies.
allow specifying libraries to be used only as local dependencies. So the
submodules are mostly used for documentation.
You can let Agda know about these libraries by appending them to your global
libraries file like so: (NB!: There is a good reason this is not in a

2
libs/agda-stdlib

@ -1 +1 @@
Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68
Subproject commit 87d28d7d753f73abd20665d7bbb88f9d72ed88aa

2
libs/cubical

@ -1 +1 @@
Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151
Subproject commit 9bfbacbb30d4673332566f6e4a58fd04e3904106

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

@ -8,55 +8,65 @@ open import Data.Product
open import Cat.Category
open IsCategory
open Category
-- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
-- emptyPath : {a : A} → Path a a
-- concatenate : {a b c : A} → Path a b → Path b c → Path a b
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
module ℂ = Category ℂ
-- import Data.List
-- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
-- P = {!Data.List.List ?!}
-- Generalized paths:
-- data P {ℓ : Level} {A : Set ℓ} (R : A → A → Set ℓ) : (a b : A) → Set ℓ where
-- e : {a : A} → P R a a
-- c : {a b c : A} → R a b → P R b c → P R a c
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
-- Path's are like lists with directions.
-- This implementation is specialized to categories.
data Path : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') where
empty : {A : Object ℂ} → Path A A
cons : ∀ {A B C} → ℂ [ B , C ] → Path A B → Path A C
concatenate : ∀ {A B C : Object ℂ} → Path B C → Path A B → Path A C
concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c
concatenate empty p = p
concatenate (cons x q) p = cons x (concatenate q p)
_++_ = concatenate
singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B
singleton f = cons f empty
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
module ℂ = Category ℂ
open Category ℂ
private
module _ {A B C D : Object ℂ} where
p-assoc : {r : Path A B} {q : Path B C} {p : Path C D} → concatenate p (concatenate q r) ≡ concatenate (concatenate p q) r
p-assoc {r} {q} {p} = {!!}
module _ {A B : Object ℂ} {p : Path A B} where
-- postulate
-- ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
-- ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
module _ {A B : Object ℂ} where
isSet : Cubical.isSet (Path A B)
isSet = {!!}
p-assoc : {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-assoc {r = r} {q} {empty} = refl
p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
cons x p ++ (q ++ r) ≡⟨ cong (cons x) lem ⟩
cons x ((p ++ q) ++ r) ≡⟨⟩
(cons x p ++ q) ++ r ∎
where
lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
lem = p-assoc {r = r} {q} {p}
ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
ident-r {p = empty} = refl
ident-r {p = cons x p} = cong (cons x) ident-r
ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p
ident-l = refl
module _ {A B : Object} where
isSet : Cubical.isSet (Path Arrow A B)
isSet a b p q = {!!}
RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
RawFree = record
{ Object = Object ℂ
; Arrow = Path
; 𝟙 = λ {o} → {!lift 𝟙!}
; _∘_ = λ {a b c} → {!concatenate {a} {b} {c}!}
{ Object = Object
; Arrow = Path Arrow
; 𝟙 = empty
; _∘_ = concatenate
}
RawIsCategoryFree : IsCategory RawFree
RawIsCategoryFree = record
{ assoc = {!p-assoc!}
; ident = {!ident-r , ident-l!}
{ assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
; ident = ident-r , ident-l
; arrowIsSet = {!!}
; univalent = {!!}
}

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

@ -9,6 +9,7 @@ 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
@ -20,7 +21,7 @@ open import Cat.Equality
open Equality.Data.Product
module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
open Category hiding ( _∘_ ; Arrow )
open Category using (Object ; 𝟙)
open Functor
module _ (F G : Functor ℂ 𝔻) where
@ -69,7 +70,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
where
module F = Functor F
F→ = F.func→
module 𝔻 = IsCategory (isCategory 𝔻)
module 𝔻 = Category 𝔻
identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
identityNat F = identityTrans F , identityNatural F
@ -94,13 +95,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎
where
open IsCategory (isCategory 𝔻)
open Category 𝔻
NatComp = _:⊕:_
private
module _ {F G : Functor ℂ 𝔻} where
module 𝔻 = IsCategory (isCategory 𝔻)
module 𝔻 = Category 𝔻
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j
@ -125,18 +126,37 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
θNat = proj₂ θ'
ηNat = proj₂ η'
ζNat = proj₂ ζ'
L : NaturalTransformation A D
L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {D}
:assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
:assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
:assoc: : L ≡ R
:assoc: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → assoc))
where
open IsCategory (isCategory 𝔻)
open Category 𝔻
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
private
allNatural = naturalIsProp {F = A} {B}
f' = proj₁ f
module 𝔻Data = Category 𝔻
eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
eq-r C = begin
𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
𝔻 [ f' C ∘ 𝔻Data.𝟙 ] ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
f' C ∎
eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
eq-l C = proj₂ (𝔻.ident {A} {B})
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
ident-r = {!!}
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
ident-l = {!!}
ident-l = lemSig allNatural _ _ (funExt eq-l)
:ident:
: (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
× (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
@ -161,7 +181,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
}
Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
raw Fun = RawFun
Category.raw Fun = RawFun
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open import Cat.Categories.Sets

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

@ -9,55 +9,92 @@ import Function
open import Cat.Category
open import Cat.Category.Functor
open import Cat.Category.Product
open Category
module _ {ℓ : Level} where
SetsRaw : RawCategory (lsuc ℓ) ℓ
RawCategory.Object SetsRaw = Set ℓ
RawCategory.Arrow SetsRaw = λ T U → T → U
RawCategory.𝟙 SetsRaw = Function.id
RawCategory._∘_ SetsRaw = Function._∘′_
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 = Cubical.Universe.0-Set
Arrow SetsRaw (T , _) (U , _) = T → U
𝟙 SetsRaw = Function.id
_∘_ SetsRaw = Function._∘′_
SetsIsCategory : IsCategory SetsRaw
assoc SetsIsCategory = refl
proj₁ (ident SetsIsCategory) = funExt λ _ → refl
proj₂ (ident SetsIsCategory) = funExt λ _ → refl
arrowIsSet SetsIsCategory = {!!}
arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
univalent SetsIsCategory = {!!}
Sets : Category (lsuc ℓ) ℓ
raw Sets = SetsRaw
isCategory Sets = SetsIsCategory
𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
Category.raw 𝓢𝓮𝓽 = SetsRaw
Category.isCategory 𝓢𝓮𝓽 = SetsIsCategory
Sets = 𝓢𝓮𝓽
module _ {ℓ : Level} where
private
𝓢 = 𝓢𝓮𝓽 ℓ
open Category 𝓢
open import Cubical.Sigma
module _ (0A 0B : Object) where
private
A : Set ℓ
A = proj₁ 0A
sA : isSet A
sA = proj₂ 0A
B : Set ℓ
B = proj₁ 0B
sB : isSet B
sB = proj₂ 0B
0A×0B : Object
0A×0B = (A × B) , sigPresSet sA λ _ → sB
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
_&&&_ : (X → A × B)
_&&&_ x = f x , g x
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
module _ {0X : Object} where
X = proj₁ 0X
module _ (f : X → A ) (g : X → B) where
lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
proj₁ lem = refl
proj₂ lem = refl
instance
isProduct : {A B : Object Sets} → IsProduct Sets {A} {B} proj₁ proj₂
isProduct f g = f &&& g , lem f g
isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
product : (A B : Object Sets) → Product {ℂ = Sets} A B
product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
product : Product {ℂ = 𝓢} 0A 0B
product = record
{ obj = 0A×0B
; proj₁ = Data.Product.proj₁
; proj₂ = Data.Product.proj₂
; isProduct = λ { {X} → isProduct {X = X}}
}
instance
SetsHasProducts : HasProducts Sets
SetsHasProducts : HasProducts 𝓢
SetsHasProducts = record { product = product }
module _ {ℓa ℓb : Level} where
module _ (ℂ : Category ℓa ℓb) where
-- Covariant Presheaf
Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
Representable : Set (ℓa ⊔ lsuc ℓb)
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
-- Contravariant Presheaf
Presheaf : Set (ℓa ⊔ lsuc ℓb)
Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
-- The "co-yoneda" embedding.
representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
{ raw = record
{ func* = λ B → ℂ [ A , B ]
{ func* = λ B → ℂ [ A , B ] , arrowIsSet
; func→ = ℂ [_∘_]
}
; isFunctor = record
@ -66,17 +103,13 @@ representable {ℂ = ℂ} A = record
}
}
where
open IsCategory (isCategory ℂ)
-- Contravariant Presheaf
Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
open Category ℂ
-- Alternate name: `yoneda`
presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ raw = record
{ func* = λ A → ℂ [ A , B ]
{ func* = λ A → ℂ [ A , B ] , arrowIsSet
; func→ = λ f g → ℂ [ g ∘ f ]
}
; isFunctor = record
@ -85,4 +118,4 @@ presheaf {ℂ = ℂ} B = record
}
}
where
open IsCategory (isCategory ℂ)
open Category ℂ

254
src/Cat/Category.agda
View file

@ -14,6 +14,8 @@ import Function
open import Cubical
open import Cubical.NType.Properties using ( propIsEquiv )
open import Cat.Wishlist
∃! : ∀ {a b} {A : Set a}
→ (A → Set b) → Set (a ⊔ b)
∃! = ∃!≈ _≡_
@ -23,64 +25,39 @@ open import Cubical.NType.Properties using ( propIsEquiv )
syntax ∃!-syntax (λ x → B) = ∃![ x ] B
-- This follows from [HoTT-book: §7.1.10]
-- Andrea says the proof is in `cubical` but I can't find it.
postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-- adding no-eta-equality can speed up type-checking.
-- ONLY IF you define your categories with copatterns though.
record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
no-eta-equality
field
-- Need something like:
-- Object : Σ (Set ℓ) isGroupoid
Object : Set ℓ
-- And:
-- Arrow : Object → Object → Σ (Set ℓ') isSet
Arrow : Object → Object → Set ℓ'
𝟙 : {o : Object} → Arrow o o
Object : Set ℓa
Arrow : Object → Object → Set ℓb
𝟙 : {A : Object} → Arrow A A
_∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
infixl 10 _∘_
domain : { a b : Object } → Arrow a b → Object
domain {a = a} _ = a
codomain : { a b : Object } → Arrow a b → Object
codomain {b = b} _ = b
-- Thierry: All projections must be `isProp`'s
-- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
-- arrows of a category form a set (arrow-is-set), and there is an
-- equivalence between the equality of objects and isomorphisms
-- (univalent).
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
open RawCategory ℂ
module Raw = RawCategory ℂ
field
assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
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
ident : {A B : Object} {f : Arrow A B}
→ f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
IsIdentity id = {A B : Object} {f : Arrow A B}
→ f ∘ id ≡ f × id ∘ f ≡ f
IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
_≅_ : (A B : Object) → Set ℓb
_≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
idIso : (A : Object) → A ≅ A
idIso A = 𝟙 , (𝟙 , ident)
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)
field
univalent : Univalent
module _ {A B : Object} where
Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
@ -88,69 +65,137 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
-- TODO, provable by using arrow-is-set and that isProp (isEquiv _ _ _)
-- This lemma will be useful to prove the equality of two categories.
IsCategory-is-prop : isProp (IsCategory ℂ)
IsCategory-is-prop x y i = record
-- Why choose `x`'s `arrowIsSet`?
{ assoc = x.arrowIsSet _ _ x.assoc y.assoc i
; ident =
( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
, x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
)
; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
; univalent = {!!}
}
where
module x = IsCategory x
module y = IsCategory y
xuni : x.Univalent
xuni = x.univalent
yuni : y.Univalent
yuni = y.univalent
open RawCategory ℂ
T : I → Set (ℓa ⊔ ℓb)
T i = {A B : Object} →
isEquiv (A ≡ B) (A x.≅ B)
(λ A≡B →
transp
(λ j →
Σ-syntax (Arrow A (A≡B j))
(λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
( 𝟙
, 𝟙
, x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
, x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
)
)
eqUni : T [ xuni ≡ yuni ]
eqUni = {!!}
IsInitial : Object → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Object} → isContr (Arrow I X)
IsTerminal : Object → Set (ℓa ⊔ ℓb)
IsTerminal T = {X : Object} → isContr (Arrow X T)
Initial : Set (ℓa ⊔ ℓb)
Initial = Σ Object IsInitial
Terminal : Set (ℓa ⊔ ℓb)
Terminal = Σ Object IsTerminal
-- Univalence is indexed by a raw category as well as an identity proof.
module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
open RawCategory ℂ
module _ (ident : IsIdentity 𝟙) where
idIso : (A : Object) → A ≅ A
idIso A = 𝟙 , (𝟙 , ident)
-- Lemma 9.1.4 in [HoTT]
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)
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
open RawCategory ℂ
open Univalence ℂ public
field
assoc : IsAssociative
ident : IsIdentity 𝟙
arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
univalent : Univalent ident
-- `IsCategory` is a mere proposition.
module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
open RawCategory C
module _ (ℂ : IsCategory C) where
open IsCategory ℂ
open import Cubical.NType
open import Cubical.NType.Properties
propIsAssociative : isProp IsAssociative
propIsAssociative x y i = arrowIsSet _ _ x y i
propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
propIsIdentity a b i
= arrowIsSet _ _ (fst a) (fst b) i
, arrowIsSet _ _ (snd a) (snd b) i
propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
propArrowIsSet a b i = isSetIsProp a b i
propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
propIsInverseOf x y = λ i →
let
h : fst x ≡ fst y
h = arrowIsSet _ _ (fst x) (fst y)
hh : snd x ≡ snd y
hh = arrowIsSet _ _ (snd x) (snd y)
in h i , hh i
module _ {A B : Object} {f : Arrow A B} where
isoIsProp : isProp (Isomorphism f)
isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
lemSig (λ g → propIsInverseOf) a a' geq
where
open Cubical.NType.Properties
geq : g ≡ g'
geq = begin
g ≡⟨ sym (fst ident) ⟩
g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ assoc ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
𝟙 ∘ g' ≡⟨ snd ident ⟩
g' ∎
propUnivalent : isProp (Univalent ident)
propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
private
module _ (x y : IsCategory C) where
module IC = IsCategory
module X = IsCategory x
module Y = IsCategory y
open Univalence C
-- 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.
ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
ident = propIsIdentity x X.ident Y.ident
done : x ≡ y
U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
P : (y : IsIdentity 𝟙)
→ (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
P y eq = ∀ (b' : Univalent y) → U eq b'
helper : ∀ (b' : Univalent X.ident)
→ (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.ident ident
eqUni : U ident Y.univalent
eqUni = foo Y.univalent
IC.assoc (done i) = propIsAssociative x X.assoc Y.assoc i
IC.ident (done i) = ident i
IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
IC.univalent (done i) = eqUni i
propIsCategory : isProp (IsCategory C)
propIsCategory = done
record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
field
raw : RawCategory ℓa ℓb
{{isCategory}} : IsCategory raw
private
module ℂ = RawCategory raw
Object : Set ℓa
Object = ℂ.Object
Arrow = ℂ.Arrow
𝟙 = ℂ.𝟙
_∘_ = ℂ._∘_
open RawCategory raw public
open IsCategory isCategory public
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Category ℂ
_[_,_] : (A : Object) → (B : Object) → Set ℓb
_[_,_] = ℂ.Arrow
_[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
_[_∘_] = ℂ._∘_
_[_,_] = Arrow
_[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
_[_∘_] = _∘_
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
private
@ -162,8 +207,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
RawCategory.𝟙 OpRaw = 𝟙
RawCategory._∘_ OpRaw = Function.flip _∘_
open IsCategory isCategory
OpIsCategory : IsCategory OpRaw
IsCategory.assoc OpIsCategory = sym assoc
IsCategory.ident OpIsCategory = swap ident
@ -199,20 +242,3 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
raw (Opposite-is-involution i) = rawOp i
isCategory (Opposite-is-involution i) = rawIsCat i
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Category
unique = isContr
IsInitial : Object ℂ → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ])
IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb)
-- ∃![ ? ] ?
IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ])
Initial : Set (ℓa ⊔ ℓb)
Initial = Σ (Object ℂ) IsInitial
Terminal : Set (ℓa ⊔ ℓb)
Terminal = Σ (Object ℂ) IsTerminal

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

@ -47,7 +47,6 @@ module _ {ℓc ℓc' ℓd ℓd'}
open IsFunctor
open Functor
-- TODO: Is `IsFunctor` a proposition?
module _
{ℓa ℓb : Level}
{ℂ 𝔻 : Category ℓa ℓb}
@ -56,11 +55,8 @@ module _
private
module 𝔻 = IsCategory (isCategory 𝔻)
-- isProp : Set ℓ
-- isProp = (x y : A) → x ≡ y
IsFunctorIsProp : isProp (IsFunctor _ _ F)
IsFunctorIsProp isF0 isF1 i = record
propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record
{ ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
}
@ -81,7 +77,7 @@ module _
IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
(\ F → IsFunctorIsProp {F = F}) (\ i → F i)
(\ F → propIsFunctor {F = F}) (\ i → F i)
where
open import Cubical.NType.Properties using (lemPropF)

1
src/Cat/Category/Properties.agda
View file

@ -14,7 +14,6 @@ open Equality.Data.Product
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
open Category ℂ
open IsCategory (isCategory)
iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin

9
src/Cat/Wishlist.agda
View file

@ -1,6 +1,15 @@
module Cat.Wishlist where
open import Level
open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
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⟩))