cat/src/Cat/Category.agda

203 lines
6.5 KiB
Agda
Raw Normal View History

2018-02-02 14:33:54 +00:00
{-# OPTIONS --allow-unsolved-metas --cubical #-}
2017-11-10 15:00:00 +00:00
module Cat.Category where
2017-11-10 15:00:00 +00:00
open import Agda.Primitive
open import Data.Unit.Base
open import Data.Product renaming
( proj₁ to fst
; proj₂ to snd
; ∃! to ∃!≈
)
2017-11-15 21:56:04 +00:00
open import Data.Empty
import Function
2018-02-06 09:34:43 +00:00
open import Cubical hiding (isSet)
2018-02-05 09:24:57 +00:00
open import Cubical.GradLemma using ( propIsEquiv )
2017-11-10 15:00:00 +00:00
∃! : {a b} {A : Set a}
(A Set b) Set (a b)
∃! = ∃!≈ _≡_
∃!-syntax : {a b} {A : Set a} (A Set b) Set (a b)
∃!-syntax =
syntax ∃!-syntax (λ x B) = ∃![ x ] B
2018-02-06 09:34:43 +00:00
IsSet : { : Level} (A : Set ) Set
IsSet A = {x y : A} (p q : x y) p q
record RawCategory ( ' : Level) : Set (lsuc (' )) where
-- adding no-eta-equality can speed up type-checking.
-- ONLY IF you define your categories with copatterns though.
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
_∘_ : {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
2018-02-02 14:33:54 +00:00
-- 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
-- (Object : Set )
-- (Arrow : Object → Object → Set ')
-- (𝟙 : {o : Object} → Arrow o o)
-- (_∘_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c)
field
assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
2018-02-02 14:33:54 +00:00
h (g f) (h g) f
ident : {A B : Object} {f : Arrow A B}
2018-02-02 14:33:54 +00:00
f 𝟙 f × 𝟙 f f
2018-02-06 09:34:43 +00:00
arrowIsSet : {A B : Object} IsSet (Arrow A B)
Isomorphism : {A B} (f : Arrow A B) Set b
2018-02-02 14:33:54 +00:00
Isomorphism {A} {B} f = Σ[ g Arrow B A ] g f 𝟙 × 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.
2018-02-05 15:35:33 +00:00
Univalent : Set (a b)
Univalent = {A B : Object} isEquiv (A B) (A B) (id-to-iso A B)
field
2018-02-05 15:35:33 +00:00
univalent : Univalent
2018-02-02 14:33:54 +00:00
module _ {A B : Object} where
Epimorphism : {X : Object } (f : Arrow A B) Set b
2018-02-02 14:33:54 +00:00
Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) g₀ f g₁ f g₀ g₁
Monomorphism : {X : Object} (f : Arrow A B) Set b
2018-02-02 14:33:54 +00:00
Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) f g₀ f g₁ g₀ g₁
module _ {a} {b} { : RawCategory a b} where
2018-02-05 09:24:57 +00:00
-- 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 )
2018-02-05 09:24:57 +00:00
IsCategory-is-prop x y i = record
2018-02-06 09:34:43 +00:00
{ assoc = x.arrowIsSet x.assoc y.assoc i
2018-02-05 09:24:57 +00:00
; ident =
2018-02-06 09:34:43 +00:00
( x.arrowIsSet (fst x.ident) (fst y.ident) i
, x.arrowIsSet (snd x.ident) (snd y.ident) i
2018-02-05 09:24:57 +00:00
)
2018-02-06 09:34:43 +00:00
; arrowIsSet = λ p q
2018-02-05 09:24:57 +00:00
let
2018-02-06 09:34:43 +00:00
golden : x.arrowIsSet p q y.arrowIsSet p q
golden = {!!}
2018-02-05 09:24:57 +00:00
in
golden i
; univalent = λ y₁ {!!}
}
where
module x = IsCategory x
module y = IsCategory y
2018-02-05 13:47:15 +00:00
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
𝟙 = .𝟙
_∘_ = ._∘_
_[_,_] : (A : Object) (B : Object) Set b
_[_,_] = .Arrow
2017-11-10 15:00:00 +00:00
_[_∘_] : {A B C : Object} (g : .Arrow B C) (f : .Arrow A B) .Arrow A C
_[_∘_] = ._∘_
2017-11-10 15:00:00 +00:00
module _ {a b : Level} ( : Category a b) where
private
open Category
2018-02-05 13:47:15 +00:00
OpRaw : RawCategory a b
2018-02-05 13:47:15 +00:00
RawCategory.Object OpRaw = Object
RawCategory.Arrow OpRaw = Function.flip Arrow
RawCategory.𝟙 OpRaw = 𝟙
RawCategory._∘_ OpRaw = Function.flip _∘_
open IsCategory isCategory
2018-02-05 13:47:15 +00:00
OpIsCategory : IsCategory OpRaw
2018-02-05 13:47:15 +00:00
IsCategory.assoc OpIsCategory = sym assoc
IsCategory.ident OpIsCategory = swap ident
2018-02-06 09:34:43 +00:00
IsCategory.arrowIsSet OpIsCategory = arrowIsSet
2018-02-05 13:47:15 +00:00
IsCategory.univalent OpIsCategory = {!!}
Opposite : Category a b
2018-02-05 13:47:15 +00:00
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 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)
assoc (rawIsCat i) = IsCat.assoc
ident (rawIsCat i) = IsCat.ident
2018-02-06 09:34:43 +00:00
arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
2018-02-05 13:47:15 +00:00
univalent (rawIsCat i) = IsCat.univalent
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
2018-02-05 13:47:15 +00:00
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