Free magmas

src/structured-types/morphisms-magmas.lagda.md

@@ -18,8 +18,8 @@ open import structured-types.magmas
 
 ## Idea
 
-A morphism of magmas from `M` to `N` is a map between their underlying type that
-preserves the binary operation
+A morphism of magmas from `M` to `N` is a map between their underlying types
+that preserves the binary operation.
 
 ## Definition
 

src/trees.lagda.md

@@ -19,6 +19,7 @@ open import trees.coalgebra-of-enriched-directed-trees public
 open import trees.coalgebras-polynomial-endofunctors public
 open import trees.combinator-directed-trees public
 open import trees.combinator-enriched-directed-trees public
+open import trees.combinator-full-binary-trees public
 open import trees.directed-trees public
 open import trees.elementhood-relation-coalgebras-polynomial-endofunctors public
 open import trees.elementhood-relation-w-types public
@@ -29,6 +30,8 @@ open import trees.equivalences-enriched-directed-trees public
 open import trees.extensional-w-types public
 open import trees.fibers-directed-trees public
 open import trees.fibers-enriched-directed-trees public
+open import trees.free-magma-on-one-generator public
+open import trees.free-magmas-on-types public
 open import trees.full-binary-trees public
 open import trees.functoriality-combinator-directed-trees public
 open import trees.functoriality-fiber-directed-tree public
@@ -37,6 +40,7 @@ open import trees.hereditary-w-types public
 open import trees.indexed-w-types public
 open import trees.induction-w-types public
 open import trees.inequality-w-types public
+open import trees.labeled-full-binary-trees public
 open import trees.lower-types-w-types public
 open import trees.morphisms-algebras-polynomial-endofunctors public
 open import trees.morphisms-coalgebras-polynomial-endofunctors public

src/trees/combinator-full-binary-trees.lagda.md

@@ -0,0 +1,59 @@
+# The combinator of full binary trees
+
+```agda
+module trees.combinator-full-binary-trees where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import structured-types.magmas
+
+open import trees.full-binary-trees
+open import trees.labeled-full-binary-trees
+```
+
+</details>
+
+## Idea
+
+Two [full binary trees](trees.full-binary-trees.md) `L, R` may be combined into
+a new full binary tree in the natural way. By abstract nonsense, this extends to
+a combinator of [labeled full binary trees](trees.labeled-full-binary-trees.md).
+These form an important class of [magmas](structured-types.magmas.md), cf.
+[the free magma on one generator](trees.free-magma-on-one-generator.md) and
+[free magmas on types](trees.free-magmas-on-types.md).
+
+## Definition
+
+```agda
+combinator-full-binary-tree :
+  full-binary-tree → full-binary-tree → full-binary-tree
+combinator-full-binary-tree L R = join-full-binary-tree L R
+
+combinator-labeled-full-binary-tree :
+  {l : Level} (X : UU l) → labeled-full-binary-tree X →
+  labeled-full-binary-tree X → labeled-full-binary-tree X
+pr1 (combinator-labeled-full-binary-tree X (L , _) (R , _)) =
+  combinator-full-binary-tree L R
+pr2 (combinator-labeled-full-binary-tree X (L , L-label) (R , _)) (inl x) =
+  L-label x
+pr2 (combinator-labeled-full-binary-tree X (L , _) (R , R-label)) (inr x) =
+  R-label x
+```
+
+### The magmas of full binary trees and labeled full binary trees
+
+```agda
+full-binary-tree-Magma : Magma lzero
+pr1 full-binary-tree-Magma = full-binary-tree
+pr2 full-binary-tree-Magma = combinator-full-binary-tree
+
+labeled-full-binary-tree-Magma : {l : Level} (X : UU l) → Magma l
+pr1 (labeled-full-binary-tree-Magma X) = labeled-full-binary-tree X
+pr2 (labeled-full-binary-tree-Magma X) = combinator-labeled-full-binary-tree X
+```

src/trees/free-magma-on-one-generator.lagda.md

@@ -0,0 +1,148 @@
+# The free magma on one generator
+
+```agda
+module trees.free-magma-on-one-generator where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import foundation-core.dependent-identifications
+open import foundation-core.sets
+open import foundation-core.transport-along-identifications
+
+open import structured-types.magmas
+open import structured-types.morphisms-magmas
+
+open import trees.combinator-full-binary-trees
+open import trees.full-binary-trees
+open import trees.labeled-full-binary-trees
+```
+
+</details>
+
+## Idea
+
+Function extensionality implies that the
+[magma of full binary trees](trees.combinator-full-binary-trees.md) is the
+**free magma on one generator**. That is, there are natural maps
+`image-of-leaf : hom-Magma full-binary-tree-Magma M → (type-Magma M), extension-of-point-hom-full-binary-tree-Magma : (type-Magma M) → hom-Magma full-binary-tree-Magma M`
+for any [magma](structured-types.magmas.md) `M`.
+`extension-of-point-hom-full-binary-tree-Magma` is always a
+[section](foundation-core.sections.md) of `image-of-leaf`, and when `M` is a
+set, we may prove it is also a [retraction](foundation-core.retractions.md),
+i.e. that `image-of-leaf` is an [equivalence](foundation-core.equivalences.md).
+
+## Proof
+
+```agda
+module _
+  {l : Level} (M : Magma l)
+  where
+
+  image-of-leaf : hom-Magma full-binary-tree-Magma M → type-Magma M
+  image-of-leaf (f , _) = f leaf-full-binary-tree
+
+  extension-of-point-full-binary-tree-Magma :
+    type-Magma M → full-binary-tree → type-Magma M
+  extension-of-point-full-binary-tree-Magma m leaf-full-binary-tree = m
+  extension-of-point-full-binary-tree-Magma m (join-full-binary-tree L R) =
+    mul-Magma M (extension-of-point-full-binary-tree-Magma m L)
+    ( extension-of-point-full-binary-tree-Magma m R)
+
+  is-hom-extension-of-point-full-binary-tree-Magma :
+    ( m : type-Magma M) → preserves-mul-Magma full-binary-tree-Magma M
+    ( extension-of-point-full-binary-tree-Magma m)
+  is-hom-extension-of-point-full-binary-tree-Magma m T U = refl
+
+  extension-of-point-hom-full-binary-tree-Magma :
+    type-Magma M → hom-Magma full-binary-tree-Magma M
+  pr1 (extension-of-point-hom-full-binary-tree-Magma m) =
+    extension-of-point-full-binary-tree-Magma m
+  pr2 (extension-of-point-hom-full-binary-tree-Magma m) =
+    is-hom-extension-of-point-full-binary-tree-Magma m
+
+  is-retraction-extension-of-point-full-binary-tree-Magma :
+    ( T : full-binary-tree) → (f : hom-Magma full-binary-tree-Magma M) →
+    extension-of-point-full-binary-tree-Magma (image-of-leaf f) T ＝
+    map-hom-Magma full-binary-tree-Magma M f T
+  is-retraction-extension-of-point-full-binary-tree-Magma
+    leaf-full-binary-tree f = refl
+  is-retraction-extension-of-point-full-binary-tree-Magma
+    ( join-full-binary-tree L R) (f , is-hom-f) =
+      ap-binary (mul-Magma M)
+      ( is-retraction-extension-of-point-full-binary-tree-Magma L
+        ( f , is-hom-f))
+      ( is-retraction-extension-of-point-full-binary-tree-Magma R
+        ( f , is-hom-f))
+      ∙ inv (is-hom-f L R)
+
+  is-set-dependent-identification-preserves-mul-full-binary-tree-Magma :
+    ( f : hom-Magma full-binary-tree-Magma M) → is-set (type-Magma M) →
+    dependent-identification (preserves-mul-Magma full-binary-tree-Magma M)
+    ( eq-htpy
+      ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f))
+    ( λ T U → refl) (pr2 f)
+  is-set-dependent-identification-preserves-mul-full-binary-tree-Magma
+    f is-set-M = eq-htpy htpy
+      where
+      htpy :
+        tr (preserves-mul-Magma full-binary-tree-Magma M) (eq-htpy
+          ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f))
+        ( λ T U → refl) ~ pr2 f
+      htpy T = eq-htpy htpy2
+        where
+        htpy2 :
+          tr (preserves-mul-Magma full-binary-tree-Magma M) (eq-htpy
+            ( λ U →
+              is-retraction-extension-of-point-full-binary-tree-Magma U f))
+          ( λ U V → refl) T ~ pr2 f T
+        htpy2 U =
+          pr1 (is-set-M (map-hom-Magma full-binary-tree-Magma M f
+            ( pr2 full-binary-tree-Magma T U))
+              ( pr2 M (map-hom-Magma full-binary-tree-Magma M f T)
+            ( map-hom-Magma full-binary-tree-Magma M f U))
+              ( tr (preserves-mul-Magma full-binary-tree-Magma M)
+            ( eq-htpy (λ V →
+              is-retraction-extension-of-point-full-binary-tree-Magma V f))
+            ( λ V W → refl) T U) (pr2 f T U))
+
+  is-set-is-equiv-image-of-leaf-full-binary-tree-Magma :
+    is-set (type-Magma M) → is-equiv image-of-leaf
+  pr1 (pr1 (is-set-is-equiv-image-of-leaf-full-binary-tree-Magma _)) =
+    extension-of-point-hom-full-binary-tree-Magma
+  pr2 (pr1 (is-set-is-equiv-image-of-leaf-full-binary-tree-Magma _)) _ = refl
+  pr1 (pr2 (is-set-is-equiv-image-of-leaf-full-binary-tree-Magma _)) =
+    extension-of-point-hom-full-binary-tree-Magma
+  pr2 (pr2 (is-set-is-equiv-image-of-leaf-full-binary-tree-Magma is-set-M)) f =
+    eq-pair-Σ (eq-htpy
+      ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f))
+    ( is-set-dependent-identification-preserves-mul-full-binary-tree-Magma
+      f is-set-M)
+
+  is-set-equiv-image-of-leaf-full-binary-tree-Magma :
+    is-set (type-Magma M) → hom-Magma full-binary-tree-Magma M ≃ type-Magma M
+  pr1 (is-set-equiv-image-of-leaf-full-binary-tree-Magma _) = image-of-leaf
+  pr2 (is-set-equiv-image-of-leaf-full-binary-tree-Magma is-set-M) =
+    is-set-is-equiv-image-of-leaf-full-binary-tree-Magma is-set-M
+```
+
+## See also
+
+- This construction may be extended to
+  [labeled full binary trees](trees.labeled-full-binary-trees.md) to realize
+  free magmas on any type, see
+  [`trees.free-magmas-on-types`](trees.free-magmas-on-types.md).
+
+## External links
+
+[Free magmas](https://ncatlab.org/nlab/show/magma#free_magmas) at $n$Lab