Skip to content

Commit c96e085

Browse files
JacquesCaretteJacquesCarette
authoredFeb 18, 2021
Merge pull request #248 from TOTBWF/spans-bicategory
Show that Monads in Span(Setoid) are categories
·
v0.2.0v0.1.6
2 parents 1ba82d9 + 462899f commit c96e085

File tree

4 files changed

+315
-0
lines changed

4 files changed

+315
-0
lines changed
 

‎src/Categories/Bicategory/Construction/Spans/Properties.agda

+133
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
module Categories.Bicategory.Construction.Spans.Properties where
4+
5+
open import Level
6+
7+
open import Data.Product using (_,_; _×_)
8+
open import Relation.Binary.Bundles using (Setoid)
9+
import Relation.Binary.Reasoning.Setoid as SR
10+
open import Function.Equality as SΠ renaming (id to ⟶-id)
11+
12+
open import Categories.Category
13+
open import Categories.Category.Helper
14+
open import Categories.Category.Instance.Setoids
15+
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
16+
17+
open import Categories.Diagram.Pullback
18+
19+
open import Categories.Bicategory
20+
open import Categories.Bicategory.Monad
21+
22+
import Categories.Category.Diagram.Span as Span
23+
import Categories.Bicategory.Construction.Spans as Spans
24+
25+
--------------------------------------------------------------------------------
26+
-- Monads in the Bicategory of Spans are Categories
27+
28+
module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where
29+
30+
private
31+
module T = Monad T
32+
33+
open Span (Setoids (o ⊔ ℓ) ℓ)
34+
open Spans (pullback o ℓ)
35+
open Span⇒
36+
open Bicategory Spans
37+
38+
open Setoid renaming (_≈_ to [_][_≈_])
39+
40+
41+
-- We can view the roof of the span as a hom set! However, we need to partition
42+
-- this big set up into small chunks with known domains/codomains.
43+
record Hom (X Y : Carrier T.C) : Set (o ⊔ ℓ) where
44+
field
45+
hom : Carrier (Span.M T.T)
46+
dom-eq : [ T.C ][ Span.dom T.T ⟨$⟩ hom ≈ X ]
47+
cod-eq : [ T.C ][ Span.cod T.T ⟨$⟩ hom ≈ Y ]
48+
49+
open Hom
50+
51+
private
52+
ObjSetoid : Setoid (o ⊔ ℓ) ℓ
53+
ObjSetoid = T.C
54+
55+
HomSetoid : Setoid (o ⊔ ℓ) ℓ
56+
HomSetoid = Span.M T.T
57+
58+
module ObjSetoid = Setoid ObjSetoid
59+
module HomSetoid = Setoid HomSetoid
60+
61+
id⇒ : (X : Carrier T.C) → Hom X X
62+
id⇒ X = record
63+
{ hom = arr T.η ⟨$⟩ X
64+
; dom-eq = commute-dom T.η (refl T.C)
65+
; cod-eq = commute-cod T.η (refl T.C)
66+
}
67+
68+
_×ₚ_ : ∀ {A B C} → (f : Hom B C) → (g : Hom A B) → FiberProduct (Span.cod T.T) (Span.dom T.T)
69+
_×ₚ_ {B = B} f g = record
70+
{ elem₁ = hom g
71+
; elem₂ = hom f
72+
; commute = begin
73+
Span.cod T.T ⟨$⟩ hom g ≈⟨ cod-eq g ⟩
74+
B ≈⟨ ObjSetoid.sym (dom-eq f) ⟩
75+
Span.dom T.T ⟨$⟩ hom f ∎
76+
}
77+
where
78+
open SR ObjSetoid
79+
80+
_∘⇒_ : ∀ {A B C} (f : Hom B C) → (g : Hom A B) → Hom A C
81+
_∘⇒_ {A = A} {C = C} f g = record
82+
{ hom = arr T.μ ⟨$⟩ (f ×ₚ g)
83+
; dom-eq = begin
84+
Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ (commute-dom T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl)) ⟩
85+
Span.dom T.T ⟨$⟩ hom g ≈⟨ dom-eq g ⟩
86+
A ∎
87+
; cod-eq = begin
88+
Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl) ⟩
89+
Span.cod T.T ⟨$⟩ hom f ≈⟨ cod-eq f ⟩
90+
C ∎
91+
}
92+
where
93+
open SR ObjSetoid
94+
95+
SpanMonad⇒Category : Category (o ⊔ ℓ) (o ⊔ ℓ) ℓ
96+
SpanMonad⇒Category = categoryHelper record
97+
{ Obj = Setoid.Carrier T.C
98+
; _⇒_ = Hom
99+
; _≈_ = λ f g → [ HomSetoid ][ hom f ≈ hom g ]
100+
; id = λ {X} → id⇒ X
101+
; _∘_ = _∘⇒_
102+
; assoc = λ {A} {B} {C} {D} {f} {g} {h} →
103+
let f×ₚ⟨g×ₚh⟩ = record
104+
{ elem₁ = record
105+
{ elem₁ = hom f
106+
; elem₂ = hom g
107+
; commute = FiberProduct.commute (g ×ₚ f)
108+
}
109+
; elem₂ = hom h
110+
; commute = FiberProduct.commute (h ×ₚ g)
111+
}
112+
in begin
113+
arr T.μ ⟨$⟩ ((h ∘⇒ g) ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl)) ⟩
114+
arr T.μ ⟨$⟩ _ ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} {f×ₚ⟨g×ₚh⟩} ((HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl) ⟩
115+
arr T.μ ⟨$⟩ _ ≈⟨ (cong (arr T.μ) (cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl)) ⟩
116+
arr T.μ ⟨$⟩ (h ×ₚ (g ∘⇒ f)) ∎
117+
; identityˡ = λ {A} {B} {f} → begin
118+
arr T.μ ⟨$⟩ (id⇒ B ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.η) (ObjSetoid.sym (cod-eq f))) ⟩
119+
arr T.μ ⟨$⟩ _ ≈⟨ T.identityʳ HomSetoid.refl ⟩
120+
hom f ∎
121+
; identityʳ = λ {A} {B} {f} → begin
122+
arr T.μ ⟨$⟩ (f ×ₚ id⇒ A) ≈⟨ cong (arr T.μ) (cong (arr T.η) (ObjSetoid.sym (dom-eq f)) , HomSetoid.refl) ⟩
123+
arr T.μ ⟨$⟩ _ ≈⟨ T.identityˡ HomSetoid.refl ⟩
124+
hom f ∎
125+
; equiv = record
126+
{ refl = HomSetoid.refl
127+
; sym = HomSetoid.sym
128+
; trans = HomSetoid.trans
129+
}
130+
; ∘-resp-≈ = λ f≈h g≈i → cong (arr T.μ) (g≈i , f≈h)
131+
}
132+
where
133+
open SR HomSetoid

‎src/Categories/Bicategory/Monad.agda

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
-- A Monad in a Bicategory.
4+
-- For the more elementary version of Monads, see 'Categories.Monad'.
5+
module Categories.Bicategory.Monad where
6+
7+
open import Level
8+
open import Data.Product using (_,_)
9+
10+
open import Categories.Bicategory
11+
import Categories.Bicategory.Extras as Bicat
12+
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
13+
14+
15+
record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
16+
open Bicat 𝒞
17+
18+
field
19+
C : Obj
20+
T : C ⇒₁ C
21+
η : id₁ ⇒₂ T
22+
μ : (T ⊚₀ T) ⇒₂ T
23+
24+
assoc : μ ∘ᵥ (T ▷ μ) ∘ᵥ associator.from ≈ (μ ∘ᵥ (μ ◁ T))
25+
sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ associator.to ≈ (μ ∘ᵥ (T ▷ μ))
26+
identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitorʳ.to ≈ id₂
27+
identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitorˡ.to ≈ id₂

‎src/Categories/Bicategory/Monad/Properties.agda

+93
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
module Categories.Bicategory.Monad.Properties where
3+
4+
open import Categories.Category
5+
open import Categories.Bicategory.Instance.Cats
6+
open import Categories.NaturalTransformation using (NaturalTransformation)
7+
open import Categories.Functor using (Functor)
8+
9+
import Categories.Bicategory.Monad as BicatMonad
10+
import Categories.Monad as ElemMonad
11+
12+
import Categories.Morphism.Reasoning as MR
13+
14+
--------------------------------------------------------------------------------
15+
-- Bicategorical Monads in Cat are the same as the more elementary
16+
-- definition of Monads.
17+
18+
CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T)
19+
CatMonad⇒Monad T = record
20+
{ F = T.T
21+
; η = T.η
22+
; μ = T.μ
23+
; assoc = λ {X} → begin
24+
η T.μ X ∘ F₁ T.T (η T.μ X) ≈⟨ intro-ids ⟩
25+
(η T.μ X ∘ (F₁ T.T (η T.μ X) ∘ id) ∘ id) ≈⟨ T.assoc ⟩
26+
(η T.μ X ∘ F₁ T.T id ∘ η T.μ (F₀ T.T X)) ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ˡ (identity T.T) ○ identityˡ) ⟩
27+
η T.μ X ∘ η T.μ (F₀ T.T X) ∎
28+
; sym-assoc = λ {X} → begin
29+
η T.μ X ∘ η T.μ (F₀ T.T X) ≈⟨ intro-F-ids ⟩
30+
η T.μ X ∘ (F₁ T.T id ∘ η T.μ (F₀ T.T X)) ∘ id ≈⟨ T.sym-assoc ⟩
31+
η T.μ X ∘ F₁ T.T (η T.μ X) ∘ id ≈⟨ ∘-resp-≈ʳ identityʳ ⟩
32+
η T.μ X ∘ F₁ T.T (η T.μ X) ∎
33+
; identityˡ = λ {X} → begin
34+
η T.μ X ∘ F₁ T.T (η T.η X) ≈⟨ intro-ids ⟩
35+
η T.μ X ∘ (F₁ T.T (η T.η X) ∘ id) ∘ id ≈⟨ T.identityˡ ⟩
36+
id ∎
37+
; identityʳ = λ {X} → begin
38+
η T.μ X ∘ η T.η (F₀ T.T X) ≈⟨ intro-F-ids ⟩
39+
η T.μ X ∘ (F₁ T.T id ∘ η T.η (F₀ T.T X)) ∘ id ≈⟨ T.identityʳ ⟩
40+
id ∎
41+
}
42+
where
43+
module T = BicatMonad.Monad T
44+
open Category (BicatMonad.Monad.C T)
45+
open HomReasoning
46+
open Equiv
47+
open MR (BicatMonad.Monad.C T)
48+
49+
open NaturalTransformation
50+
open Functor
51+
52+
intro-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ g ≈ f ∘ (g ∘ id) ∘ id
53+
intro-ids = ⟺ (∘-resp-≈ʳ identityʳ) ○ ⟺ (∘-resp-≈ʳ identityʳ)
54+
55+
intro-F-ids : ∀ {X Y Z} {f : F₀ T.T Y ⇒ Z} {g : X ⇒ F₀ T.T Y} → f ∘ g ≈ f ∘ (F₁ T.T id ∘ g) ∘ id
56+
intro-F-ids = ∘-resp-≈ʳ (⟺ identityˡ ○ ⟺ (∘-resp-≈ˡ (identity T.T))) ○ ⟺ (∘-resp-≈ʳ identityʳ)
57+
58+
Monad⇒CatMonad : ∀ {o ℓ e} {𝒞 : Category o ℓ e} → (T : ElemMonad.Monad 𝒞) → BicatMonad.Monad (Cats o ℓ e)
59+
Monad⇒CatMonad {𝒞 = 𝒞} T = record
60+
{ C = 𝒞
61+
; T = T.F
62+
; η = T.η
63+
; μ = T.μ
64+
; assoc = λ {X} → begin
65+
T.μ.η X ∘ (T.F.F₁ (T.μ.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
66+
T.μ.η X ∘ T.F.F₁ (T.μ.η X) ≈⟨ T.assoc ⟩
67+
T.μ.η X ∘ T.μ.η (T.F.F₀ X) ≈⟨ ∘-resp-≈ʳ (⟺ identityˡ ○ ∘-resp-≈ˡ (⟺ T.F.identity)) ⟩
68+
T.μ.η X ∘ T.F.F₁ id ∘ T.μ.η (T.F.F₀ X) ∎
69+
; sym-assoc = λ {X} → begin
70+
T.μ.η X ∘ (T.F.F₁ id ∘ T.μ.η (T.F.F₀ X)) ∘ id ≈⟨ eliminate-F-ids ⟩
71+
T.μ.η X ∘ T.μ.η (T.F.F₀ X) ≈⟨ T.sym-assoc ⟩
72+
T.μ.η X ∘ T.F.F₁ (T.μ.η X) ≈⟨ ∘-resp-≈ʳ (⟺ identityʳ) ⟩
73+
T.μ.η X ∘ T.F.F₁ (T.μ.η X) ∘ id ∎
74+
; identityˡ = λ {X} → begin
75+
T.μ.η X ∘ (T.F.F₁ (T.η.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
76+
T.μ.η X ∘ T.F.F₁ (T.η.η X) ≈⟨ T.identityˡ ⟩
77+
id ∎
78+
; identityʳ = λ {X} → begin
79+
(T.μ.η X ∘ (T.F.F₁ id ∘ T.η.η (T.F.F₀ X)) ∘ id) ≈⟨ eliminate-F-ids ⟩
80+
T.μ.η X ∘ T.η.η (T.F.F₀ X) ≈⟨ T.identityʳ ⟩
81+
id ∎
82+
}
83+
where
84+
module T = ElemMonad.Monad T
85+
open Category 𝒞
86+
open HomReasoning
87+
open MR 𝒞
88+
89+
eliminate-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ (g ∘ id) ∘ id ≈ f ∘ g
90+
eliminate-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ identityʳ
91+
92+
eliminate-F-ids : ∀ {X Y Z} {f : T.F.F₀ Y ⇒ Z} {g : X ⇒ T.F.F₀ Y} → f ∘ (T.F.F₁ id ∘ g) ∘ id ≈ f ∘ g
93+
eliminate-F-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ (∘-resp-≈ˡ T.F.identity ○ identityˡ)

‎src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda

+62
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
-- A "canonical" presentation of limits in Setoid.
4+
--
5+
-- These limits are obviously isomorphic to those created by
6+
-- the Completeness proof, but are far less unweildy to work with.
7+
-- This isomorphism is witnessed by Categories.Diagram.Pullback.up-to-iso
8+
9+
module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where
10+
11+
open import Level
12+
13+
open import Data.Product using (_,_; _×_)
14+
15+
open import Relation.Binary.Bundles using (Setoid)
16+
open import Function.Equality as SΠ renaming (id to ⟶-id)
17+
import Relation.Binary.Reasoning.Setoid as SR
18+
19+
open import Categories.Diagram.Pullback
20+
21+
open import Categories.Category.Instance.Setoids
22+
23+
open Setoid renaming (_≈_ to [_][_≈_])
24+
25+
--------------------------------------------------------------------------------
26+
-- Pullbacks
27+
28+
record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where
29+
field
30+
elem₁ : Carrier X
31+
elem₂ : Carrier Y
32+
commute : [ Z ][ f ⟨$⟩ elem₁ ≈ g ⟨$⟩ elem₂ ]
33+
34+
open FiberProduct
35+
36+
pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
37+
pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
38+
{ P = record
39+
{ Carrier = FiberProduct f g
40+
; _≈_ = λ p q → [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ]
41+
; isEquivalence = record
42+
{ refl = (refl X) , (refl Y)
43+
; sym = λ (eq₁ , eq₂) → sym X eq₁ , sym Y eq₂
44+
; trans = λ (eq₁ , eq₂) (eq₁′ , eq₂′) → (trans X eq₁ eq₁′) , (trans Y eq₂ eq₂′)
45+
}
46+
}
47+
; p₁ = record { _⟨$⟩_ = elem₁ ; cong = λ (eq₁ , _) → eq₁ }
48+
; p₂ = record { _⟨$⟩_ = elem₂ ; cong = λ (_ , eq₂) → eq₂ }
49+
; isPullback = record
50+
{ commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q)
51+
; universal = λ {A} {h₁} {h₂} eq → record
52+
{ _⟨$⟩_ = λ a → record
53+
{ elem₁ = h₁ ⟨$⟩ a
54+
; elem₂ = h₂ ⟨$⟩ a
55+
; commute = eq (refl A)
56+
}
57+
; cong = λ eq → cong h₁ eq , cong h₂ eq }
58+
; unique = λ eq₁ eq₂ x≈y → eq₁ x≈y , eq₂ x≈y
59+
; p₁∘universal≈h₁ = λ {_} {h₁} {_} eq → cong h₁ eq
60+
; p₂∘universal≈h₂ = λ {_} {_} {h₂} eq → cong h₂ eq
61+
}
62+
}

0 commit comments

Comments
 (0)
Please sign in to comment.