open import SOAS.Common
module SOAS.Construction.Free {β π : Category 1β 0β 0β}
(U : Functor π β) where
open import Categories.Adjoint
import Categories.Morphism.Reasoning as MR
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
open import Categories.Adjoint.Properties
open import Categories.Monad
private module β = Category β
private module π = Category π
private module U = Functor U
_βͺ_ : β.Obj β π.Obj β Set
C βͺ S = β [ C , U.β S ]
record FreeConstruction (F : β.Obj β π.Obj)
(C : β.Obj)
(embed : C βͺ F C)
(S : π.Obj)
(c : C βͺ S)
: Setβ where
field
extend : π [ F C , S ]
factor : U.β extend β.β embed β.β c
unique : (e : π [ F C , S ])
β (p : (U.β e β.β embed) β.β c)
β π [ e β extend ]
record FreeMapping (F : β.Obj β π.Obj) : Setβ where
field
embed : {C : β.Obj} β C βͺ F C
univ : (C : β.Obj) (S : π.Obj)(c : C βͺ S)
β FreeConstruction F C embed S c
module Universal C S c = FreeConstruction (univ C S c)
module _ {C : β.Obj} {S : π.Obj}(c : C βͺ S) where
open Universal C S c public
open MR β
open β.HomReasoning
private module πR = π.HomReasoning
open NT
equate : {C : β.Obj}{S : π.Obj}
β (f g : π [ F C , S ])
β (p : U.β f β.β embed β.β U.β g β.β embed)
β π [ f β g ]
equate f g p = unique _ f p πR.β πR.βΊ (unique _ g β.Equiv.refl)
[_β_]! : {C : β.Obj}{S : π.Obj}
β (f g : π [ F C , S ])
β (p : U.β f β.β embed β.β U.β g β.β embed)
β π [ f β g ]
[ f β g ]! p = equate f g p
extend-cong : {C : β.Obj}{S : π.Obj}(cβ cβ : C βͺ S)
β β [ cβ β cβ ] β π [ extend cβ β extend cβ ]
extend-cong {C}{S} cβ cβ p = unique _ (extend cβ) (factor cβ β p)
map : {C D : β.Obj} β C β.β D β F C π.β F D
map {C}{D} f = extend (embed β.β f)
embed-commute : {C D : β.Obj}(f : C β.β D)
β embed β.β f β.β (U.β (map f) β.β embed)
embed-commute {C}{D} f = βΊ (factor (embed β.β f))
identity : {C : β.Obj} β map (β.id {C}) π.β π.id
identity {C} = πR.βΊ $αΆ unique _ π.id (begin
U.β π.id β.β embed ββ¨ U.identity β©ββ¨refl β©
β.id β.β embed ββ¨ id-comm-sym β©
embed β.β β.id β)
homomorphism : {C D E : β.Obj} {f : β [ C , D ]} {g : β [ D , E ]}
β π [ map (β [ g β f ])
β π [ map g β map f ] ]
homomorphism {C}{D}{E}{f}{g} = πR.βΊ $αΆ unique _ (π [ map g β map f ]) (begin
U.β (map g π.β map f) β.β embed ββ¨ pushΛ‘ U.homomorphism β©
U.β (map g) β.β U.β (map f) β.β embed ββ¨ pushΚ³ (βΊ (embed-commute f)) β©
(U.β (map g) β.β embed) β.β f ββ¨ pushΛ‘ (βΊ (embed-commute g)) β©
embed β.β g β.β f β)
Free : Functor β π
Free = record
{ Fβ = F
; Fβ = map
; identity = identity
; homomorphism = homomorphism
; F-resp-β = Ξ» {C}{D}{f}{g} p β
extend-cong (embed β.β f) (embed β.β g) (β.β-resp-βΚ³ p)
}
module F = Functor Free
embed-NT : NT idF (U βF Free)
embed-NT = ntHelper record
{ Ξ· = Ξ» C β embed
; commute = embed-commute
}
extract : (S : π.Obj) β F (U.β S) π.β S
extract S = extend β.id
extract-NT : NT (Free βF U) idF
extract-NT = ntHelper record
{ Ξ· = extract
; commute = Ξ» {S}{T} f β [ extract T π.β F.β (U.β f) β f π.β extract S ]!
(begin
U.β (extract T π.β F.β (U.β f)) β.β embed
ββ¨ pushΛ‘ U.homomorphism β©
U.β (extract T) β.β U.β (F.β (U.β f)) β.β embed
ββ¨ reflβ©ββ¨ sym-commute embed-NT (U.β f) β©
U.β (extract T) β.β embed β.β U.β f
ββ¨ pullΛ‘ (factor β.id) β β.identityΛ‘ β©
U.β f
βΛβ¨ (reflβ©ββ¨ factor β.id) β β.identityΚ³ β©
U.β f β.β U.β (extract S) β.β embed
βΛβ¨ pushΛ‘ U.homomorphism β©
U.β (f π.β extract S) β.β embed
β)
}
Freeβ£Forgetful : Free β£ U
Freeβ£Forgetful = record
{ unit = embed-NT
; counit = extract-NT
; zig = Ξ» {C} β [ extract (F.β C) π.β F.β embed β π.id ]!
(begin
U.β (extract (F.β C) π.β F.β embed) β.β embed
ββ¨ pushΛ‘ U.homomorphism β©
U.β (extract (F.β C)) β.β U.β (F.β embed) β.β embed
ββ¨ reflβ©ββ¨ (sym-commute embed-NT embed) β©
U.β (extract (F.β C)) β.β (embed β.β embed)
ββ¨ pullΛ‘ (factor (β.id)) β©
β.id β.β embed
βΛβ¨ U.identity β©ββ¨refl β©
U.β π.id β.β embed
β)
; zag = factor β.id
}
FreeMonad : Monad β
FreeMonad = adjointβmonad Freeβ£Forgetful