cat/src/Cat/Category.agda

277 lines
8.8 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 ( ' : Level) : Set (lsuc (' )) where
no-eta-equality
field
Object : Set
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
module Raw = RawCategory
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
field
assoc : IsAssociative
ident : IsIdentity 𝟙
arrowIsSet : {A B : Object} isSet (Arrow A B)
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
IsInverseOf : {A B} (Arrow A B) (Arrow B A) Set b
IsInverseOf = λ f g g f 𝟙 × f g 𝟙
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
Isomorphism : {A B} (f : Arrow A B) Set b
Isomorphism {A} {B} f = Σ[ g Arrow B A ] IsInverseOf f g
inverse : {A B} {f : Arrow A B} Isomorphism f Arrow B A
inverse iso = fst iso
_≅_ : (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)
2018-02-20 13:08:47 +00:00
-- 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 : 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'
module _ {a b : Level} {C : RawCategory a b} { : IsCategory C} where
open IsCategory
open import Cubical.NType
open import Cubical.NType.Properties
propUnivalent : isProp Univalent
propUnivalent a b i = propPi (λ iso propHasLevel ⟨-2⟩) a b i
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
-- Why choose `x`'s `propIsAssociative`?
-- Well, probably it could be pulled out of the record.
{ assoc = x.propIsAssociative x.assoc y.assoc i
2018-02-20 13:08:47 +00:00
; ident = ident' i
; arrowIsSet = x.propArrowIsSet x.arrowIsSet y.arrowIsSet i
; univalent = eqUni i
2018-02-05 09:24:57 +00:00
}
where
module x = IsCategory x
module y = IsCategory y
2018-02-20 13:08:47 +00:00
ident' = x.propIsIdentity x.ident y.ident
ident'' = ident' i
xuni : x.Univalent
xuni = x.univalent
yuni : y.Univalent
yuni = y.univalent
open RawCategory
2018-02-20 13:08:47 +00:00
Pp : (x.ident y.ident) I Set (a b)
Pp eqIdent 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 𝟙)))
( 𝟙
, 𝟙
2018-02-20 13:08:47 +00:00
, ident' i
)
)
2018-02-20 13:08:47 +00:00
T : I Set (a b)
T = Pp {!ident'!}
open Cubical.NType.Properties
test : (λ _ x.Univalent) [ xuni xuni ]
test = refl
t = {!!}
P : (uni : x.Univalent) xuni uni Set (a b)
P = {!!}
2018-02-20 13:08:47 +00:00
-- T i0 ≡ x.Univalent
-- T i1 ≡ y.Univalent
eqUni : T [ xuni yuni ]
2018-02-20 13:08:47 +00:00
eqUni = {!!}
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