cat/src/Cat/Category.agda

253 lines
8.7 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
open import Cubical
2018-02-16 10:36:44 +00:00
open import Cubical.NType.Properties using ( propIsEquiv )
2017-11-10 15:00:00 +00:00
2018-02-19 10:25:16 +00:00
open import Cat.Wishlist
∃! : {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
record RawCategory (a b : Level) : Set (lsuc (a b)) where
no-eta-equality
field
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
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
IsIdentity : ({A : Object} Arrow A A) Set (a b)
IsIdentity id = {A B : Object} {f : Arrow A B}
f id f × id f f
2018-02-23 09:35:42 +00:00
ArrowsAreSets : Set (a b)
ArrowsAreSets = {A B : Object} isSet (Arrow A B)
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 ] IsInverseOf f g
_≅_ : (A B : Object) Set b
_≅_ A B = Σ[ f Arrow A B ] (Isomorphism f)
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₁
Monomorphism : {X : Object} (f : Arrow A B) Set b
Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) f g₀ f g₁ g₀ g₁
2018-02-21 11:59:31 +00:00
IsInitial : Object Set (a b)
IsInitial I = {X : Object} isContr (Arrow I X)
IsTerminal : Object Set (a b)
2018-02-20 17:15:07 +00:00
IsTerminal T = {X : Object} isContr (Arrow X T)
2018-02-21 11:59:31 +00:00
Initial : Set (a b)
Initial = Σ Object IsInitial
Terminal : Set (a b)
2018-02-21 11:59:31 +00:00
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)
2018-02-21 12:37:07 +00:00
-- 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
2018-02-23 11:43:49 +00:00
isAssociative : IsAssociative
ident : IsIdentity 𝟙
2018-02-23 09:35:42 +00:00
arrowIsSet : ArrowsAreSets
univalent : Univalent ident
2018-02-20 16:59:48 +00:00
-- `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 ε')
2018-02-23 11:43:49 +00:00
g (f g') ≡⟨ isAssociative
2018-02-20 16:59:48 +00:00
(g f) g' ≡⟨ cong (λ φ φ g') η
𝟙 g' ≡⟨ snd ident
g'
propUnivalent : isProp (Univalent ident)
2018-02-20 16:59:48 +00:00
propUnivalent a b i = propPi (λ iso propHasLevel ⟨-2⟩) a b i
2018-02-20 15:42:56 +00:00
private
2018-02-20 16:59:48 +00:00
module _ (x y : IsCategory C) where
2018-02-20 15:42:56 +00:00
module IC = IsCategory
module X = IsCategory x
module Y = IsCategory y
open Univalence C
2018-02-20 16:59:48 +00:00
-- 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.
2018-02-20 16:33:02 +00:00
ident : (λ _ IsIdentity 𝟙) [ X.ident Y.ident ]
2018-02-20 16:59:48 +00:00
ident = propIsIdentity x X.ident Y.ident
2018-02-20 16:33:02 +00:00
done : x y
2018-02-23 09:35:42 +00:00
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
2018-02-20 16:33:02 +00:00
eqUni : U ident Y.univalent
eqUni = foo Y.univalent
2018-02-23 11:43:49 +00:00
IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
2018-02-20 15:42:56 +00:00
IC.ident (done i) = ident i
2018-02-20 16:59:48 +00:00
IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
2018-02-20 15:42:56 +00:00
IC.univalent (done i) = eqUni i
2018-02-20 16:59:48 +00:00
propIsCategory : isProp (IsCategory C)
2018-02-20 15:42:56 +00:00
propIsCategory = done
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
2018-02-20 15:25:49 +00:00
open RawCategory raw public
2018-02-21 12:37:07 +00:00
open IsCategory isCategory public
2018-02-21 12:37:07 +00:00
module _ {a b : Level} ( : Category a b) where
open Category
_[_,_] : (A : Object) (B : Object) Set b
2018-02-20 15:25:49 +00:00
_[_,_] = Arrow
2017-11-10 15:00:00 +00:00
2018-02-20 15:25:49 +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 _∘_
OpIsCategory : IsCategory OpRaw
2018-02-23 11:43:49 +00:00
IsCategory.isAssociative OpIsCategory = sym isAssociative
2018-02-05 13:47:15 +00:00
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)
2018-02-23 11:43:49 +00:00
isAssociative (rawIsCat i) = IsCat.isAssociative
2018-02-05 13:47:15 +00:00
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