fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Rename identity in category to ascii-name

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-03 11:36:09 +02:00
parent 41b442c0d8
commit 1c6d9ad2b5
16 changed files with 221 additions and 198 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/Cat/Categories/Cat.agda
View file

@ -15,10 +15,10 @@ open import Cat.Categories.Fun
-- The category of categories
module _ (ℓ ℓ' : Level) where
RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
RawCategory.Object RawCat = Category ℓ ℓ'
RawCategory.Arrow RawCat = Functor
RawCategory.𝟙 RawCat = Functors.identity
RawCategory._∘_ RawCat = F[_∘_]
RawCategory.Object RawCat = Category ℓ ℓ'
RawCategory.Arrow RawCat = Functor
RawCategory.identity RawCat = Functors.identity
RawCategory._∘_ RawCat = F[_∘_]
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
@ -48,8 +48,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
Obj = ℂ.Object × 𝔻.Object
Arr : Obj → Obj → Set ℓ'
Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
𝟙 : {o : Obj} → Arr o o
𝟙 = ℂ.𝟙 , 𝔻.𝟙
identity : {o : Obj} → Arr o o
identity = ℂ.identity , 𝔻.identity
_∘_ :
{a b c : Obj} →
Arr b c →
@ -58,16 +58,16 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
_∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
rawProduct : RawCategory ℓ ℓ'
RawCategory.Object rawProduct = Obj
RawCategory.Arrow rawProduct = Arr
RawCategory.𝟙 rawProduct = 𝟙
RawCategory._∘_ rawProduct = _∘_
RawCategory.Object rawProduct = Obj
RawCategory.Arrow rawProduct = Arr
RawCategory.identity rawProduct = identity
RawCategory._∘_ rawProduct = _∘_
open RawCategory rawProduct
arrowsAreSets : ArrowsAreSets
arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets}
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity
= Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
, Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
@ -202,14 +202,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
open Σ c renaming (proj₁ to F ; proj₂ to C)
ident : fmap {c} {c} (identityNT F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙
ident : fmap {c} {c} (identityNT F , ℂ.identity {A = snd c}) ≡ 𝔻.identity
ident = begin
fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩
fmap {c} {c} (idN F , ℂ.𝟙) ≡⟨⟩
𝔻 [ identityTrans F C ∘ F.fmap ℂ.𝟙 ] ≡⟨⟩
𝔻 [ 𝔻.𝟙 ∘ F.fmap ℂ.𝟙 ] ≡⟨ 𝔻.leftIdentity ⟩
F.fmap ℂ.𝟙 ≡⟨ F.isIdentity ⟩
𝔻.𝟙 ∎
fmap {c} {c} (Category.identity (object ⊗ ℂ) {c}) ≡⟨⟩
fmap {c} {c} (idN F , ℂ.identity) ≡⟨⟩
𝔻 [ identityTrans F C ∘ F.fmap ℂ.identity ] ≡⟨⟩
𝔻 [ 𝔻.identity ∘ F.fmap ℂ.identity ] ≡⟨ 𝔻.leftIdentity ⟩
F.fmap ℂ.identity ≡⟨ F.isIdentity ⟩
𝔻.identity ∎
where
module F = Functor F
@ -278,16 +278,16 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
transpose : Functor 𝔸 object
eq : F[ eval ∘ (parallelProduct transpose (Functors.identity {ℂ = ℂ})) ] ≡ F
-- eq : F[ :eval: ∘ {!!} ] ≡ F
-- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
-- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (identity Catℓ {o = ℂ})) ] ≡ F
-- eq' : (Catℓ [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
-- (𝟙 Catℓ)
-- (identity Catℓ)
-- ])
-- ≡ F
-- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
-- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
-- :eval: ∘ (parallelProduct F~ (identity Catℓ {o = ℂ}))] ≡ F) catTranspose =
-- transpose , eq
-- We don't care about filling out the holes below since they are anyways hidden

2
src/Cat/Categories/Cube.agda
View file

@ -67,7 +67,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
Raw.Object Rawℂ = FiniteDecidableSubset
Raw.Arrow Rawℂ = Hom
Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
Raw._∘_ Rawℂ = {!!}
postulate IsCategoryℂ : IsCategory Rawℂ

12
src/Cat/Categories/Fam.agda
View file

@ -11,9 +11,9 @@ module _ (ℓa ℓb : Level) where
Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb)
Arr : Object → Object → Set (ℓa ⊔ ℓb)
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
𝟙 : {A : Object} → Arr A A
proj₁ 𝟙 = λ x → x
proj₂ 𝟙 = λ b → b
identity : {A : Object} → Arr A A
proj₁ identity = λ x → x
proj₂ identity = λ b → b
_∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
(g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
@ -21,16 +21,16 @@ module _ (ℓa ℓb : Level) where
RawFam = record
{ Object = Object
; Arrow = Arr
; 𝟙 = λ { {A} → 𝟙 {A = A}}
; identity = λ { {A} → identity {A = A}}
; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
}
open RawCategory RawFam hiding (Object ; 𝟙)
open RawCategory RawFam hiding (Object ; identity)
isAssociative : IsAssociative
isAssociative = Σ≡ refl refl
isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
isIdentity : IsIdentity λ { {A} → identity {A} }
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
open import Cubical.NType.Properties

10
src/Cat/Categories/Free.agda
View file

@ -27,10 +27,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
module ℂ = Category ℂ
RawFree : RawCategory ℓa (ℓa ⊔ ℓb)
RawCategory.Object RawFree = ℂ.Object
RawCategory.Arrow RawFree = Path ℂ.Arrow
RawCategory.𝟙 RawFree = empty
RawCategory._∘_ RawFree = concatenate
RawCategory.Object RawFree = ℂ.Object
RawCategory.Arrow RawFree = Path ℂ.Arrow
RawCategory.identity RawFree = empty
RawCategory._∘_ RawFree = concatenate
open RawCategory RawFree
@ -52,7 +52,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
ident-l : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate empty p ≡ p
ident-l = refl
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity = ident-l , ident-r
open Univalence isIdentity

109
src/Cat/Categories/Fun.agda
View file

@ -1,28 +1,28 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-}
{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
module Cat.Categories.Fun where
open import Cat.Prelude
open import Cat.Category
open import Cat.Category.Functor
import Cat.Category.NaturalTransformation
as NaturalTransformation
module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
import Cat.Category.NaturalTransformation ℂ 𝔻
as NaturalTransformation
open NaturalTransformation public hiding (module Properties)
open NaturalTransformation.Properties
open NaturalTransformation ℂ 𝔻 public hiding (module Properties)
open NaturalTransformation.Properties ℂ 𝔻
private
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
-- Functor categories. Objects are functors, arrows are natural transformations.
raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
RawCategory.Object raw = Functor ℂ 𝔻
RawCategory.Arrow raw = NaturalTransformation
RawCategory.𝟙 raw {F} = identity F
RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
RawCategory.Object raw = Functor ℂ 𝔻
RawCategory.Arrow raw = NaturalTransformation
RawCategory.identity raw {F} = identity F
RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
open RawCategory raw
open RawCategory raw hiding (identity)
open Univalence (λ {A} {B} {f} → isIdentity {F = A} {B} {f})
module _ (F : Functor ℂ 𝔻) where
@ -32,7 +32,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
open Σ center renaming (proj₂ to isoF)
module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where
open Σ cG renaming (proj₁ to G ; proj₂ to isoG)
open Σ cG renaming (proj₁ to G ; proj₂ to isoG)
module G = Functor G
open Σ isoG renaming (proj₁ to θNT ; proj₂ to invθNT)
open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv)
@ -46,10 +46,10 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
-- g = T[ η ∘ θ ] {!!}
ntF : NaturalTransformation F F
ntF = 𝟙 {A = F}
ntF = identity F
ntG : NaturalTransformation G G
ntG = 𝟙 {A = G}
ntG = identity G
idFunctor = Functors.identity
@ -103,14 +103,14 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
-- The transformation will be the identity on 𝔻. Such an arrow has the
-- type `A.omap A → A.omap A`. Which we can coerce to have the type
-- `A.omap → B.omap` since `A` and `B` are equal.
coe𝟙 : Transformation A B
coe𝟙 X = coe coerceAB 𝔻.𝟙
coeidentity : Transformation A B
coeidentity X = coe coerceAB 𝔻.identity
module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where
nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ]
nat' : 𝔻 [ coeidentity b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coeidentity a ]
nat' = begin
(𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
(𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎
(𝔻 [ coeidentity b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
(𝔻 [ B.fmap f ∘ coeidentity a ]) ∎
transs : (i : I) → Transformation A (p i)
transs = {!!}
@ -118,26 +118,26 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
natt : (i : I) → Natural A (p i) {!!}
natt = {!!}
t : Natural A B coe𝟙
t : Natural A B coeidentity
t = coe c (identityNatural A)
where
c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙
c : Natural A A (identityTrans A) ≡ Natural A B coeidentity
c = begin
Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩
Natural A B coe𝟙 ∎
Natural A B coeidentity ∎
-- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!}
k : Natural A A (identityTrans A) → Natural A B coe𝟙
k : Natural A A (identityTrans A) → Natural A B coeidentity
k n {a} {b} f = res
where
res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ])
res : (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coeidentity a ])
res = {!!}
nat : Natural A B coe𝟙
nat : Natural A B coeidentity
nat = nat'
fromEq : NaturalTransformation A B
fromEq = coe𝟙 , nat
fromEq = coeidentity , nat
module _ {A B : Functor ℂ 𝔻} where
obverse : A ≡ B → A ≅ B
@ -147,9 +147,9 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
ob = fromEq p
re : Arrow B A
re = fromEq (sym p)
vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
vr : _∘_ {A = A} {B} {A} re ob ≡ identity A
vr = {!!}
rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
rv : _∘_ {A = B} {A} {B} ob re ≡ identity B
rv = {!!}
isInverse : IsInverseOf {A} {B} ob re
isInverse = vr , rv
@ -183,23 +183,42 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
Category.raw Fun = raw
Category.isCategory Fun = isCategory
-- module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-- private
-- open import Cat.Categories.Sets
-- open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
private
open import Cat.Categories.Sets
open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
module K = Fun (opposite ℂ) (𝓢𝓮𝓽 ℓ')
module F = Category K.Fun
-- -- Restrict the functors to Presheafs.
-- rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-- rawPresh = record
-- { Object = Presheaf ℂ
-- ; Arrow = NaturalTransformation
-- ; 𝟙 = λ {F} → identity F
-- ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
-- }
-- instance
-- isCategory : IsCategory rawPresh
-- isCategory = Fun.isCategory _ _
-- Restrict the functors to Presheafs.
raw : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
raw = record
{ Object = Presheaf ℂ
; Arrow = NaturalTransformation
; identity = λ {F} → identity F
; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
}
-- Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-- Category.raw Presh = rawPresh
-- Category.isCategory Presh = isCategory
isCategory : IsCategory raw
isCategory = record
{ isAssociative =
λ{ {A} {B} {C} {D} {f} {g} {h}
→ F.isAssociative {A} {B} {C} {D} {f} {g} {h}
}
; isIdentity =
λ{ {A} {B} {f}
→ F.isIdentity {A} {B} {f}
}
; arrowsAreSets =
λ{ {A} {B}
→ F.arrowsAreSets {A} {B}
}
; univalent =
λ{ {A} {B}
→ F.univalent {A} {B}
}
}
Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
Category.raw Presh = raw
Category.isCategory Presh = isCategory

2
src/Cat/Categories/Rel.agda
View file

@ -153,7 +153,7 @@ RawRel : RawCategory (lsuc lzero) (lsuc lzero)
RawRel = record
{ Object = Set
; Arrow = λ S R → Subset (S × R)
; 𝟙 = λ {S} → Diag S
; identity = λ {S} → Diag S
; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
}

8
src/Cat/Categories/Sets.agda
View file

@ -60,10 +60,10 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
module _ (ℓ : Level) where
private
SetsRaw : RawCategory (lsuc ℓ) ℓ
RawCategory.Object SetsRaw = hSet ℓ
RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U
RawCategory.𝟙 SetsRaw = Function.id
RawCategory._∘_ SetsRaw = Function._∘′_
RawCategory.Object SetsRaw = hSet ℓ
RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U
RawCategory.identity SetsRaw = Function.id
RawCategory._∘_ SetsRaw = Function._∘′_
open RawCategory SetsRaw hiding (_∘_)

72
src/Cat/Category.agda
View file

@ -12,7 +12,7 @@
--
-- Data
-- ----
-- 𝟙; the identity arrow
-- identity; the identity arrow
-- _∘_; function composition
--
-- Laws
@ -48,10 +48,10 @@ import Function
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
Object : Set ℓa
Arrow : Object → Object → Set ℓb
identity : {A : Object} → Arrow A A
_∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
infixl 10 _∘_ _>>>_
@ -82,7 +82,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
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 ≡ 𝟙
IsInverseOf = λ f g → g ∘ f ≡ identity × f ∘ g ≡ identity
Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
@ -110,10 +110,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
Terminal = Σ Object IsTerminal
-- | Univalence is indexed by a raw category as well as an identity proof.
module Univalence (isIdentity : IsIdentity 𝟙) where
module Univalence (isIdentity : IsIdentity identity) where
-- | The identity isomorphism
idIso : (A : Object) → A ≅ A
idIso A = 𝟙 , 𝟙 , isIdentity
idIso A = identity , identity , isIdentity
-- | Extract an isomorphism from an equality
--
@ -150,16 +150,16 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
open RawCategory ℂ public
field
isAssociative : IsAssociative
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
arrowsAreSets : ArrowsAreSets
open Univalence isIdentity public
field
univalent : Univalent
leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f
leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ f ≡ f
leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f})
rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f
rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ identity ≡ f
rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f})
------------
@ -171,24 +171,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
iso→epi : Isomorphism f → Epimorphism {X = X} f
iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym rightIdentity ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ identity ≡⟨ 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₁ ∘ 𝟙 ≡⟨ rightIdentity ⟩
g₁ ∘ identity ≡⟨ rightIdentity ⟩
g₁ ∎
iso→mono : Isomorphism f → Monomorphism {X = X} f
iso→mono (f- , left-inv , right-inv) g₀ g₁ eq =
begin
g₀ ≡⟨ sym leftIdentity ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
identity ∘ 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₁ ≡⟨ leftIdentity ⟩
identity ∘ g₁ ≡⟨ leftIdentity ⟩
g₁ ∎
iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
@ -228,12 +228,12 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
where
geq : g ≡ g'
geq = begin
g ≡⟨ sym rightIdentity ⟩
g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
𝟙 ∘ g' ≡⟨ leftIdentity ⟩
g' ∎
g ≡⟨ sym rightIdentity ⟩
g ∘ identity ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
identity ∘ g' ≡⟨ leftIdentity ⟩
g' ∎
propUnivalent : isProp Univalent
propUnivalent a b i = propPi (λ iso → propIsContr) a b i
@ -274,9 +274,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
Xprop f g = trans (sym (snd Xit f)) (snd Xit g)
Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yit f)) (snd Yit g)
left : Y→X ∘ X→Y ≡ 𝟙
left : Y→X ∘ X→Y ≡ identity
left = Xprop _ _
right : X→Y ∘ Y→X ≡ 𝟙
right : X→Y ∘ Y→X ≡ identity
right = Yprop _ _
iso : X ≅ Y
iso = X→Y , Y→X , left , right
@ -321,9 +321,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
Xprop f g = trans (sym (snd Xii f)) (snd Xii g)
Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yii f)) (snd Yii g)
left : Y→X ∘ X→Y ≡ 𝟙
left : Y→X ∘ X→Y ≡ identity
left = Yprop _ _
right : X→Y ∘ Y→X ≡ 𝟙
right : X→Y ∘ Y→X ≡ identity
right = Xprop _ _
iso : X ≅ Y
iso = Y→X , X→Y , right , left
@ -351,18 +351,18 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
-- adverse effects this may have.
module Prop = X.Propositionality
isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
isIdentity : (λ _ → IsIdentity identity) [ X.isIdentity ≡ Y.isIdentity ]
isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity
U : ∀ {a : IsIdentity 𝟙}
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
U : ∀ {a : IsIdentity identity}
→ (λ _ → IsIdentity identity) [ X.isIdentity ≡ a ]
→ (b : Univalent a)
→ Set _
U eqwal univ =
(λ i → Univalent (eqwal i))
[ X.univalent ≡ univ ]
P : (y : IsIdentity 𝟙)
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
P : (y : IsIdentity identity)
→ (λ _ → IsIdentity identity) [ X.isIdentity ≡ y ] → Set _
P y eq = ∀ (univ : Univalent y) → U eq univ
p : ∀ (b' : Univalent X.isIdentity)
→ (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
@ -426,14 +426,14 @@ module Opposite {ℓa ℓb : Level} where
private
module ℂ = Category ℂ
opRaw : RawCategory ℓa ℓb
RawCategory.Object opRaw = ℂ.Object
RawCategory.Arrow opRaw = Function.flip ℂ.Arrow
RawCategory.𝟙 opRaw = ℂ.𝟙
RawCategory._∘_ opRaw = Function.flip ℂ._∘_
RawCategory.Object opRaw = ℂ.Object
RawCategory.Arrow opRaw = Function.flip ℂ.Arrow
RawCategory.identity opRaw = ℂ.identity
RawCategory._∘_ opRaw = Function.flip ℂ._∘_
open RawCategory opRaw
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity = swap ℂ.isIdentity
open Univalence isIdentity
@ -530,7 +530,7 @@ module Opposite {ℓa ℓb : Level} where
rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
RawCategory.Object (rawInv _) = Object
RawCategory.Arrow (rawInv _) = Arrow
RawCategory.𝟙 (rawInv _) = 𝟙
RawCategory.identity (rawInv _) = identity
RawCategory._∘_ (rawInv _) = _∘_
oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ

4
src/Cat/Category/Exponential.agda
View file

@ -16,11 +16,11 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
field
uniq
: ∀ (A : Object) (f : ℂ [ A × B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f)
IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
→ ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f)
record Exponential : Set (ℓ ⊔ ℓ') where
field

10
src/Cat/Category/Functor.agda
View file

@ -30,7 +30,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
IsIdentity : Set _
IsIdentity = {A : ℂ.Object} → fmap (ℂ.𝟙 {A}) ≡ 𝔻.𝟙 {omap A}
IsIdentity = {A : ℂ.Object} → fmap (ℂ.identity {A}) ≡ 𝔻.identity {omap A}
IsDistributive : Set _
IsDistributive = {A B C : ℂ.Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
@ -150,10 +150,10 @@ module _ {ℓ0 ℓ1 ℓ2 ℓ3 ℓ4 ℓ5 : Level}
isFunctor : IsFunctor A C raw
isFunctor = record
{ isIdentity = begin
(F.fmap ∘ G.fmap) A.𝟙 ≡⟨ refl ⟩
F.fmap (G.fmap A.𝟙) ≡⟨ cong F.fmap (G.isIdentity)⟩
F.fmap B.𝟙 ≡⟨ F.isIdentity ⟩
C.𝟙 ∎
(F.fmap ∘ G.fmap) A.identity ≡⟨ refl ⟩
F.fmap (G.fmap A.identity) ≡⟨ cong F.fmap (G.isIdentity)⟩
F.fmap B.identity ≡⟨ F.isIdentity ⟩
C.identity ∎
; isDistributive = dist
}

34
src/Cat/Category/Monad.agda
View file

@ -33,10 +33,10 @@ module Kleisli = Cat.Category.Monad.Kleisli
-- | The monoidal- and kleisli presentation of monads are equivalent.
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Cat.Category.NaturalTransformation ℂ ℂ
open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural)
private
module ℂ = Category ℂ
open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
open ℂ using (Object ; Arrow ; identity ; _∘_ ; _>>>_)
module M = Monoidal ℂ
module K = Kleisli ℂ
@ -84,11 +84,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
inv-l = begin
joinT X ∘ pureT (R.omap X) ≡⟨⟩
join ∘ pure ≡⟨ proj₁ isInverse ⟩
𝟙 ∎
identity ∎
inv-r = begin
joinT X ∘ R.fmap (pureT X) ≡⟨⟩
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
𝟙 ∎
identity ∎
back : K.Monad → M.Monad
Monoidal.Monad.raw (back m) = backRaw m
@ -103,21 +103,21 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
bindEq {X} {Y} = begin
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
(λ f → join ∘ fmap f) ≡⟨⟩
(λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩
(λ f → bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem ⟩
(λ f → bind f) ≡⟨⟩
bind ∎
where
lem : (f : Arrow X (omap Y))
→ bind (f >>> pure) >>> bind 𝟙
→ bind (f >>> pure) >>> bind identity
≡ bind f
lem f = begin
bind (f >>> pure) >>> bind 𝟙
bind (f >>> pure) >>> bind identity
≡⟨ isDistributive _ _ ⟩
bind ((f >>> pure) >>> bind 𝟙)
bind ((f >>> pure) >>> bind identity)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (f >>> (pure >>> bind 𝟙))
bind (f >>> (pure >>> bind identity))
≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩
bind (f >>> 𝟙)
bind (f >>> identity)
≡⟨ cong bind ℂ.leftIdentity ⟩
bind f ∎
@ -146,10 +146,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
joinEq : ∀ {X} → KM.join ≡ joinT X
joinEq {X} = begin
KM.join ≡⟨⟩
KM.bind 𝟙 ≡⟨⟩
bind 𝟙 ≡⟨⟩
joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩
KM.bind identity ≡⟨⟩
bind identity ≡⟨⟩
joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩
joinT X ∎
fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap
@ -161,7 +161,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩
joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩
𝟙 ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩
identity ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩
Rfmap f ∎
)
@ -183,8 +183,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
joinTEq = funExt (λ X → begin
M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
KM.join ≡⟨⟩
joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩
joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩
joinT X ∎)
joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))

80
src/Cat/Category/Monad/Kleisli.agda
View file

@ -12,11 +12,13 @@ open import Cat.Categories.Fun
-- "A monad in the Kleisli form" [voe]
module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open import Cat.Category.NaturalTransformation ℂ ℂ hiding (propIsNatural)
open import Cat.Category.NaturalTransformation ℂ ℂ
using (NaturalTransformation ; Transformation ; Natural)
private
ℓ = ℓa ⊔ ℓb
module ℂ = Category ℂ
open ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
open ℂ using (Arrow ; identity ; Object ; _∘_ ; _>>>_)
-- | Data for a monad.
--
@ -40,7 +42,7 @@ record RawMonad : Set ℓ where
-- | Flattening nested monads.
join : {A : Object} → ℂ [ omap (omap A) , omap A ]
join = bind 𝟙
join = bind identity
------------------
-- * Monad laws --
@ -49,7 +51,7 @@ record RawMonad : Set ℓ where
-- There may be better names than what I've chosen here.
IsIdentity = {X : Object}
→ bind pure ≡ 𝟙 {omap X}
→ bind pure ≡ identity {omap X}
IsNatural = {X Y : Object} (f : ℂ [ X , omap Y ])
→ pure >>> (bind f) ≡ f
IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ])
@ -67,7 +69,7 @@ record RawMonad : Set ℓ where
IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join
IsInverse : Set _
IsInverse = {X : Object} → join {X} ∘ pure ≡ 𝟙 × join {X} ∘ fmap pure ≡ 𝟙
IsInverse = {X : Object} → join {X} ∘ pure ≡ identity × join {X} ∘ fmap pure ≡ identity
record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public
@ -100,9 +102,9 @@ record IsMonad (raw : RawMonad) : Set ℓ where
isFunctorR : IsFunctor ℂ ℂ rawR
IsFunctor.isIdentity isFunctorR = begin
bind (pure ∘ 𝟙) ≡⟨ cong bind (ℂ.rightIdentity) ⟩
bind pure ≡⟨ isIdentity ⟩
𝟙 ∎
bind (pure ∘ identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩
bind pure ≡⟨ isIdentity ⟩
identity ∎
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
bind (pure ∘ (g ∘ f)) ≡⟨⟩
@ -137,29 +139,29 @@ record IsMonad (raw : RawMonad) : Set ℓ where
joinN : Natural R² R joinT
joinN f = begin
join ∘ R².fmap f ≡⟨⟩
bind 𝟙 ∘ R².fmap f ≡⟨⟩
R².fmap f >>> bind 𝟙 ≡⟨⟩
fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
bind identity ∘ R².fmap f ≡⟨⟩
R².fmap f >>> bind identity ≡⟨⟩
fmap (fmap f) >>> bind identity ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩
bind (bind (f >>> pure) >>> pure) >>> bind identity
≡⟨ isDistributive _ _ ⟩
bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
bind ((bind (f >>> pure) >>> pure) >=> identity)
≡⟨⟩
bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
bind ((bind (f >>> pure) >>> pure) >>> bind identity)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
bind (bind (f >>> pure) >>> (pure >>> bind identity))
≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩
bind (bind (f >>> pure) >>> 𝟙)
bind (bind (f >>> pure) >>> identity)
≡⟨ cong bind ℂ.leftIdentity ⟩
bind (bind (f >>> pure))
≡⟨ cong bind (sym ℂ.rightIdentity) ⟩
bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
bind (𝟙 >=> (f >>> pure))
bind (identity >>> bind (f >>> pure)) ≡⟨⟩
bind (identity >=> (f >>> pure))
≡⟨ sym (isDistributive _ _) ⟩
bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩
bind 𝟙 >>> fmap f ≡⟨⟩
bind 𝟙 >>> R.fmap f ≡⟨⟩
R.fmap f ∘ bind 𝟙 ≡⟨⟩
bind identity >>> bind (f >>> pure) ≡⟨⟩
bind identity >>> fmap f ≡⟨⟩
bind identity >>> R.fmap f ≡⟨⟩
R.fmap f ∘ bind identity ≡⟨⟩
R.fmap f ∘ join ∎
pureNT : NaturalTransformation R⁰ R
@ -173,20 +175,20 @@ record IsMonad (raw : RawMonad) : Set ℓ where
isNaturalForeign : IsNaturalForeign
isNaturalForeign = begin
fmap join >>> join ≡⟨⟩
bind (join >>> pure) >>> bind 𝟙
bind (join >>> pure) >>> bind identity
≡⟨ isDistributive _ _ ⟩
bind ((join >>> pure) >>> bind 𝟙)
bind ((join >>> pure) >>> bind identity)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (join >>> (pure >>> bind 𝟙))
bind (join >>> (pure >>> bind identity))
≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩
bind (join >>> 𝟙)
bind (join >>> identity)
≡⟨ cong bind ℂ.leftIdentity ⟩
bind join ≡⟨⟩
bind (bind 𝟙)
bind (bind identity)
≡⟨ cong bind (sym ℂ.rightIdentity) ⟩
bind (𝟙 >>> bind 𝟙) ≡⟨⟩
bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _) ⟩
bind 𝟙 >>> bind 𝟙 ≡⟨⟩
bind (identity >>> bind identity) ≡⟨⟩
bind (identity >=> identity) ≡⟨ sym (isDistributive _ _) ⟩
bind identity >>> bind identity ≡⟨⟩
join >>> join ∎
isInverse : IsInverse
@ -194,21 +196,21 @@ record IsMonad (raw : RawMonad) : Set ℓ where
where
inv-l = begin
pure >>> join ≡⟨⟩
pure >>> bind 𝟙 ≡⟨ isNatural _ ⟩
𝟙 ∎
pure >>> bind identity ≡⟨ isNatural _ ⟩
identity ∎
inv-r = begin
fmap pure >>> join ≡⟨⟩
bind (pure >>> pure) >>> bind 𝟙
bind (pure >>> pure) >>> bind identity
≡⟨ isDistributive _ _ ⟩
bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
bind ((pure >>> pure) >>> bind 𝟙)
bind ((pure >>> pure) >=> identity) ≡⟨⟩
bind ((pure >>> pure) >>> bind identity)
≡⟨ cong bind ℂ.isAssociative ⟩
bind (pure >>> (pure >>> bind 𝟙))
bind (pure >>> (pure >>> bind identity))
≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩
bind (pure >>> 𝟙)
bind (pure >>> identity)
≡⟨ cong bind ℂ.leftIdentity ⟩
bind pure ≡⟨ isIdentity ⟩
𝟙 ∎
identity ∎
record Monad : Set ℓ where
field

10
src/Cat/Category/Monad/Monoidal.agda
View file

@ -16,8 +16,10 @@ module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb
private
ℓ = ℓa ⊔ ℓb
open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
open Category ℂ using (Object ; Arrow ; identity ; _∘_)
open import Cat.Category.NaturalTransformation ℂ ℂ
using (NaturalTransformation ; Transformation ; Natural)
record RawMonad : Set ℓ where
field
R : EndoFunctor ℂ
@ -47,8 +49,8 @@ record RawMonad : Set ℓ where
→ joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X)
IsInverse : Set _
IsInverse = {X : Object}
→ joinT X ∘ pureT (Romap X) ≡ 𝟙
× joinT X ∘ Rfmap (pureT X) ≡ 𝟙
→ joinT X ∘ pureT (Romap X) ≡ identity
× joinT X ∘ Rfmap (pureT X) ≡ identity
IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f
IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
→ joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f)
@ -70,7 +72,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
𝟙 ∘ f ≡⟨ ℂ.leftIdentity ⟩
identity ∘ f ≡⟨ ℂ.leftIdentity ⟩
f ∎
isDistributive : IsDistributive

8
src/Cat/Category/NaturalTransformation.agda
View file

@ -31,7 +31,7 @@ module Cat.Category.NaturalTransformation
{ℓc ℓc' ℓd ℓd' : Level}
(ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙)
open Category using (Object)
private
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
@ -63,14 +63,14 @@ module _ (F G : Functor ℂ 𝔻) where
NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝟙 𝔻
identityTrans F C = 𝔻.identity
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩
𝔻 [ 𝔻.identity ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩
F→ f ≡⟨ sym 𝔻.rightIdentity ⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ 𝔻.identity ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
module F = Functor F

14
src/Cat/Category/Product.agda
View file

@ -134,7 +134,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
( ℂ [ ya ∘ xy ] ≡ xa)
× ℂ [ yb ∘ xy ] ≡ xb
}
; 𝟙 = λ{ {A , f , g} → ℂ.𝟙 {A} , ℂ.rightIdentity , ℂ.rightIdentity}
; identity = λ{ {A , f , g} → ℂ.identity {A} , ℂ.rightIdentity , ℂ.rightIdentity}
; _∘_ = λ { {A , a0 , a1} {B , b0 , b1} {C , c0 , c1} (f , f0 , f1) (g , g0 , g1)
→ (f ℂ.∘ g)
, (begin
@ -169,24 +169,24 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
s0 = ℂ.isAssociative {f = f} {g} {h}
isIdentity : IsIdentity 𝟙
isIdentity : IsIdentity identity
isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
where
leftIdentity : 𝟙 ∘ (f , f0 , f1) ≡ (f , f0 , f1)
leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1)
leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
where
L = 𝟙 ∘ (f , f0 , f1)
L = identity ∘ (f , f0 , f1)
R : Arrow AA BB
R = f , f0 , f1
l : proj₁ L ≡ proj₁ R
l = ℂ.leftIdentity
rightIdentity : (f , f0 , f1) ∘ 𝟙 ≡ (f , f0 , f1)
rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1)
rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
where
L = (f , f0 , f1) ∘ 𝟙
L = (f , f0 , f1) ∘ identity
R : Arrow AA BB
R = (f , f0 , f1)
l : ℂ [ f ∘ ℂ.𝟙 ] ≡ f
l : ℂ [ f ∘ ℂ.identity ] ≡ f
l = ℂ.rightIdentity
arrowsAreSets : ArrowsAreSets

2
src/Cat/Category/Yoneda.agda
View file

@ -52,7 +52,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
isIdentity : IsIdentity
isIdentity {c} = lemSig prp _ _ eq
where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c)
eq : (λ C x → ℂ [ ℂ.identity ∘ x ]) ≡ identityTrans (presheaf c)
eq = funExt λ A → funExt λ B → ℂ.leftIdentity
prp = F.naturalIsProp _ _ {F = presheaf c} {presheaf c}