cat/src/Cat/Category.agda

368 lines
13 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

-- | 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.
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category where
open import Agda.Primitive
open import Data.Unit.Base
open import Data.Product renaming
( proj₁ to fst
; proj₂ to snd
; ∃! to ∃!≈
)
open import Data.Empty
import Function
open import Cubical
open import Cubical.NType.Properties using ( propIsEquiv )
open import Cat.Wishlist
-----------------
-- * 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
-----------------
-- * 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 _∘_ _>>>_
-- | 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
_>>>_ : {A B C : Object} (Arrow A B) (Arrow B C) Arrow A C
f >>> g = g f
-- | Laws about the data
-- FIXME 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
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₁
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 _ (isIdentity : IsIdentity 𝟙) where
idIso : (A : Object) A A
idIso A = 𝟙 , (𝟙 , isIdentity)
-- 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)
-- | 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
open RawCategory public
open Univalence public
field
isAssociative : IsAssociative
isIdentity : IsIdentity 𝟙
arrowsAreSets : ArrowsAreSets
univalent : Univalent isIdentity
-- Some common lemmas about categories.
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
-- | Propositionality of being a category
--
-- Proves that all projections of `IsCategory` are mere propositions as well as
-- `IsCategory` itself being a mere proposition.
module Propositionality {a b : Level} {C : RawCategory a b} where
open RawCategory C
module _ ( : IsCategory C) where
open IsCategory using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent)
open import Cubical.NType
open import Cubical.NType.Properties
propIsAssociative : isProp IsAssociative
propIsAssociative x y i = arrowsAreSets _ _ x y i
propIsIdentity : {f : {A} Arrow A A} isProp (IsIdentity f)
propIsIdentity a b i
= arrowsAreSets _ _ (fst a) (fst b) i
, arrowsAreSets _ _ (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 = arrowsAreSets _ _ (fst x) (fst y)
hh : snd x snd y
hh = arrowsAreSets _ _ (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 isIdentity)
g 𝟙 ≡⟨ cong (λ φ g φ) (sym ε')
g (f g') ≡⟨ isAssociative
(g f) g' ≡⟨ cong (λ φ φ g') η
𝟙 g' ≡⟨ snd isIdentity
g'
propUnivalent : isProp (Univalent isIdentity)
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.
isIdentity : (λ _ IsIdentity 𝟙) [ X.isIdentity Y.isIdentity ]
isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
done : x y
U : {a : IsIdentity 𝟙}
(λ _ IsIdentity 𝟙) [ X.isIdentity a ]
(b : Univalent a)
Set _
U eqwal bbb =
(λ i Univalent (eqwal i))
[ X.univalent bbb ]
P : (y : IsIdentity 𝟙)
(λ _ IsIdentity 𝟙) [ X.isIdentity y ] Set _
P y eq = (b' : Univalent y) U eq b'
helper : (b' : Univalent X.isIdentity)
(λ _ Univalent X.isIdentity) [ X.univalent b' ]
helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.isIdentity isIdentity
eqUni : U isIdentity Y.univalent
eqUni = foo Y.univalent
IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
IC.isIdentity (done i) = isIdentity i
IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
IC.univalent (done i) = eqUni i
propIsCategory : isProp (IsCategory C)
propIsCategory = done
-- | Univalent categories
--
-- Just bundles up the data with witnesses inhabting the propositions.
record Category (a b : Level) : Set (lsuc (a b)) where
field
raw : RawCategory a b
{{isCategory}} : IsCategory raw
open IsCategory isCategory public
Category≡ : {a b : Level} { 𝔻 : Category a b} Category.raw Category.raw 𝔻 𝔻
Category≡ { = } {𝔻} eq i = record
{ raw = eq i
; isCategory = isCategoryEq i
}
where
open Category
module = Category
isCategoryEq : (λ i IsCategory (eq i)) [ isCategory isCategory 𝔻 ]
isCategoryEq = {!!}
-- | Syntax for arrows- and composition in a given category.
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
_[_∘_] = _∘_
-- | 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
private
module = Category
opRaw : RawCategory a b
RawCategory.Object opRaw = .Object
RawCategory.Arrow opRaw = Function.flip .Arrow
RawCategory.𝟙 opRaw = .𝟙
RawCategory._∘_ opRaw = Function.flip ._∘_
open RawCategory opRaw
open Univalence opRaw
isIdentity : IsIdentity 𝟙
isIdentity = swap .isIdentity
module _ {A B : .Object} where
univalent : isEquiv (A B) (A B)
(id-to-iso (swap .isIdentity) A B)
fst (univalent iso) = flipFiber (fst (.univalent (flipIso iso)))
where
flipIso : A B B .≅ A
flipIso (f , f~ , iso) = f , f~ , swap iso
flipFiber
: fiber (.id-to-iso .isIdentity B A) (flipIso iso)
fiber ( id-to-iso isIdentity A B) iso
flipFiber (eq , eqIso) = sym eq , {!!}
snd (univalent iso) = {!!}
isCategory : IsCategory opRaw
IsCategory.isAssociative isCategory = sym .isAssociative
IsCategory.isIdentity isCategory = isIdentity
IsCategory.arrowsAreSets isCategory = .arrowsAreSets
IsCategory.univalent isCategory = univalent
opposite : Category a b
Category.raw opposite = opRaw
Category.isCategory opposite = isCategory
-- 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 _) = _∘_
oppositeIsInvolution : opposite (opposite )
oppositeIsInvolution = Category≡ rawInv
open Opposite public