The universal property of lists with respect to wild monoids
module lists.universal-property-lists-wild-monoids where
Imports
open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.unit-type open import foundation.universe-levels open import group-theory.homomorphisms-semigroups open import lists.concatenation-lists open import lists.lists open import structured-types.coherent-h-spaces open import structured-types.morphisms-coherent-h-spaces open import structured-types.wild-monoids
Idea
The type of lists of elements of X is the initial wild monoid equipped with a
map from X into it.
Definition
The wild unital magma of lists of elements of X
list-Coherent-H-Space : {l : Level} (X : UU l) → Coherent-H-Space l list-Coherent-H-Space X = pair ( pair (list X) nil) ( pair ( concat-list) ( pair ( left-unit-law-concat-list) ( pair right-unit-law-concat-list refl)))
The wild monoid of lists of elements of X
unit-law-011-associative-concat-list : {l1 : Level} {X : UU l1} (y z : list X) → Id ( ( associative-concat-list nil y z) ∙ ( left-unit-law-concat-list (concat-list y z))) ( ap (λ t → concat-list t z) (left-unit-law-concat-list y)) unit-law-011-associative-concat-list y z = refl concat-list' : {l : Level} {A : UU l} → list A → list A → list A concat-list' x y = concat-list y x unit-law-101-associative-concat-list : {l1 : Level} {X : UU l1} (x z : list X) → Id ( ( associative-concat-list x nil z) ∙ ( ap (concat-list x) (left-unit-law-concat-list z))) ( ap (λ t → concat-list t z) (right-unit-law-concat-list x)) unit-law-101-associative-concat-list nil z = refl unit-law-101-associative-concat-list (cons x l) z = ( ( ( inv ( ap-concat ( cons x) ( associative-concat-list l nil z) ( ap (concat-list l) (left-unit-law-concat-list z)))) ∙ ( ap (ap (cons x)) (unit-law-101-associative-concat-list l z))) ∙ ( inv ( ap-comp (cons x) (concat-list' z) (right-unit-law-concat-list l)))) ∙ ( ap-comp (concat-list' z) (cons x) (right-unit-law-concat-list l)) unit-law-110-associative-concat-list : {l1 : Level} {X : UU l1} (x y : list X) → Id ( ( associative-concat-list x y nil) ∙ ( ap (concat-list x) (right-unit-law-concat-list y))) ( right-unit-law-concat-list (concat-list x y)) unit-law-110-associative-concat-list nil y = ap-id (right-unit-law-concat-list y) unit-law-110-associative-concat-list (cons a x) y = ( ap ( concat ( associative-concat-list (cons a x) y nil) ( concat-list (cons a x) y)) ( ap-comp (cons a) (concat-list x) (right-unit-law-concat-list y))) ∙ ( ( inv ( ap-concat ( cons a) ( associative-concat-list x y nil) ( ap (concat-list x) (right-unit-law-concat-list y)))) ∙ ( ap (ap (cons a)) (unit-law-110-associative-concat-list x y))) list-Wild-Monoid : {l : Level} → UU l → Wild-Monoid l list-Wild-Monoid X = pair ( list-Coherent-H-Space X) ( pair ( associative-concat-list) ( pair ( unit-law-011-associative-concat-list) ( pair ( unit-law-101-associative-concat-list) ( pair unit-law-110-associative-concat-list star))))
Properties
For any wild monoid M with a map X → M there is a morphism of wild monoids list X → M
module _ {l1 l2 : Level} {X : UU l1} (M : Wild-Monoid l2) (f : X → type-Wild-Monoid M) where map-elim-list-Wild-Monoid : list X → type-Wild-Monoid M map-elim-list-Wild-Monoid nil = unit-Wild-Monoid M map-elim-list-Wild-Monoid (cons u x) = mul-Wild-Monoid M (f u) (map-elim-list-Wild-Monoid x) preserves-unit-map-elim-list-Wild-Monoid : Id (map-elim-list-Wild-Monoid nil) (unit-Wild-Monoid M) preserves-unit-map-elim-list-Wild-Monoid = refl preserves-mul-map-elim-list-Wild-Monoid : preserves-mul ( concat-list) ( mul-Wild-Monoid M) ( map-elim-list-Wild-Monoid) preserves-mul-map-elim-list-Wild-Monoid nil y = inv (left-unit-law-mul-Wild-Monoid M (map-elim-list-Wild-Monoid y)) preserves-mul-map-elim-list-Wild-Monoid (cons u x) y = ( ap (mul-Wild-Monoid M (f u)) ( preserves-mul-map-elim-list-Wild-Monoid x y)) ∙ ( inv ( associative-mul-Wild-Monoid M ( f u) ( map-elim-list-Wild-Monoid x) ( map-elim-list-Wild-Monoid y))) preserves-left-unit-law-map-elim-list-Wild-Monoid : preserves-left-unit-law-mul ( concat-list) { nil} ( left-unit-law-concat-list) ( mul-Wild-Monoid M) ( left-unit-law-mul-Wild-Monoid M) ( map-elim-list-Wild-Monoid) ( preserves-unit-map-elim-list-Wild-Monoid) ( preserves-mul-map-elim-list-Wild-Monoid) preserves-left-unit-law-map-elim-list-Wild-Monoid x = inv ( left-inv ( left-unit-law-mul-Wild-Monoid M (map-elim-list-Wild-Monoid x))) preserves-right-unit-law-map-elim-list-Wild-Monoid : preserves-right-unit-law-mul ( concat-list) { nil} ( right-unit-law-concat-list) ( mul-Wild-Monoid M) ( right-unit-law-mul-Wild-Monoid M) ( map-elim-list-Wild-Monoid) ( preserves-unit-map-elim-list-Wild-Monoid) ( preserves-mul-map-elim-list-Wild-Monoid) preserves-right-unit-law-map-elim-list-Wild-Monoid nil = ( inv (left-inv (left-unit-law-mul-Wild-Monoid M (unit-Wild-Monoid M)))) ∙ ( ap ( concat ( inv (left-unit-law-mul-Wild-Monoid M (unit-Wild-Monoid M))) ( unit-Wild-Monoid M)) ( coh-unit-laws-mul-Wild-Monoid M)) preserves-right-unit-law-map-elim-list-Wild-Monoid (cons a x) = ( inv ( ap-comp ( map-elim-list-Wild-Monoid) ( cons a) ( right-unit-law-concat-list x))) ∙ ( ( ap-comp ( mul-Wild-Monoid M (f a)) ( map-elim-list-Wild-Monoid) ( right-unit-law-concat-list x)) ∙ ( ( ap ( ap (mul-Wild-Monoid M (f a))) ( preserves-right-unit-law-map-elim-list-Wild-Monoid x)) ∙ ( ( ap-concat ( mul-Wild-Monoid M (f a)) ( preserves-mul-map-elim-list-Wild-Monoid x nil) ( right-unit-law-mul-Wild-Monoid M ( map-elim-list-Wild-Monoid x))) ∙ ( ( ap ( concat ( ap ( mul-Wild-Monoid M (f a)) ( preserves-mul-map-elim-list-Wild-Monoid x nil)) ( map-elim-list-Wild-Monoid (cons a x))) ( ( ap ( concat' ( mul-Wild-Monoid M ( f a) ( mul-Wild-Monoid M ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M))) ( ap ( mul-Wild-Monoid M (f a)) ( right-unit-law-mul-Wild-Monoid M ( map-elim-list-Wild-Monoid x)))) ( inv ( left-inv ( associative-mul-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M))))) ∙ ( ( assoc ( inv ( associative-mul-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M))) ( associative-mul-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M)) ( ap ( mul-Wild-Monoid M (f a)) ( right-unit-law-mul-Wild-Monoid M ( map-elim-list-Wild-Monoid x)))) ∙ ( ap ( concat ( inv ( associative-mul-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M))) ( map-elim-list-Wild-Monoid (cons a x))) ( unit-law-110-associative-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x)))))) ∙ ( inv ( assoc ( ap ( mul-Wild-Monoid M (f a)) ( preserves-mul-map-elim-list-Wild-Monoid x nil)) ( inv ( associative-mul-Wild-Monoid M ( f a) ( map-elim-list-Wild-Monoid x) ( unit-Wild-Monoid M))) ( right-unit-law-mul-Wild-Monoid M ( map-elim-list-Wild-Monoid (cons a x))))))))) preserves-coh-unit-laws-map-elim-list-Wild-Monoid : {l1 l2 : Level} {X : UU l1} (M : Wild-Monoid l2) (f : X → type-Wild-Monoid M) → preserves-coh-unit-laws-mul ( list-Coherent-H-Space X) ( wild-unital-magma-Wild-Monoid M) ( pair (map-elim-list-Wild-Monoid M f) refl) ( preserves-mul-map-elim-list-Wild-Monoid M f) ( preserves-left-unit-law-map-elim-list-Wild-Monoid M f) ( preserves-right-unit-law-map-elim-list-Wild-Monoid M f) preserves-coh-unit-laws-map-elim-list-Wild-Monoid (pair (pair (pair M eM) (pair μ (pair lM (pair rM cM)))) αM) f = refl elim-list-Wild-Monoid : {l1 l2 : Level} {X : UU l1} (M : Wild-Monoid l2) (f : X → type-Wild-Monoid M) → hom-Wild-Monoid (list-Wild-Monoid X) M elim-list-Wild-Monoid M f = pair ( pair (map-elim-list-Wild-Monoid M f) refl) ( pair ( preserves-mul-map-elim-list-Wild-Monoid M f) ( pair (preserves-left-unit-law-map-elim-list-Wild-Monoid M f) ( pair ( preserves-right-unit-law-map-elim-list-Wild-Monoid M f) ( preserves-coh-unit-laws-map-elim-list-Wild-Monoid M f))))
Contractibility of the type hom (list X) M of morphisms of wild monoids
-- htpy-elim-list-Wild-Monoid : -- {l1 l2 : Level} {X : UU l1} (M : Wild-Monoid l2) -- (g h : hom-Wild-Monoid (list-Wild-Monoid X) M) -- ( H : ( map-hom-Wild-Monoid (list-Wild-Monoid X) M g ∘ unit-list) ~ -- ( map-hom-Wild-Monoid (list-Wild-Monoid X) M h ∘ unit-list)) → -- htpy-hom-Wild-Monoid (list-Wild-Monoid X) M g h -- htpy-elim-list-Wild-Monoid {X = X} M g h H = -- pair (pair α β) γ -- where -- α : pr1 (pr1 g) ~ pr1 (pr1 h) -- α nil = -- ( preserves-unit-map-hom-Wild-Monoid (list-Wild-Monoid X) M g) ∙ -- ( inv (preserves-unit-map-hom-Wild-Monoid (list-Wild-Monoid X) M h)) -- α (cons x l) = -- ( preserves-mul-map-hom-Wild-Monoid -- ( list-Wild-Monoid X) -- ( M) -- ( g) -- ( unit-list x) -- ( l)) ∙ -- ( ( ap-mul-Wild-Monoid M (H x) (α l)) ∙ -- ( inv -- ( preserves-mul-map-hom-Wild-Monoid -- ( list-Wild-Monoid X) -- ( M) -- ( h) -- ( unit-list x) -- ( l)))) -- β : (x y : pr1 (pr1 (list-Wild-Monoid X))) → -- Id ( pr2 (pr1 g) x y ∙ ap-mul-Wild-Monoid M (α x) (α y)) -- ( α (concat-list x y) ∙ pr2 (pr1 h) x y) -- β nil y = {!!} -- β (cons x x₁) y = {!!} -- γ : Id (pr2 g) (α nil ∙ pr2 h) -- γ = -- ( inv right-unit) ∙ -- ( ( ap (concat (pr2 g) (pr1 (pr2 M))) (inv (left-inv (pr2 h)))) ∙ -- ( inv (assoc (pr2 g) (inv (pr2 h)) (pr2 h))))