Free magmas

src/foundation.lagda.md

@@ -14,6 +14,7 @@ open import foundation.0-images-of-maps public
 open import foundation.0-maps public
 open import foundation.1-types public
 open import foundation.2-types public
+open import foundation.action-on-binary-homotopies-binary-functions public
 open import foundation.action-on-equivalences-functions public
 open import foundation.action-on-equivalences-functions-out-of-subuniverses public
 open import foundation.action-on-equivalences-type-families public
@@ -448,6 +449,7 @@ open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
+open import foundation.transport-along-identifications-dependent-functions public
 open import foundation.transport-split-type-families public
 open import foundation.transposition-identifications-along-equivalences public
 open import foundation.transposition-identifications-along-retractions public

src/foundation/action-on-binary-homotopies-binary-functions.lagda.md

@@ -0,0 +1,36 @@
+# The action on binary homotopies
+
+```agda
+module foundation.action-on-binary-homotopies-binary-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.function-extensionality
+open import foundation.homotopy-induction
+open import foundation.universe-levels
+
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Definition
+
+```agda
+ap-binary-htpy :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {f g : A → B} (H : f ~ g) (m : B → B → C)
+  {x y : A} →
+  ap-binary m (H x) (H y) ＝ ap (λ f → m (f x) (f y)) (eq-htpy H)
+ap-binary-htpy {f = f} H m {x = x} {y = y} =
+  ind-htpy f
+    ( λ g H → ap-binary m (H x) (H y) ＝ ap (λ f → m (f x) (f y)) (eq-htpy H))
+    ( inv
+      (ap (ap (λ f → m (f x) (f y))) (eq-htpy-refl-htpy _)))
+    ( H)
+```

src/foundation/transport-along-identifications-dependent-functions.lagda.md

@@ -0,0 +1,29 @@
+# Transport along identifications in dependent functions
+
+```agda
+module foundation.transport-along-identifications-dependent-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.transport-along-identifications
+```
+
+</details>
+
+## Definition
+
+```agda
+tr-Π :
+  {l1 l2 l3 : Level} {I : UU l1}
+  {A : UU l2} {B : I → A → UU l3}
+  {i j : I} (p : i ＝ j) →
+  (f : (a : A) → B i a) →
+  (a : A) →
+  tr (λ f → (a : A) → B f a) p f a ＝ tr (λ x → B x a) p (f a)
+tr-Π refl f a = refl
+```

src/lists.lagda.md

@@ -10,6 +10,7 @@ open import lists.concatenation-lists public
 open import lists.dependent-sequences public
 open import lists.equivalence-tuples-finite-sequences public
 open import lists.finite-sequences public
+open import lists.flattening-free-magmas-lists public
 open import lists.flattening-lists public
 open import lists.functoriality-finite-sequences public
 open import lists.functoriality-lists public

src/lists/flattening-free-magmas-lists.lagda.md

@@ -0,0 +1,137 @@
+# The flattening morphisms from free magmas to free monoids
+
+```agda
+module lists.flattening-free-magmas-lists where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+
+open import lists.concatenation-lists
+open import lists.lists
+open import lists.universal-property-lists-wild-monoids
+
+open import structured-types.magmas
+open import structured-types.morphisms-h-spaces
+open import structured-types.morphisms-magmas
+open import structured-types.morphisms-wild-monoids
+open import structured-types.pointed-maps
+open import structured-types.wild-monoids
+
+open import trees.combinator-full-binary-trees
+open import trees.free-magmas-on-types
+open import trees.full-binary-trees
+open import trees.labeled-full-binary-trees
+```
+
+</details>
+
+## Idea
+
+For any type `X`, there is a natural
+[magma map](structured-types.morphisms-magmas.md) from
+`labeled-full-binary-tree-Magma X`, the
+[free magma on `X`](trees.free-magmas-on-types.md), to `list-Wild-Monoid X`, the
+[free wild monoid on `X`](lists.universal-property-lists-wild-monoids.md), that
+can be thought of as forgetting the tree structure and remembering the order
+leaves are read off in. This map is universal among magma maps from
+`labeled-full-binary-tree-Magma X` to
+[wild monoids](structured-types.wild-monoids.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level} (X : UU l)
+  where
+
+  {-# TERMINATING #-}
+  flattening-map-free-Magma-free-Wild-Monoid :
+    type-Magma (labeled-full-binary-tree-Magma X) →
+    type-Wild-Monoid (list-Wild-Monoid X)
+  flattening-map-free-Magma-free-Wild-Monoid (leaf-full-binary-tree , label) =
+    cons (label star) nil
+  flattening-map-free-Magma-free-Wild-Monoid
+    (join-full-binary-tree L R , label) =
+      concat-list
+      ( flattening-map-free-Magma-free-Wild-Monoid (L , λ z → label (inl z)))
+      ( flattening-map-free-Magma-free-Wild-Monoid (R , (λ z → label (inr z))))
+
+  preserves-mul-flattening-map-free-Magma-free-Wild-Monoid :
+    preserves-mul-Magma (labeled-full-binary-tree-Magma X)
+    (magma-Wild-Monoid (list-Wild-Monoid X))
+    flattening-map-free-Magma-free-Wild-Monoid
+  preserves-mul-flattening-map-free-Magma-free-Wild-Monoid T U = refl
+
+  flattening-hom-free-Magma-free-Wild-Monoid :
+    hom-Magma (labeled-full-binary-tree-Magma X)
+    (magma-Wild-Monoid (list-Wild-Monoid X))
+  pr1 flattening-hom-free-Magma-free-Wild-Monoid =
+    flattening-map-free-Magma-free-Wild-Monoid
+  pr2 flattening-hom-free-Magma-free-Wild-Monoid =
+    preserves-mul-flattening-map-free-Magma-free-Wild-Monoid
+```
+
+## Properties
+
+### The flattening map preserves weights
+
+That is, the length of a flattened full binary tree `T` is equal to the weight
+of `T`.
+
+```agda
+  preserves-weight-flattening-hom-free-Magma-free-Wild-Monoid :
+    (T : labeled-full-binary-tree X) →
+    length-list (flattening-map-free-Magma-free-Wild-Monoid T) ＝
+    weight-labeled-full-binary-tree X T
+  preserves-weight-flattening-hom-free-Magma-free-Wild-Monoid
+    (leaf-full-binary-tree , label) =
+      refl
+  preserves-weight-flattening-hom-free-Magma-free-Wild-Monoid
+    (join-full-binary-tree L R , label) =
+      ap-binary add-ℕ refl refl
+```
+
+### The flattening map is the universal map from `labeled-full-binary-tree-Magma X` to a wild monoid
+
+More precisely, for any wild monoid `M` and magma map
+`f : labeled-full-binary-tree-Magma X → M`, the space of monoid maps
+`list-Wild-Monoid X → M` commuting with the flattening map is contractible.
+
+```agda
+module _
+  {l1 l2 : Level} (X : UU l1) (M : Wild-Monoid l2)
+  where
+
+  extension-flattening-map-free-Magma-free-Wild-Monoid :
+    (f : hom-Magma (labeled-full-binary-tree-Magma X) (magma-Wild-Monoid M)) →
+    hom-Wild-Monoid (list-Wild-Monoid X) M
+  extension-flattening-map-free-Magma-free-Wild-Monoid f =
+    elim-list-Wild-Monoid M (label-of-leaf X (magma-Wild-Monoid M) f)
+
+  extension-flattening-map-commutes-free-Magma-free-Wild-Monoid :
+    (f : hom-Magma (labeled-full-binary-tree-Magma X) (magma-Wild-Monoid M)) →
+    map-hom-Magma (labeled-full-binary-tree-Magma X) (magma-Wild-Monoid M) f ~
+    map-hom-Wild-Monoid (list-Wild-Monoid X) M
+      (extension-flattening-map-free-Magma-free-Wild-Monoid f) ∘
+    flattening-map-free-Magma-free-Wild-Monoid X
+  extension-flattening-map-commutes-free-Magma-free-Wild-Monoid
+    (f , hom-f) (leaf-full-binary-tree , label) =
+      {!   !}
+  extension-flattening-map-commutes-free-Magma-free-Wild-Monoid
+    (f , hom-f) (join-full-binary-tree L R , label) =
+      {!   !}
+```