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

Rename \o to <<<

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-11 10:58:50 +02:00
parent 6d59a8f79e
commit c90b064bb0
12 changed files with 191 additions and 188 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -18,7 +18,7 @@ module _ (ℓ ℓ' : Level) where
RawCategory.Object RawCat = Category ℓ ℓ' RawCategory.Object RawCat = Category ℓ ℓ'
RawCategory.Arrow RawCat = Functor RawCategory.Arrow RawCat = Functor
RawCategory.identity RawCat = Functors.identity RawCategory.identity RawCat = Functors.identity
RawCategory._∘_ RawCat = F[_∘_] RawCategory._<<<_ RawCat = F[_∘_]
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of -- however, form a groupoid! Therefore there is no (1-)category of
@ -50,18 +50,18 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
identity : {o : Obj} → Arr o o identity : {o : Obj} → Arr o o
identity = ℂ.identity , 𝔻.identity identity = ℂ.identity , 𝔻.identity
_∘_ : _<<<_ :
{a b c : Obj} → {a b c : Obj} →
Arr b c → Arr b c →
Arr a b → Arr a b →
Arr a c Arr a c
_∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} _<<<_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
rawProduct : RawCategory ℓ ℓ' rawProduct : RawCategory ℓ ℓ'
RawCategory.Object rawProduct = Obj RawCategory.Object rawProduct = Obj
RawCategory.Arrow rawProduct = Arr RawCategory.Arrow rawProduct = Arr
RawCategory.identity rawProduct = identity RawCategory.identity rawProduct = identity
RawCategory._∘_ rawProduct = _∘_ RawCategory._<<<_ rawProduct = _<<<_
open RawCategory rawProduct open RawCategory rawProduct

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

@ -19,7 +19,7 @@ open import Cat.Category.Functor
-- See section 6.8 in Huber's thesis for details on how to implement the -- See section 6.8 in Huber's thesis for details on how to implement the
-- categorical version of CTT -- categorical version of CTT
open Category hiding (_∘_) open Category hiding (_<<<_)
open Functor open Functor
module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
@ -68,7 +68,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
Raw.Object Rawℂ = FiniteDecidableSubset Raw.Object Rawℂ = FiniteDecidableSubset
Raw.Arrow Rawℂ = Hom Raw.Arrow Rawℂ = Hom
Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
Raw._∘_ Rawℂ = {!!} Raw._<<<_ Rawℂ = {!!}
postulate IsCategoryℂ : IsCategory Rawℂ postulate IsCategoryℂ : IsCategory Rawℂ

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

@ -14,15 +14,15 @@ module _ (ℓa ℓb : Level) where
identity : {A : Object} → Arr A A identity : {A : Object} → Arr A A
fst identity = λ x → x fst identity = λ x → x
snd identity = λ b → b snd identity = λ b → b
_∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c _<<<_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
(g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f' (g , g') <<< (f , f') = g Function.∘ f , g' Function.∘ f'
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb) RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
RawFam = record RawFam = record
{ Object = Object { Object = Object
; Arrow = Arr ; Arrow = Arr
; identity = λ { {A} → identity {A = A}} ; identity = λ { {A} → identity {A = A}}
; _∘_ = λ {a b c} → _∘_ {a} {b} {c} ; _<<<_ = λ {a b c} → _<<<_ {a} {b} {c}
} }
open RawCategory RawFam hiding (Object ; identity) open RawCategory RawFam hiding (Object ; identity)

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

@ -30,7 +30,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
RawCategory.Object RawFree = ℂ.Object RawCategory.Object RawFree = ℂ.Object
RawCategory.Arrow RawFree = Path ℂ.Arrow RawCategory.Arrow RawFree = Path ℂ.Arrow
RawCategory.identity RawFree = empty RawCategory.identity RawFree = empty
RawCategory._∘_ RawFree = concatenate RawCategory._<<<_ RawFree = concatenate
open RawCategory RawFree open RawCategory RawFree

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

@ -20,7 +20,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
RawCategory.Object raw = Functor ℂ 𝔻 RawCategory.Object raw = Functor ℂ 𝔻
RawCategory.Arrow raw = NaturalTransformation RawCategory.Arrow raw = NaturalTransformation
RawCategory.identity raw {F} = identity F RawCategory.identity raw {F} = identity F
RawCategory._∘_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H} RawCategory._<<<_ raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
module _ where module _ where
open RawCategory raw hiding (identity) open RawCategory raw hiding (identity)
@ -154,9 +154,9 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
ob = fromEq p ob = fromEq p
re : Arrow B A re : Arrow B A
re = fromEq (sym p) re = fromEq (sym p)
vr : _∘_ {A = A} {B} {A} re ob ≡ identity A vr : _<<<_ {A = A} {B} {A} re ob ≡ identity A
vr = {!!} vr = {!!}
rv : _∘_ {A = B} {A} {B} ob re ≡ identity B rv : _<<<_ {A = B} {A} {B} ob re ≡ identity B
rv = {!!} rv = {!!}
isInverse : IsInverseOf {A} {B} ob re isInverse : IsInverseOf {A} {B} ob re
isInverse = vr , rv isInverse = vr , rv
@ -201,7 +201,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
{ Object = Presheaf ℂ { Object = Presheaf ℂ
; Arrow = NaturalTransformation ; Arrow = NaturalTransformation
; identity = λ {F} → identity F ; identity = λ {F} → identity F
; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H} ; _<<<_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
} }
-- isCategory : IsCategory raw -- isCategory : IsCategory raw

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

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

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

@ -26,11 +26,11 @@ module _ (ℓ : Level) where
RawCategory.Object SetsRaw = hSet ℓ RawCategory.Object SetsRaw = hSet ℓ
RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U
RawCategory.identity SetsRaw = Function.id RawCategory.identity SetsRaw = Function.id
RawCategory._∘_ SetsRaw = Function._∘′_ RawCategory._<<<_ SetsRaw = Function._∘′_
module _ where module _ where
private private
open RawCategory SetsRaw hiding (_∘_) open RawCategory SetsRaw hiding (_<<<_)
isIdentity : IsIdentity Function.id isIdentity : IsIdentity Function.id
fst isIdentity = funExt λ _ → refl fst isIdentity = funExt λ _ → refl
@ -44,7 +44,7 @@ module _ (ℓ : Level) where
IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B} IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B}
IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B} IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B}
open IsPreCategory isPreCat hiding (_∘_) open IsPreCategory isPreCat hiding (_<<<_)
isIso = TypeIsomorphism isIso = TypeIsomorphism
module _ {hA hB : hSet ℓ} where module _ {hA hB : hSet ℓ} where

98
src/Cat/Category.agda
View file

@ -13,7 +13,7 @@
-- Data -- Data
-- ---- -- ----
-- identity; the identity arrow -- identity; the identity arrow
-- _∘_; function composition -- _<<<_; function composition
-- --
-- Laws -- Laws
-- ---- -- ----
@ -52,9 +52,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
Object : Set ℓa Object : Set ℓa
Arrow : Object → Object → Set ℓb Arrow : Object → Object → Set ℓb
identity : {A : Object} → Arrow A A identity : {A : Object} → Arrow A A
_∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C _<<<_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
infixl 10 _∘_ _>>>_ infixl 10 _<<<_ _>>>_
-- | Operations on data -- | Operations on data
@ -65,7 +65,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
codomain {b = b} _ = b codomain {b = b} _ = b
_>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C
f >>> g = g ∘ f f >>> g = g <<< f
-- | Laws about the data -- | Laws about the data
@ -73,17 +73,17 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
-- right-hand-side. -- right-hand-side.
IsAssociative : Set (ℓa ⊔ ℓb) IsAssociative : Set (ℓa ⊔ ℓb)
IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D} IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
→ h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f → h <<< (g <<< f) ≡ (h <<< g) <<< f
IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb) IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
IsIdentity id = {A B : Object} {f : Arrow A B} IsIdentity id = {A B : Object} {f : Arrow A B}
→ id ∘ f ≡ f × f ∘ id ≡ f → id <<< f ≡ f × f <<< id ≡ f
ArrowsAreSets : Set (ℓa ⊔ ℓb) ArrowsAreSets : Set (ℓa ⊔ ℓb)
ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
IsInverseOf = λ f g → g ∘ f ≡ identity × f ∘ g ≡ identity IsInverseOf = λ f g → g <<< f ≡ identity × f <<< g ≡ identity
Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
@ -93,10 +93,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
module _ {A B : Object} where module _ {A B : Object} where
Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
Epimorphism {X} f = (g₀ g₁ : Arrow B X) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁ 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 : Object} → (f : Arrow A B) → Set ℓb
Monomorphism {X} f = (g₀ g₁ : Arrow X A) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁ Monomorphism {X} f = (g₀ g₁ : Arrow X A) → f <<< g₀ ≡ f <<< g₁ → g₀ ≡ g₁
IsInitial : Object → Set (ℓa ⊔ ℓb) IsInitial : Object → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Object} → isContr (Arrow I X) IsInitial I = {X : Object} → isContr (Arrow I X)
@ -167,10 +167,10 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
arrowsAreSets : ArrowsAreSets arrowsAreSets : ArrowsAreSets
open Univalence isIdentity public open Univalence isIdentity public
leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ f ≡ f leftIdentity : {A B : Object} {f : Arrow A B} → identity <<< f ≡ f
leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f})
rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ identity ≡ f rightIdentity : {A B : Object} {f : Arrow A B} → f <<< identity ≡ f
rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f})
------------ ------------
@ -182,24 +182,24 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
iso→epi : Isomorphism f → Epimorphism {X = X} f iso→epi : Isomorphism f → Epimorphism {X = X} f
iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym rightIdentity ⟩ g₀ ≡⟨ sym rightIdentity ⟩
g₀ ∘ identity ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ <<< identity ≡⟨ cong (_<<<_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ g₀ <<< (f <<< f-) ≡⟨ isAssociative ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ (g₀ <<< f) <<< f- ≡⟨ cong (λ φ → φ <<< f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ (g₁ <<< f) <<< f- ≡⟨ sym isAssociative ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ g₁ <<< (f <<< f-) ≡⟨ cong (_<<<_ g₁) right-inv ⟩
g₁ ∘ identity ≡⟨ rightIdentity ⟩ g₁ <<< identity ≡⟨ rightIdentity ⟩
g₁ ∎ g₁ ∎
iso→mono : Isomorphism f → Monomorphism {X = X} f iso→mono : Isomorphism f → Monomorphism {X = X} f
iso→mono (f- , left-inv , right-inv) g₀ g₁ eq = iso→mono (f- , left-inv , right-inv) g₀ g₁ eq =
begin begin
g₀ ≡⟨ sym leftIdentity ⟩ g₀ ≡⟨ sym leftIdentity ⟩
identity ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ identity <<< g₀ ≡⟨ cong (λ φ → φ <<< g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ (f- <<< f) <<< g₀ ≡⟨ sym isAssociative ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ f- <<< (f <<< g₀) ≡⟨ cong (_<<<_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ f- <<< (f <<< g₁) ≡⟨ isAssociative ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ (f- <<< f) <<< g₁ ≡⟨ cong (λ φ → φ <<< g₁) left-inv ⟩
identity ∘ g₁ ≡⟨ leftIdentity ⟩ identity <<< g₁ ≡⟨ leftIdentity ⟩
g₁ ∎ g₁ ∎
iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
@ -210,7 +210,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f) propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
propIsIdentity {id} = propPiImpl (λ _ → propPiImpl λ _ → propPiImpl (λ f → propIsIdentity {id} = propPiImpl (λ _ → propPiImpl λ _ → propPiImpl (λ f →
propSig (arrowsAreSets (id ∘ f) f) λ _ → arrowsAreSets (f ∘ id) f)) propSig (arrowsAreSets (id <<< f) f) λ _ → arrowsAreSets (f <<< id) f))
propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B)) propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
propArrowIsSet = propPiImpl λ _ → propPiImpl (λ _ → isSetIsProp) propArrowIsSet = propPiImpl λ _ → propPiImpl (λ _ → isSetIsProp)
@ -226,10 +226,10 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
geq : g ≡ g' geq : g ≡ g'
geq = begin geq = begin
g ≡⟨ sym rightIdentity ⟩ g ≡⟨ sym rightIdentity ⟩
g ∘ identity ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ g <<< identity ≡⟨ cong (λ φ → g <<< φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ g <<< (f <<< g') ≡⟨ isAssociative ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ (g <<< f) <<< g' ≡⟨ cong (λ φ → φ <<< g') η ⟩
identity ∘ g' ≡⟨ leftIdentity ⟩ identity <<< g' ≡⟨ leftIdentity ⟩
g' ∎ g' ∎
propIsInitial : ∀ I → isProp (IsInitial I) propIsInitial : ∀ I → isProp (IsInitial I)
@ -266,22 +266,22 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
private private
trans≅ : Transitive _≅_ trans≅ : Transitive _≅_
trans≅ (f , f~ , f-inv) (g , g~ , g-inv) trans≅ (f , f~ , f-inv) (g , g~ , g-inv)
= g ∘ f = g <<< f
, f~ ∘ g~ , f~ <<< g~
, ( begin , ( begin
(f~ ∘ g~) ∘ (g ∘ f) ≡⟨ isAssociative ⟩ (f~ <<< g~) <<< (g <<< f) ≡⟨ isAssociative ⟩
(f~ ∘ g~) ∘ g ∘ f ≡⟨ cong (λ φ → φ ∘ f) (sym isAssociative) ⟩ (f~ <<< g~) <<< g <<< f ≡⟨ cong (λ φ → φ <<< f) (sym isAssociative) ⟩
f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) (fst g-inv) ⟩ f~ <<< (g~ <<< g) <<< f ≡⟨ cong (λ φ → f~ <<< φ <<< f) (fst g-inv) ⟩
f~ ∘ identity ∘ f ≡⟨ cong (λ φ → φ ∘ f) rightIdentity ⟩ f~ <<< identity <<< f ≡⟨ cong (λ φ → φ <<< f) rightIdentity ⟩
f~ ∘ f ≡⟨ fst f-inv ⟩ f~ <<< f ≡⟨ fst f-inv ⟩
identity ∎ identity ∎
) )
, ( begin , ( begin
g ∘ f ∘ (f~ ∘ g~) ≡⟨ isAssociative ⟩ g <<< f <<< (f~ <<< g~) ≡⟨ isAssociative ⟩
g ∘ f ∘ f~ ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) (sym isAssociative) ⟩ g <<< f <<< f~ <<< g~ ≡⟨ cong (λ φ → φ <<< g~) (sym isAssociative) ⟩
g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) (snd f-inv) ⟩ g <<< (f <<< f~) <<< g~ ≡⟨ cong (λ φ → g <<< φ <<< g~) (snd f-inv) ⟩
g ∘ identity ∘ g~ ≡⟨ cong (λ φ → φ ∘ g~) rightIdentity ⟩ g <<< identity <<< g~ ≡⟨ cong (λ φ → φ <<< g~) rightIdentity ⟩
g ∘ g~ ≡⟨ snd g-inv ⟩ g <<< g~ ≡⟨ snd g-inv ⟩
identity ∎ identity ∎
) )
isPreorder : IsPreorder _≅_ isPreorder : IsPreorder _≅_
@ -341,7 +341,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
pq : Arrow a b ≡ Arrow a' b' pq : Arrow a b ≡ Arrow a' b'
pq i = Arrow (p i) (q i) pq i = Arrow (p i) (q i)
9-1-9 : coe pq f ≡ q* ∘ f ∘ p~ 9-1-9 : coe pq f ≡ q* <<< f <<< p~
9-1-9 = transpP {!!} {!!} 9-1-9 = transpP {!!} {!!}
-- | All projections are propositions. -- | All projections are propositions.
@ -366,9 +366,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
Xprop f g = trans (sym (snd Xit f)) (snd Xit g) Xprop f g = trans (sym (snd Xit f)) (snd Xit g)
Yprop : isProp (Arrow Y Y) Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yit f)) (snd Yit g) Yprop f g = trans (sym (snd Yit f)) (snd Yit g)
left : Y→X ∘ X→Y ≡ identity left : Y→X <<< X→Y ≡ identity
left = Xprop _ _ left = Xprop _ _
right : X→Y ∘ Y→X ≡ identity right : X→Y <<< Y→X ≡ identity
right = Yprop _ _ right = Yprop _ _
iso : X ≅ Y iso : X ≅ Y
iso = X→Y , Y→X , left , right iso = X→Y , Y→X , left , right
@ -396,9 +396,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
Xprop f g = trans (sym (snd Xii f)) (snd Xii g) Xprop f g = trans (sym (snd Xii f)) (snd Xii g)
Yprop : isProp (Arrow Y Y) Yprop : isProp (Arrow Y Y)
Yprop f g = trans (sym (snd Yii f)) (snd Yii g) Yprop f g = trans (sym (snd Yii f)) (snd Yii g)
left : Y→X ∘ X→Y ≡ identity left : Y→X <<< X→Y ≡ identity
left = Yprop _ _ left = Yprop _ _
right : X→Y ∘ Y→X ≡ identity right : X→Y <<< Y→X ≡ identity
right = Xprop _ _ right = Xprop _ _
iso : X ≅ Y iso : X ≅ Y
iso = Y→X , X→Y , right , left iso = Y→X , X→Y , right , left
@ -497,7 +497,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
_[_,_] = Arrow _[_,_] = Arrow
_[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
_[_∘_] = _∘_ _[_∘_] = _<<<_
-- | The opposite category -- | The opposite category
-- --
@ -512,7 +512,7 @@ module Opposite {ℓa ℓb : Level} where
RawCategory.Object opRaw = ℂ.Object RawCategory.Object opRaw = ℂ.Object
RawCategory.Arrow opRaw = Function.flip ℂ.Arrow RawCategory.Arrow opRaw = Function.flip ℂ.Arrow
RawCategory.identity opRaw = ℂ.identity RawCategory.identity opRaw = ℂ.identity
RawCategory._∘_ opRaw = ℂ._>>>_ RawCategory._<<<_ opRaw = ℂ._>>>_
open RawCategory opRaw open RawCategory opRaw
@ -561,7 +561,7 @@ module Opposite {ℓa ℓb : Level} where
-- inv : AreInverses (ℂ.idToIso A B) f -- inv : AreInverses (ℂ.idToIso A B) f
inv-ζ : AreInverses (idToIso A B) ζ inv-ζ : AreInverses (idToIso A B) ζ
-- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B) -- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
inv-ζ = record inv-ζ = record
{ verso-recto = funExt (λ x → begin { verso-recto = funExt (λ x → begin
(ζ ⊙ idToIso A B) x ≡⟨⟩ (ζ ⊙ idToIso A B) x ≡⟨⟩
@ -600,7 +600,7 @@ module Opposite {ℓa ℓb : Level} where
RawCategory.Object (rawInv _) = Object RawCategory.Object (rawInv _) = Object
RawCategory.Arrow (rawInv _) = Arrow RawCategory.Arrow (rawInv _) = Arrow
RawCategory.identity (rawInv _) = identity RawCategory.identity (rawInv _) = identity
RawCategory._∘_ (rawInv _) = _∘_ RawCategory._<<<_ (rawInv _) = _<<<_
oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
oppositeIsInvolution = Category≡ rawInv oppositeIsInvolution = Category≡ rawInv

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

@ -36,7 +36,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural) open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural)
private private
module ℂ = Category ℂ module ℂ = Category ℂ
open ℂ using (Object ; Arrow ; identity ; _∘_ ; _>>>_) open ℂ using (Object ; Arrow ; identity ; _<<<_ ; _>>>_)
module M = Monoidal ℂ module M = Monoidal ℂ
module K = Kleisli ℂ module K = Kleisli ℂ
@ -74,20 +74,20 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
backIsMonad : M.IsMonad backRaw backIsMonad : M.IsMonad backRaw
M.IsMonad.isAssociative backIsMonad {X} = begin M.IsMonad.isAssociative backIsMonad {X} = begin
joinT X ∘ R.fmap (joinT X) ≡⟨⟩ joinT X <<< R.fmap (joinT X) ≡⟨⟩
join ∘ fmap (joinT X) ≡⟨⟩ join <<< fmap (joinT X) ≡⟨⟩
join ∘ fmap join ≡⟨ isNaturalForeign ⟩ join <<< fmap join ≡⟨ isNaturalForeign ⟩
join ∘ join ≡⟨⟩ join <<< join ≡⟨⟩
joinT X ∘ joinT (R.omap X) ∎ joinT X <<< joinT (R.omap X) ∎
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
where where
inv-l = begin inv-l = begin
joinT X ∘ pureT (R.omap X) ≡⟨⟩ joinT X <<< pureT (R.omap X) ≡⟨⟩
join ∘ pure ≡⟨ fst isInverse ⟩ join <<< pure ≡⟨ fst isInverse ⟩
identity ∎ identity ∎
inv-r = begin inv-r = begin
joinT X ∘ R.fmap (pureT X) ≡⟨⟩ joinT X <<< R.fmap (pureT X) ≡⟨⟩
join ∘ fmap pure ≡⟨ snd isInverse ⟩ join <<< fmap pure ≡⟨ snd isInverse ⟩
identity ∎ identity ∎
back : K.Monad → M.Monad back : K.Monad → M.Monad
@ -102,7 +102,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
≡ K.RawMonad.bind (K.Monad.raw m) ≡ K.RawMonad.bind (K.Monad.raw m)
bindEq {X} {Y} = begin bindEq {X} {Y} = begin
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩ K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
(λ f → join ∘ fmap f) ≡⟨⟩ (λ f → join <<< fmap f) ≡⟨⟩
(λ f → bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem ⟩ (λ f → bind (f >>> pure) >>> bind identity) ≡⟨ funExt lem ⟩
(λ f → bind f) ≡⟨⟩ (λ f → bind f) ≡⟨⟩
bind ∎ bind ∎
@ -140,7 +140,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f bindEq : ∀ {X Y} {f : Arrow X (Romap Y)} → KM.bind f ≡ bind f
bindEq {X} {Y} {f} = begin bindEq {X} {Y} {f} = begin
KM.bind f ≡⟨⟩ KM.bind f ≡⟨⟩
joinT Y ∘ Rfmap f ≡⟨⟩ joinT Y <<< Rfmap f ≡⟨⟩
bind f ∎ bind f ∎
joinEq : ∀ {X} → KM.join ≡ joinT X joinEq : ∀ {X} → KM.join ≡ joinT X
@ -148,8 +148,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
KM.join ≡⟨⟩ KM.join ≡⟨⟩
KM.bind identity ≡⟨⟩ KM.bind identity ≡⟨⟩
bind identity ≡⟨⟩ bind identity ≡⟨⟩
joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ joinT X <<< Rfmap identity ≡⟨ cong (λ φ → _ <<< φ) R.isIdentity ⟩
joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩ joinT X <<< identity ≡⟨ ℂ.rightIdentity ⟩
joinT X ∎ joinT X ∎
fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap
@ -160,8 +160,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩ Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩
Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩
joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (snd isInverse) ⟩ joinT B <<< Rfmap (pureT B) <<< Rfmap f ≡⟨ cong (λ φ → φ <<< Rfmap f) (snd isInverse) ⟩
identity ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ identity <<< Rfmap f ≡⟨ ℂ.leftIdentity ⟩
Rfmap f ∎ Rfmap f ∎
) )
@ -183,8 +183,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
joinTEq = funExt (λ X → begin joinTEq = funExt (λ X → begin
M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩ M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
KM.join ≡⟨⟩ KM.join ≡⟨⟩
joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ joinT X <<< Rfmap identity ≡⟨ cong (λ φ → joinT X <<< φ) R.isIdentity ⟩
joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩ joinT X <<< identity ≡⟨ ℂ.rightIdentity ⟩
joinT X ∎) joinT X ∎)
joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i)) joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))

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

@ -18,7 +18,7 @@ open import Cat.Category.NaturalTransformation ℂ ℂ
private private
ℓ = ℓa ⊔ ℓb ℓ = ℓa ⊔ ℓb
module ℂ = Category ℂ module ℂ = Category ℂ
open ℂ using (Arrow ; identity ; Object ; _∘_ ; _>>>_) open ℂ using (Arrow ; identity ; Object ; _<<<_ ; _>>>_)
-- | Data for a monad. -- | Data for a monad.
-- --
@ -34,7 +34,7 @@ record RawMonad : Set ℓ where
-- --
-- This should perhaps be defined in a "Klesli-version" of functors as well? -- This should perhaps be defined in a "Klesli-version" of functors as well?
fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ] fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ]
fmap f = bind (pure ∘ f) fmap f = bind (pure <<< f)
-- | Composition of monads aka. the kleisli-arrow. -- | Composition of monads aka. the kleisli-arrow.
_>=>_ : {A B C : Object} → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ] _>=>_ : {A B C : Object} → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ]
@ -62,14 +62,14 @@ record RawMonad : Set ℓ where
-- This is really a functor law. Should we have a kleisli-representation of -- This is really a functor law. Should we have a kleisli-representation of
-- functors as well and make them a super-class? -- functors as well and make them a super-class?
Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]} Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
→ fmap (g ∘ f) ≡ fmap g ∘ fmap f → fmap (g <<< f) ≡ fmap g <<< fmap f
-- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be: -- In the ("foreign") formulation of a monad `IsNatural`'s analogue here would be:
IsNaturalForeign : Set _ IsNaturalForeign : Set _
IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join IsNaturalForeign = {X : Object} → join {X} <<< fmap join ≡ join <<< join
IsInverse : Set _ IsInverse : Set _
IsInverse = {X : Object} → join {X} ∘ pure ≡ identity × join {X} ∘ fmap pure ≡ identity IsInverse = {X : Object} → join {X} <<< pure ≡ identity × join {X} <<< fmap pure ≡ identity
record IsMonad (raw : RawMonad) : Set ℓ where record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public open RawMonad raw public
@ -81,18 +81,21 @@ record IsMonad (raw : RawMonad) : Set ℓ where
-- | Map fusion is admissable. -- | Map fusion is admissable.
fusion : Fusion fusion : Fusion
fusion {g = g} {f} = begin fusion {g = g} {f} = begin
fmap (g ∘ f) ≡⟨⟩ fmap (g <<< f) ≡⟨⟩
bind ((f >>> g) >>> pure) ≡⟨ cong bind ℂ.isAssociative ⟩ bind ((f >>> g) >>> pure) ≡⟨ cong bind ℂ.isAssociative ⟩
bind (f >>> (g >>> pure)) ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩ bind (f >>> (g >>> pure))
bind (f >>> (pure >>> (bind (g >>> pure)))) ≡⟨⟩ ≡⟨ cong (λ φ → bind (f >>> φ)) (sym (isNatural _)) ⟩
bind (f >>> (pure >>> (bind (g >>> pure))))
≡⟨⟩
bind (f >>> (pure >>> fmap g)) ≡⟨⟩ bind (f >>> (pure >>> fmap g)) ≡⟨⟩
bind ((fmap g ∘ pure) ∘ f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩ bind ((fmap g <<< pure) <<< f) ≡⟨ cong bind (sym ℂ.isAssociative) ⟩
bind (fmap g ∘ (pure ∘ f)) ≡⟨ sym distrib ⟩ bind (fmap g <<< (pure <<< f)) ≡⟨ sym distrib ⟩
bind (pure ∘ g) ∘ bind (pure ∘ f) ≡⟨⟩ bind (pure <<< g) <<< bind (pure <<< f)
fmap g ∘ fmap f ∎ ≡⟨⟩
fmap g <<< fmap f ∎
where where
distrib : fmap g ∘ fmap f ≡ bind (fmap g ∘ (pure ∘ f)) distrib : fmap g <<< fmap f ≡ bind (fmap g <<< (pure <<< f))
distrib = isDistributive (pure ∘ g) (pure ∘ f) distrib = isDistributive (pure <<< g) (pure <<< f)
-- | This formulation gives rise to the following endo-functor. -- | This formulation gives rise to the following endo-functor.
private private
@ -102,15 +105,15 @@ record IsMonad (raw : RawMonad) : Set ℓ where
isFunctorR : IsFunctor ℂ ℂ rawR isFunctorR : IsFunctor ℂ ℂ rawR
IsFunctor.isIdentity isFunctorR = begin IsFunctor.isIdentity isFunctorR = begin
bind (pure ∘ identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ bind (pure <<< identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩
bind pure ≡⟨ isIdentity ⟩ bind pure ≡⟨ isIdentity ⟩
identity ∎ identity ∎
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
bind (pure ∘ (g ∘ f)) ≡⟨⟩ bind (pure <<< (g <<< f)) ≡⟨⟩
fmap (g ∘ f) ≡⟨ fusion ⟩ fmap (g <<< f) ≡⟨ fusion ⟩
fmap g ∘ fmap f ≡⟨⟩ fmap g <<< fmap f ≡⟨⟩
bind (pure ∘ g) ∘ bind (pure ∘ f) ∎ bind (pure <<< g) <<< bind (pure <<< f) ∎
-- FIXME Naming! -- FIXME Naming!
R : EndoFunctor ℂ R : EndoFunctor ℂ
@ -129,17 +132,17 @@ record IsMonad (raw : RawMonad) : Set ℓ where
pureT A = pure pureT A = pure
pureN : Natural R⁰ R pureT pureN : Natural R⁰ R pureT
pureN {A} {B} f = begin pureN {A} {B} f = begin
pureT B ∘ R⁰.fmap f ≡⟨⟩ pureT B <<< R⁰.fmap f ≡⟨⟩
pure ∘ f ≡⟨ sym (isNatural _) ⟩ pure <<< f ≡⟨ sym (isNatural _) ⟩
bind (pure ∘ f) ∘ pure ≡⟨⟩ bind (pure <<< f) <<< pure ≡⟨⟩
fmap f ∘ pure ≡⟨⟩ fmap f <<< pure ≡⟨⟩
R.fmap f ∘ pureT A ∎ R.fmap f <<< pureT A ∎
joinT : Transformation R² R joinT : Transformation R² R
joinT C = join joinT C = join
joinN : Natural R² R joinT joinN : Natural R² R joinT
joinN f = begin joinN f = begin
join ∘ R².fmap f ≡⟨⟩ join <<< R².fmap f ≡⟨⟩
bind identity ∘ R².fmap f ≡⟨⟩ bind identity <<< R².fmap f ≡⟨⟩
R².fmap f >>> bind identity ≡⟨⟩ R².fmap f >>> bind identity ≡⟨⟩
fmap (fmap f) >>> bind identity ≡⟨⟩ fmap (fmap f) >>> bind identity ≡⟨⟩
fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩ fmap (bind (f >>> pure)) >>> bind identity ≡⟨⟩
@ -161,8 +164,8 @@ record IsMonad (raw : RawMonad) : Set ℓ where
bind identity >>> bind (f >>> pure) ≡⟨⟩ bind identity >>> bind (f >>> pure) ≡⟨⟩
bind identity >>> fmap f ≡⟨⟩ bind identity >>> fmap f ≡⟨⟩
bind identity >>> R.fmap f ≡⟨⟩ bind identity >>> R.fmap f ≡⟨⟩
R.fmap f ∘ bind identity ≡⟨⟩ R.fmap f <<< bind identity ≡⟨⟩
R.fmap f ∘ join ∎ R.fmap f <<< join ∎
pureNT : NaturalTransformation R⁰ R pureNT : NaturalTransformation R⁰ R
fst pureNT = pureT fst pureNT = pureT

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

@ -16,7 +16,7 @@ module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb
private private
ℓ = ℓa ⊔ ℓb ℓ = ℓa ⊔ ℓb
open Category ℂ using (Object ; Arrow ; identity ; _∘_) open Category ℂ using (Object ; Arrow ; identity ; _<<<_)
open import Cat.Category.NaturalTransformation ℂ ℂ open import Cat.Category.NaturalTransformation ℂ ℂ
using (NaturalTransformation ; Transformation ; Natural) using (NaturalTransformation ; Transformation ; Natural)
@ -42,19 +42,19 @@ record RawMonad : Set ℓ where
Rfmap = Functor.fmap R Rfmap = Functor.fmap R
bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ] bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ]
bind {X} {Y} f = joinT Y ∘ Rfmap f bind {X} {Y} f = joinT Y <<< Rfmap f
IsAssociative : Set _ IsAssociative : Set _
IsAssociative = {X : Object} IsAssociative = {X : Object}
→ joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X) → joinT X <<< Rfmap (joinT X) ≡ joinT X <<< joinT (Romap X)
IsInverse : Set _ IsInverse : Set _
IsInverse = {X : Object} IsInverse = {X : Object}
→ joinT X ∘ pureT (Romap X) ≡ identity → joinT X <<< pureT (Romap X) ≡ identity
× joinT X ∘ Rfmap (pureT X) ≡ identity × joinT X <<< Rfmap (pureT X) ≡ identity
IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f 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)) IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
→ joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f) → joinT Z <<< Rfmap g <<< (joinT Y <<< Rfmap f)
≡ joinT Z ∘ Rfmap (joinT Z ∘ Rfmap g ∘ f) ≡ joinT Z <<< Rfmap (joinT Z <<< Rfmap g <<< f)
record IsMonad (raw : RawMonad) : Set ℓ where record IsMonad (raw : RawMonad) : Set ℓ where
open RawMonad raw public open RawMonad raw public
@ -68,11 +68,11 @@ record IsMonad (raw : RawMonad) : Set ℓ where
isNatural : IsNatural isNatural : IsNatural
isNatural {X} {Y} f = begin isNatural {X} {Y} f = begin
joinT Y ∘ R.fmap f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩ joinT Y <<< R.fmap f <<< pureT X ≡⟨ sym ℂ.isAssociative ⟩
joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩ 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) ≡⟨ ℂ.isAssociative ⟩
joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (fst isInverse) ⟩ joinT Y <<< pureT (R.omap Y) <<< f ≡⟨ cong (λ φ → φ <<< f) (fst isInverse) ⟩
identity ∘ f ≡⟨ ℂ.leftIdentity ⟩ identity <<< f ≡⟨ ℂ.leftIdentity ⟩
f ∎ f ∎
isDistributive : IsDistributive isDistributive : IsDistributive
@ -80,36 +80,36 @@ record IsMonad (raw : RawMonad) : Set ℓ where
where where
module R² = Functor F[ R ∘ R ] module R² = Functor F[ R ∘ R ]
distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B} distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
→ R.fmap (a ∘ b ∘ c) → R.fmap (a <<< b <<< c)
≡ R.fmap a ∘ R.fmap b ∘ R.fmap c ≡ R.fmap a <<< R.fmap b <<< R.fmap c
distrib3 {a = a} {b} {c} = begin distrib3 {a = a} {b} {c} = begin
R.fmap (a ∘ b ∘ c) ≡⟨ R.isDistributive ⟩ R.fmap (a <<< b <<< c) ≡⟨ R.isDistributive ⟩
R.fmap (a ∘ b) ∘ R.fmap c ≡⟨ cong (_∘ _) R.isDistributive ⟩ R.fmap (a <<< b) <<< R.fmap c ≡⟨ cong (_<<< _) R.isDistributive ⟩
R.fmap a ∘ R.fmap b ∘ R.fmap c ∎ R.fmap a <<< R.fmap b <<< R.fmap c ∎
aux = begin aux = begin
joinT Z ∘ R.fmap (joinT Z ∘ R.fmap g ∘ f) joinT Z <<< R.fmap (joinT Z <<< R.fmap g <<< f)
≡⟨ cong (λ φ → joinT Z ∘ φ) distrib3 ⟩ ≡⟨ cong (λ φ → joinT Z <<< φ) distrib3 ⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ R.fmap (R.fmap g) ∘ R.fmap f) joinT Z <<< (R.fmap (joinT Z) <<< R.fmap (R.fmap g) <<< R.fmap f)
≡⟨⟩ ≡⟨⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ R².fmap g ∘ R.fmap f) joinT Z <<< (R.fmap (joinT Z) <<< R².fmap g <<< R.fmap f)
≡⟨ cong (_∘_ (joinT Z)) (sym ℂ.isAssociative) ⟩ ≡⟨ cong (_<<<_ (joinT Z)) (sym ℂ.isAssociative) ⟩
joinT Z ∘ (R.fmap (joinT Z) ∘ (R².fmap g ∘ R.fmap f)) joinT Z <<< (R.fmap (joinT Z) <<< (R².fmap g <<< R.fmap f))
≡⟨ ℂ.isAssociative ⟩ ≡⟨ ℂ.isAssociative ⟩
(joinT Z ∘ R.fmap (joinT Z)) ∘ (R².fmap g ∘ R.fmap f) (joinT Z <<< R.fmap (joinT Z)) <<< (R².fmap g <<< R.fmap f)
≡⟨ cong (λ φ → φ ∘ (R².fmap g ∘ R.fmap f)) isAssociative ⟩ ≡⟨ cong (λ φ → φ <<< (R².fmap g <<< R.fmap f)) isAssociative ⟩
(joinT Z ∘ joinT (R.omap Z)) ∘ (R².fmap g ∘ R.fmap f) (joinT Z <<< joinT (R.omap Z)) <<< (R².fmap g <<< R.fmap f)
≡⟨ ℂ.isAssociative ⟩ ≡⟨ ℂ.isAssociative ⟩
joinT Z ∘ joinT (R.omap Z) ∘ R².fmap g ∘ R.fmap f joinT Z <<< joinT (R.omap Z) <<< R².fmap g <<< R.fmap f
≡⟨⟩ ≡⟨⟩
((joinT Z ∘ joinT (R.omap Z)) ∘ R².fmap g) ∘ R.fmap f ((joinT Z <<< joinT (R.omap Z)) <<< R².fmap g) <<< R.fmap f
≡⟨ cong (_∘ R.fmap f) (sym ℂ.isAssociative) ⟩ ≡⟨ cong (_<<< R.fmap f) (sym ℂ.isAssociative) ⟩
(joinT Z ∘ (joinT (R.omap Z) ∘ R².fmap g)) ∘ R.fmap f (joinT Z <<< (joinT (R.omap Z) <<< R².fmap g)) <<< R.fmap f
≡⟨ cong (λ φ → φ ∘ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩ ≡⟨ cong (λ φ → φ <<< R.fmap f) (cong (_<<<_ (joinT Z)) (joinN g)) ⟩
(joinT Z ∘ (R.fmap g ∘ joinT Y)) ∘ R.fmap f (joinT Z <<< (R.fmap g <<< joinT Y)) <<< R.fmap f
≡⟨ cong (_∘ R.fmap f) ℂ.isAssociative ⟩ ≡⟨ cong (_<<< R.fmap f) ℂ.isAssociative ⟩
joinT Z ∘ R.fmap g ∘ joinT Y ∘ R.fmap f joinT Z <<< R.fmap g <<< joinT Y <<< R.fmap f
≡⟨ sym (Category.isAssociative ℂ) ⟩ ≡⟨ sym (Category.isAssociative ℂ) ⟩
joinT Z ∘ R.fmap g ∘ (joinT Y ∘ R.fmap f) joinT Z <<< R.fmap g <<< (joinT Y <<< R.fmap f)
∎ ∎
record Monad : Set ℓ where record Monad : Set ℓ where

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

@ -105,8 +105,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
× ℂ [ y1 ∘ f ] ≡ x1 × ℂ [ y1 ∘ f ] ≡ x1
} }
; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity} ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity}
; _∘_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
→ (f ℂ.∘ g) → (f ℂ.<<< g)
, (begin , (begin
ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩
ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩ ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩
@ -134,9 +134,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i
= s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i
where where
l = hh ∘ (gg ∘ ff) l = hh <<< (gg <<< ff)
r = hh ∘ gg ∘ ff r = hh <<< gg <<< ff
-- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f -- s0 : h ℂ.<<< (g ℂ.<<< f) ≡ h ℂ.<<< g ℂ.<<< f
s0 : fst l ≡ fst r s0 : fst l ≡ fst r
s0 = ℂ.isAssociative {f = f} {g} {h} s0 = ℂ.isAssociative {f = f} {g} {h}
@ -144,18 +144,18 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
isIdentity : IsIdentity identity isIdentity : IsIdentity identity
isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
where where
leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1) leftIdentity : identity <<< (f , f0 , f1) ≡ (f , f0 , f1)
leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
where where
L = identity ∘ (f , f0 , f1) L = identity <<< (f , f0 , f1)
R : Arrow AA BB R : Arrow AA BB
R = f , f0 , f1 R = f , f0 , f1
l : fst L ≡ fst R l : fst L ≡ fst R
l = ℂ.leftIdentity l = ℂ.leftIdentity
rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1) rightIdentity : (f , f0 , f1) <<< identity ≡ (f , f0 , f1)
rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
where where
L = (f , f0 , f1) ∘ identity L = (f , f0 , f1) <<< identity
R : Arrow AA BB R : Arrow AA BB
R = (f , f0 , f1) R = (f , f0 , f1)
l : ℂ [ f ∘ ℂ.identity ] ≡ f l : ℂ [ f ∘ ℂ.identity ] ≡ f