cat/src/Cat/Category.agda

340 lines
12 KiB
Agda
Raw Normal View History

2018-02-25 14:21:38 +00:00
-- | 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.
--
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
2018-02-25 14:21:38 +00:00
-----------------
-- * Utilities --
-----------------
-- | Unique existensials.
∃! : {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-25 14:21:38 +00:00
-----------------
-- * 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
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 _∘_
2018-02-25 14:21:38 +00:00
-- | 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
2018-02-25 14:21:38 +00:00
-- | 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
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
2018-02-23 11:49:41 +00:00
module _ (isIdentity : IsIdentity 𝟙) where
idIso : (A : Object) A A
2018-02-23 11:49:41 +00:00
idIso A = 𝟙 , (𝟙 , isIdentity)
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)
Univalent : Set (a b)
Univalent = {A B : Object} isEquiv (A B) (A B) (id-to-iso A B)
2018-02-25 14:21:38 +00:00
-- | 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
2018-02-25 13:37:28 +00:00
open RawCategory public
open Univalence public
field
2018-02-23 11:43:49 +00:00
isAssociative : IsAssociative
2018-02-23 11:52:14 +00:00
isIdentity : IsIdentity 𝟙
2018-02-23 11:51:44 +00:00
arrowsAreSets : ArrowsAreSets
2018-02-23 11:52:14 +00:00
univalent : Univalent isIdentity
2018-02-25 14:21:38 +00:00
-- Some common lemmas about categories.
2018-02-25 13:44:03 +00:00
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
2018-02-25 14:21:38 +00:00
-- | Propositionality of being a category
--
-- Proves that all projections of `IsCategory` are mere propositions as well as
-- `IsCategory` itself being a mere proposition.
2018-02-20 16:59:48 +00:00
module _ {a b : Level} {C : RawCategory a b} where
open RawCategory C
module _ ( : IsCategory C) where
2018-02-25 13:37:28 +00:00
open IsCategory using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
2018-02-20 16:59:48 +00:00
open import Cubical.NType
open import Cubical.NType.Properties
propIsAssociative : isProp IsAssociative
2018-02-23 11:51:44 +00:00
propIsAssociative x y i = arrowsAreSets _ _ x y i
2018-02-20 16:59:48 +00:00
propIsIdentity : {f : {A} Arrow A A} isProp (IsIdentity f)
propIsIdentity a b i
2018-02-23 11:51:44 +00:00
= arrowsAreSets _ _ (fst a) (fst b) i
, arrowsAreSets _ _ (snd a) (snd b) i
2018-02-20 16:59:48 +00:00
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
2018-02-23 11:51:44 +00:00
h = arrowsAreSets _ _ (fst x) (fst y)
2018-02-20 16:59:48 +00:00
hh : snd x snd y
2018-02-23 11:51:44 +00:00
hh = arrowsAreSets _ _ (snd x) (snd y)
2018-02-20 16:59:48 +00:00
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
2018-02-23 11:49:41 +00:00
g ≡⟨ sym (fst isIdentity)
2018-02-20 16:59:48 +00:00
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') η
2018-02-23 11:49:41 +00:00
𝟙 g' ≡⟨ snd isIdentity
2018-02-20 16:59:48 +00:00
g'
2018-02-23 11:49:41 +00:00
propUnivalent : isProp (Univalent isIdentity)
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-23 11:49:41 +00:00
isIdentity : (λ _ IsIdentity 𝟙) [ X.isIdentity Y.isIdentity ]
isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
2018-02-20 16:33:02 +00:00
done : x y
2018-02-23 09:35:42 +00:00
U : {a : IsIdentity 𝟙}
2018-02-23 11:49:41 +00:00
(λ _ IsIdentity 𝟙) [ X.isIdentity a ]
2018-02-23 09:35:42 +00:00
(b : Univalent a)
Set _
U eqwal bbb =
(λ i Univalent (eqwal i))
[ X.univalent bbb ]
P : (y : IsIdentity 𝟙)
2018-02-23 11:49:41 +00:00
(λ _ IsIdentity 𝟙) [ X.isIdentity y ] Set _
P y eq = (b' : Univalent y) U eq b'
2018-02-23 11:49:41 +00:00
helper : (b' : Univalent X.isIdentity)
(λ _ Univalent X.isIdentity) [ X.univalent b' ]
helper univ = propUnivalent x X.univalent univ
2018-02-23 11:49:41 +00:00
foo = pathJ P helper Y.isIdentity isIdentity
eqUni : U isIdentity 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-23 11:49:41 +00:00
IC.isIdentity (done i) = isIdentity i
2018-02-23 11:51:44 +00:00
IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets 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-25 14:21:38 +00:00
-- | Univalent categories
--
-- Just bundles up the data with witnesses inhabting the propositions.
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-21 12:37:07 +00:00
open IsCategory isCategory public
2018-02-25 14:21:38 +00:00
-- | Syntax for arrows- and composition in a given category.
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
2018-02-25 14:21:38 +00:00
-- | 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
2018-02-25 14:21:38 +00:00
private
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 = {!!}
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 _) = _∘_
-- TODO: Define and use Monad≡
oppositeIsInvolution : opposite (opposite )
Category.raw (oppositeIsInvolution i) = rawInv i
Category.isCategory (oppositeIsInvolution x) = {!!}
open Opposite public renaming (opposite to Opposite)