diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index f0f52a7493..1d97f1ad40 100644
--- a/src/foundation.lagda.md
+++ b/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
diff --git a/src/foundation/action-on-binary-homotopies-binary-functions.lagda.md b/src/foundation/action-on-binary-homotopies-binary-functions.lagda.md
new file mode 100644
index 0000000000..605252453b
--- /dev/null
+++ b/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)
+```
diff --git a/src/foundation/transport-along-identifications-dependent-functions.lagda.md b/src/foundation/transport-along-identifications-dependent-functions.lagda.md
new file mode 100644
index 0000000000..4a838dbe11
--- /dev/null
+++ b/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
+```
diff --git a/src/lists.lagda.md b/src/lists.lagda.md
index 373398754b..d67e1ed594 100644
--- a/src/lists.lagda.md
+++ b/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
diff --git a/src/lists/flattening-free-magmas-lists.lagda.md b/src/lists/flattening-free-magmas-lists.lagda.md
new file mode 100644
index 0000000000..114159ee2f
--- /dev/null
+++ b/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) =
+      {!   !}
+```
diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md
index 67c4735fec..748b6132f2 100644
--- a/src/lists/universal-property-lists-wild-monoids.lagda.md
+++ b/src/lists/universal-property-lists-wild-monoids.lagda.md
@@ -7,13 +7,25 @@ module lists.universal-property-lists-wild-monoids where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-binary-homotopies-binary-functions
+open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
 open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.transport-along-identifications-dependent-functions
 open import foundation.unit-type
 open import foundation.universe-levels
 open import foundation.whiskering-higher-homotopies-composition
 
+open import foundation-core.dependent-identifications
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.transport-along-identifications
+
 open import group-theory.homomorphisms-semigroups
 
 open import lists.concatenation-lists
@@ -22,6 +34,7 @@ open import lists.lists
 open import structured-types.h-spaces
 open import structured-types.morphisms-h-spaces
 open import structured-types.morphisms-wild-monoids
+open import structured-types.pointed-homotopies
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
 open import structured-types.wild-monoids
@@ -31,11 +44,30 @@ 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.
+The type of lists of elements of `X` is the free wild monoid on `X` - that is,
+for any wild monoid `M`, there is an equivalence:
+
+```text
+  (X → type-Wild-Monoid M)
+  ≃
+  hom-Wild-Monoid (list X) M
+```
 
 ## Definition
 
+### The universal property of free wild monoids on a type
+
+```agda
+module _
+  {l1 l2 : Level} (X : UU l1) (M : Wild-Monoid l2) (f : X → type-Wild-Monoid M)
+  where
+
+  is-free-wild-monoid-on-type : UUω
+  is-free-wild-monoid-on-type =
+    {l3 : Level} (N : Wild-Monoid l3) →
+    is-equiv (λ g → map-hom-Wild-Monoid M N g ∘ f)
+```
+
 ### The pointed type of lists of elements of `X`
 
 ```agda
@@ -301,48 +333,92 @@ 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
+### Pulling back `hom (list X) M` along the inclusion `X → list X` is an equivalence
 
-This remains to be formalized. The following block contains some abandoned old
-code towards this goal:
+This remains to be formalized. Below is some work towards this goal:
 
-```text
-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 α β) γ
+```agda
+{-
+
+module _
+  {l1 l2 : Level} (X : UU l1) (M : Wild-Monoid l2)
   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) ∙
-    ( ( left-whisker-concat (pr2 g) (inv (left-inv (pr2 h)))) ∙
-      ( inv (assoc (pr2 g) (inv (pr2 h)) (pr2 h))))
+
+  map-inv-elim-list-Wild-Monoid :
+    hom-Wild-Monoid (list-Wild-Monoid X) M → X → type-Wild-Monoid M
+  map-inv-elim-list-Wild-Monoid f x =
+    map-hom-Wild-Monoid (list-Wild-Monoid X) M f (cons x nil)
+
+  htpy-elim-list-Wild-Monoid :
+    (f : hom-Wild-Monoid (list-Wild-Monoid X) M) →
+    pr1 (pr1 ((elim-list-Wild-Monoid M ∘ (λ g x → pr1 (pr1 g) (cons x nil))) f))
+    ~ map-hom-Wild-Monoid _ _ f
+  htpy-elim-list-Wild-Monoid ((f , pt-f) , _) nil =
+    inv pt-f
+  htpy-elim-list-Wild-Monoid f (cons x y) =
+    ap-binary (mul-Wild-Monoid M) refl (htpy-elim-list-Wild-Monoid f y) ∙
+    inv (preserves-mul-hom-Wild-Monoid (list-Wild-Monoid X) M f)
+
+  dependent-identification-mul-elim-list-Wild-Monoid :
+    (f : hom-Wild-Monoid (list-Wild-Monoid X) M) →
+    pr1 (tr (preserves-unital-mul-pointed-map-H-Space (list-H-Space X) (pr1 M))
+      (eq-pointed-htpy
+        ((λ x →
+          map-elim-list-Wild-Monoid M
+            (λ x₁ → pr1 (pr1 f) (cons x₁ nil)) x) , refl)
+        ((λ x → pr1 (pr1 f) x) , pr2 (pr1 f))
+        (htpy-elim-list-Wild-Monoid f , inv (left-inv (pr2 (pr1 f)))))
+      (pr2 (elim-list-Wild-Monoid M (λ x → pr1 (pr1 f) (cons x nil))))) ＝
+    preserves-mul-hom-Wild-Monoid (list-Wild-Monoid X) M f
+  dependent-identification-mul-elim-list-Wild-Monoid ((f , pt-f) , mul-f , _) =
+    {!   !} -- this should fill with eq-binary-htpy as mul-f is a binary function but the type checker is unhappy with that...
+
+  dependent-identification-left-unit-law-elim-list-Wild-Monoid :
+    (f : hom-Wild-Monoid (list-Wild-Monoid X) M) →
+    {!   !} ＝
+    preserves-left-unit-law-mul-map-hom-Wild-Monoid (list-Wild-Monoid X) M f
+  dependent-identification-left-unit-law-elim-list-Wild-Monoid f = {!   !}
+
+  dependent-identification-right-unit-law-elim-list-Wild-Monoid :
+    (f : hom-Wild-Monoid (list-Wild-Monoid X) M) →
+    {!   !} ＝
+    preserves-right-unit-law-mul-map-hom-Wild-Monoid (list-Wild-Monoid X) M f
+  dependent-identification-right-unit-law-elim-list-Wild-Monoid f = {!   !}
+
+  dependent-identification-coh-unit-law-elim-list-Wild-Monoid :
+    (f : hom-Wild-Monoid (list-Wild-Monoid X) M) →
+    {!   !} ＝
+    preserves-coh-unit-laws-map-hom-Wild-Monoid (list-Wild-Monoid X) M f
+  dependent-identification-coh-unit-law-elim-list-Wild-Monoid f = {!   !}
+
+  is-equiv-elim-list-Wild-Monoid : is-equiv (elim-list-Wild-Monoid M)
+  pr1 (pr1 is-equiv-elim-list-Wild-Monoid) = map-inv-elim-list-Wild-Monoid
+  pr2 (pr1 is-equiv-elim-list-Wild-Monoid) f =
+    eq-pair-Σ
+    ( eq-pointed-htpy _ _
+      ( htpy-elim-list-Wild-Monoid f ,
+      inv (left-inv
+        ( preserves-unit-map-hom-Wild-Monoid (list-Wild-Monoid X) M f))))
+    ( eq-pair-Σ {! dependent-identification-mul-elim-list-Wild-Monoid f !} -- this should fill with dependent-identification-mul-elim-list-Wild-Monoid f but the type checker is unhappy with that too?
+      ( eq-pair-Σ
+      {!   !}
+        (eq-pair-Σ
+        {!   !}
+        {!   !})))
+  pr1 (pr2 is-equiv-elim-list-Wild-Monoid) = map-inv-elim-list-Wild-Monoid
+  pr2 (pr2 is-equiv-elim-list-Wild-Monoid) f =
+    eq-htpy (λ x → pr1 (pr2 (pr2 (pr2 (pr1 M)))) (f x))
+
+  equiv-elim-list-Wild-Monoid :
+    (X → type-Wild-Monoid M) ≃ hom-Wild-Monoid (list-Wild-Monoid X) M
+  pr1 equiv-elim-list-Wild-Monoid = elim-list-Wild-Monoid M
+  pr2 equiv-elim-list-Wild-Monoid = is-equiv-elim-list-Wild-Monoid
+
+is-free-wild-monoid-on-type-list-Wild-Monoid :
+  {l : Level} (X : UU l) →
+  is-free-wild-monoid-on-type X (list-Wild-Monoid X) (λ x → cons x nil)
+is-free-wild-monoid-on-type-list-Wild-Monoid X N =
+  is-equiv-map-inv-is-equiv (is-equiv-elim-list-Wild-Monoid X N)
+
+-}
 ```
diff --git a/src/structured-types/morphisms-magmas.lagda.md b/src/structured-types/morphisms-magmas.lagda.md
index e5d3920e3b..f5068cdf37 100644
--- a/src/structured-types/morphisms-magmas.lagda.md
+++ b/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
 
@@ -42,3 +42,16 @@ module _
     (f : hom-Magma) → preserves-mul-Magma (map-hom-Magma f)
   preserves-mul-map-hom-Magma = pr2
 ```
+
+## Properties
+
+### Evaluating magma morphisms at an element
+
+```agda
+module _
+  {l1 l2 : Level} (M : Magma l1) (N : Magma l2)
+  where
+
+  ev-element-hom-Magma : type-Magma M → hom-Magma M N → type-Magma N
+  ev-element-hom-Magma x f = map-hom-Magma M N f x
+```
diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md
index 250cabb823..143fb8a38e 100644
--- a/src/structured-types/wild-monoids.lagda.md
+++ b/src/structured-types/wild-monoids.lagda.md
@@ -14,6 +14,7 @@ open import foundation.unit-type
 open import foundation.universe-levels
 
 open import structured-types.h-spaces
+open import structured-types.magmas
 open import structured-types.pointed-types
 ```
 
@@ -173,6 +174,10 @@ module _
   mul-Wild-Monoid' : type-Wild-Monoid → type-Wild-Monoid → type-Wild-Monoid
   mul-Wild-Monoid' = mul-H-Space' h-space-Wild-Monoid
 
+  magma-Wild-Monoid : Magma l
+  pr1 magma-Wild-Monoid = type-Wild-Monoid
+  pr2 magma-Wild-Monoid = mul-Wild-Monoid
+
   ap-mul-Wild-Monoid :
     {a b c d : type-Wild-Monoid} →
     a ＝ b → c ＝ d → mul-Wild-Monoid a c ＝ mul-Wild-Monoid b d
diff --git a/src/trees.lagda.md b/src/trees.lagda.md
index c2cfc02fbc..5547c50b38 100644
--- a/src/trees.lagda.md
+++ b/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
diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md
new file mode 100644
index 0000000000..8e6a5c760e
--- /dev/null
+++ b/src/trees/combinator-full-binary-trees.lagda.md
@@ -0,0 +1,118 @@
+# The combinator of full binary trees
+
+```agda
+module trees.combinator-full-binary-trees where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.dependent-identifications
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.transport-along-identifications
+
+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. 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
+```
+
+## Properties
+
+### The combinator of labeled full binary trees commutes with branches
+
+That is, for binary trees `L R : full-binary-tree` and an `X`-labeling `lab` of
+`join-full-binary-tree L R`, we have
+
+```text
+  combinator-labeled-full-binary-tree X (L , λ x → lab (inl x)) (R , λ x → lab (inr x))
+  =
+  (( join-full-binary-tree L R) , lab)
+```
+
+```agda
+Eq-combinator-commutes-with-labelings-full-binary-tree :
+  {l : Level} (X : UU l) (L R : full-binary-tree)
+  (lab : labeling-full-binary-tree X (join-full-binary-tree L R)) →
+  Eq-labeled-full-binary-tree X
+    (combinator-labeled-full-binary-tree X
+      (L , (λ z → lab (inl z)))
+      (R , (λ z → lab (inr z))))
+    ((join-full-binary-tree L R) , lab)
+pr1 (Eq-combinator-commutes-with-labelings-full-binary-tree X L R lab) =
+  ( refl-Eq-full-binary-tree L , refl-Eq-full-binary-tree R)
+pr2 (Eq-combinator-commutes-with-labelings-full-binary-tree X L R lab) =
+  (( refl-htpy-labeled-full-binary-tree X (L , λ x → lab (inl x))) ,
+    refl-htpy-labeled-full-binary-tree X (R , (λ x → lab (inr x))))
+
+is-refl-Eq-combinator-commutes-with-labelings-full-binary-tree :
+  {l : Level} (X : UU l) (L R : full-binary-tree)
+  (lab : labeling-full-binary-tree X (join-full-binary-tree L R)) →
+  Eq-combinator-commutes-with-labelings-full-binary-tree X L R lab ＝
+  refl-Eq-labeled-full-binary-tree X ((join-full-binary-tree L R) , lab)
+is-refl-Eq-combinator-commutes-with-labelings-full-binary-tree X L R lab = refl
+
+combinator-commutes-with-labelings-full-binary-tree :
+  {l : Level} (X : UU l) (L R : full-binary-tree)
+  (lab : labeling-full-binary-tree X (join-full-binary-tree L R)) →
+  combinator-labeled-full-binary-tree X
+    ( L , (λ x → lab (inl x))) (R , (λ x → lab (inr x))) ＝
+  ( join-full-binary-tree L R , lab)
+combinator-commutes-with-labelings-full-binary-tree X L R lab =
+  eq-Eq-labeled-full-binary-tree X
+    ( combinator-labeled-full-binary-tree X
+      ( L , (λ x → lab (inl x)))
+      ( R , (λ x → lab (inr x))))
+    ( join-full-binary-tree L R , lab)
+    ( Eq-combinator-commutes-with-labelings-full-binary-tree X L R lab)
+```
diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md
new file mode 100644
index 0000000000..8aaecdcfc0
--- /dev/null
+++ b/src/trees/free-magma-on-one-generator.lagda.md
@@ -0,0 +1,179 @@
+# 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-binary-homotopies-binary-functions
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+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.transport-along-identifications-dependent-functions
+open import foundation.universe-levels
+
+open import foundation-core.dependent-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
+```
+
+</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
+
+```text
+  ev-leaf-hom-Magma : hom-Magma full-binary-tree-Magma M → (type-Magma M)
+  map-inv-ev-leaf-hom-Magma : (type-Magma M) → hom-Magma full-binary-tree-Magma M
+```
+
+for any [magma](structured-types.magmas.md) `M` that form an
+[equivalence](foundation-core.equivalences.md).
+
+## Definitions
+
+### The universal property of free magmas with one generator
+
+```agda
+module _
+  {l : Level} (M : Magma l) (x : type-Magma M)
+  where
+
+  is-free-magma-on-one-generator : UUω
+  is-free-magma-on-one-generator =
+    {l2 : Level} (N : Magma l2) → is-equiv (ev-element-hom-Magma M N x)
+```
+
+## Proof
+
+```agda
+module _
+  {l : Level} (M : Magma l)
+  where
+
+  ev-leaf-hom-Magma : hom-Magma full-binary-tree-Magma M → type-Magma M
+  ev-leaf-hom-Magma (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
+
+  map-inv-ev-leaf-hom-Magma :
+    type-Magma M → hom-Magma full-binary-tree-Magma M
+  pr1 (map-inv-ev-leaf-hom-Magma m) =
+    extension-of-point-full-binary-tree-Magma m
+  pr2 (map-inv-ev-leaf-hom-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 (ev-leaf-hom-Magma 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)
+
+  dependent-identification-preserves-mul-full-binary-tree-Magma :
+    ( f : hom-Magma full-binary-tree-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)
+  dependent-identification-preserves-mul-full-binary-tree-Magma f =
+    eq-binary-htpy _ _
+      ( λ U V →
+        ( htpy-eq
+          ( tr-Π
+            ( eq-htpy (λ T →
+              is-retraction-extension-of-point-full-binary-tree-Magma T f))
+            ( λ T U → refl)
+            ( U))
+          ( V)) ∙
+        ( tr-Π
+          ( eq-htpy (λ T →
+            is-retraction-extension-of-point-full-binary-tree-Magma T f))
+          ( λ U → refl)
+          ( V)) ∙
+        ( map-compute-dependent-identification-eq-value-function
+          ( λ f → f (combinator-full-binary-tree U V))
+          ( λ f → mul-Magma M (f U) (f V))
+          ( eq-htpy
+            ( λ T →
+              is-retraction-extension-of-point-full-binary-tree-Magma T f))
+          ( refl)
+          ( preserves-mul-map-hom-Magma full-binary-tree-Magma M f U V)
+          ( ( ap
+              ( _∙ preserves-mul-map-hom-Magma full-binary-tree-Magma M f U V)
+              ( htpy-eq (is-section-eq-htpy _) _)) ∙
+            ( is-section-inv-concat'
+              ( preserves-mul-map-hom-Magma full-binary-tree-Magma M f U V)
+              ( _)) ∙
+            ( ap-binary-htpy
+              ( λ T →
+                is-retraction-extension-of-point-full-binary-tree-Magma T f)
+              ( mul-Magma M)))))
+
+  is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma :
+    is-equiv ev-leaf-hom-Magma
+  pr1 (pr1 (is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma)) =
+    map-inv-ev-leaf-hom-Magma
+  pr2 (pr1 (is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma)) _ = refl
+  pr1 (pr2 (is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma)) =
+    map-inv-ev-leaf-hom-Magma
+  pr2 (pr2 (is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma)) f =
+    eq-pair-Σ (eq-htpy
+      ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f))
+    ( dependent-identification-preserves-mul-full-binary-tree-Magma f)
+
+  equiv-ev-leaf-hom-Magma-full-binary-tree-Magma :
+    hom-Magma full-binary-tree-Magma M ≃ type-Magma M
+  pr1 (equiv-ev-leaf-hom-Magma-full-binary-tree-Magma) = ev-leaf-hom-Magma
+  pr2 (equiv-ev-leaf-hom-Magma-full-binary-tree-Magma) =
+    is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma
+
+is-free-magma-on-one-generator-full-binary-tree-Magma :
+  is-free-magma-on-one-generator full-binary-tree-Magma leaf-full-binary-tree
+is-free-magma-on-one-generator-full-binary-tree-Magma =
+  is-equiv-ev-leaf-hom-Magma-full-binary-tree-Magma
+```
+
+## 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
diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md
new file mode 100644
index 0000000000..9fafb3352a
--- /dev/null
+++ b/src/trees/free-magmas-on-types.lagda.md
@@ -0,0 +1,194 @@
+# Free magmas on types
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module trees.free-magmas-on-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-binary-homotopies-binary-functions
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+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.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.transport-along-identifications-dependent-functions
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.coproduct-types
+open import foundation-core.dependent-identifications
+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
+
+As the type of [full binary trees](trees.full-binary-trees.md) is the
+[free magma on one generator](trees.free-magma-on-one-generator.md), so too is
+the type of [labeled full binary trees](trees.labeled-full-binary-trees.md) with
+indices labeled in a type `X` the **free magma on `X`**. The product comes from
+the [combinator of full binary trees](trees.combinator-full-binary-trees.md).
+
+What is meant by the "free magma on `X`" is the following. There are natural
+maps
+
+```text
+  ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M)
+  map-inv-ev-label-leaf-hom-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M
+```
+
+for any [magma](structured-types.magmas.md) `M` and type `X` that form an
+[equivalence](foundation-core.equivalences.md).
+
+## Definition
+
+### The universal property of free magmas on types
+
+```agda
+module _
+  {l1 l2 : Level} (M : Magma l1) (X : UU l2) (f : X → type-Magma M)
+  where
+
+  is-free-magma-on-type : UUω
+  is-free-magma-on-type =
+    {l3 : Level} (N : Magma l3) → is-equiv (λ g → map-hom-Magma M N g ∘ f)
+```
+
+## Proof
+
+```agda
+module _
+  {l1 l2 : Level} (X : UU l1) (M : Magma l2)
+  where
+
+  ev-label-leaf-hom-Magma :
+    hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M)
+  ev-label-leaf-hom-Magma (f , _) x = f (leaf-full-binary-tree , λ _ → x)
+
+  {-# TERMINATING #-}
+  extension-of-map-labeled-full-binary-tree-Magma :
+    ( X → type-Magma M) → labeled-full-binary-tree X → type-Magma M
+  extension-of-map-labeled-full-binary-tree-Magma
+    f (leaf-full-binary-tree , label-T) = f (label-T star)
+  extension-of-map-labeled-full-binary-tree-Magma
+    f (join-full-binary-tree L R , label-T) =
+      mul-Magma M
+        ( extension-of-map-labeled-full-binary-tree-Magma f
+          ( L , (λ x → label-T (inl x))))
+        ( extension-of-map-labeled-full-binary-tree-Magma f
+          ( R , (λ x → label-T (inr x))))
+
+  is-hom-extension-of-map-labeled-full-binary-tree-Magma :
+    ( f : X → type-Magma M) →
+    preserves-mul-Magma (labeled-full-binary-tree-Magma X) M
+    ( extension-of-map-labeled-full-binary-tree-Magma f)
+  is-hom-extension-of-map-labeled-full-binary-tree-Magma _ _ _ = refl
+
+  map-inv-ev-label-leaf-hom-Magma :
+    ( X → type-Magma M) → hom-Magma (labeled-full-binary-tree-Magma X) M
+  map-inv-ev-label-leaf-hom-Magma f =
+    extension-of-map-labeled-full-binary-tree-Magma f ,
+    is-hom-extension-of-map-labeled-full-binary-tree-Magma f
+
+  {-# TERMINATING #-}
+  is-retraction-extension-of-map-labeled-full-binary-tree-Magma :
+    ( T : labeled-full-binary-tree X) →
+    ( f : hom-Magma (labeled-full-binary-tree-Magma X) M) →
+    extension-of-map-labeled-full-binary-tree-Magma
+      ( ev-label-leaf-hom-Magma f) T ＝
+    map-hom-Magma (labeled-full-binary-tree-Magma X) M f T
+  is-retraction-extension-of-map-labeled-full-binary-tree-Magma
+    ( leaf-full-binary-tree , label-T) f = refl
+  is-retraction-extension-of-map-labeled-full-binary-tree-Magma
+    ( join-full-binary-tree L R , label-T) (f , is-hom-f) =
+      ap-binary (mul-Magma M)
+      ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma
+        ( L , (λ x → label-T (inl x))) (f , is-hom-f))
+      ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma
+        ( R , (λ x → label-T (inr x))) (f , is-hom-f))
+      ∙ inv (is-hom-f
+        ( L , (λ x → label-T (inl x))) (R , (λ x → label-T (inr x))))
+      ∙ ap f (combinator-commutes-with-labelings-full-binary-tree X L R label-T)
+
+  dependent-identification-preserves-mul-labeled-full-binary-tree-Magma :
+    ( f : hom-Magma (labeled-full-binary-tree-Magma X) M) →
+    dependent-identification
+    ( preserves-mul-Magma (labeled-full-binary-tree-Magma X) M)
+    ( eq-htpy
+      ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f))
+    ( λ T U → refl)
+    ( preserves-mul-map-hom-Magma
+      ( labeled-full-binary-tree-Magma X)
+      ( M)
+      ( f))
+  dependent-identification-preserves-mul-labeled-full-binary-tree-Magma f =
+    eq-binary-htpy _ _
+      ( λ U V →
+        ( htpy-eq
+          ( tr-Π _ ( λ T U₁ → refl) ( U))
+          ( V)) ∙
+        ( tr-Π _ (λ U₁ → refl) V) ∙
+        ( map-compute-dependent-identification-eq-value-function
+          ( λ f → f (combinator-labeled-full-binary-tree X U V))
+          ( λ f → mul-Magma M (f U) (f V))
+          ( eq-htpy
+            ( λ T →
+              is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f))
+          ( refl)
+          ( preserves-mul-map-hom-Magma
+            ( labeled-full-binary-tree-Magma X) M f U V)
+          ( ( ap
+              ( _∙ preserves-mul-map-hom-Magma
+                ( labeled-full-binary-tree-Magma X) M f U V)
+              ( htpy-eq (is-section-eq-htpy _) _)) ∙
+            ( {!   !}) ∙
+            ( ap-binary-htpy _ (mul-Magma M)))))
+
+  is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma :
+    is-equiv ev-label-leaf-hom-Magma
+  pr1 (pr1 (is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma)) =
+    map-inv-ev-label-leaf-hom-Magma
+  pr2 (pr1 (is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma)) _ = refl
+  pr1 (pr2 (is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma)) =
+    map-inv-ev-label-leaf-hom-Magma
+  pr2 (pr2 (is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma)) f =
+    eq-pair-Σ (eq-htpy (λ T →
+    is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f))
+      ( dependent-identification-preserves-mul-labeled-full-binary-tree-Magma f)
+
+  equiv-ev-label-leaf-hom-Magma-labeled-full-binary-tree-Magma :
+    hom-Magma (labeled-full-binary-tree-Magma X) M ≃ (X → type-Magma M)
+  pr1 (equiv-ev-label-leaf-hom-Magma-labeled-full-binary-tree-Magma) =
+    ev-label-leaf-hom-Magma
+  pr2 (equiv-ev-label-leaf-hom-Magma-labeled-full-binary-tree-Magma) =
+    is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma
+
+is-free-magma-on-type-labeled-full-binary-tree-Magma :
+  {l : Level} (X : UU l) →
+  is-free-magma-on-type
+    ( labeled-full-binary-tree-Magma X) X
+    ( λ x → leaf-full-binary-tree , λ _ → x)
+is-free-magma-on-type-labeled-full-binary-tree-Magma X =
+  is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma X
+```
+
+## External links
+
+[Free magmas](https://ncatlab.org/nlab/show/magma#free_magmas) at $n$Lab
diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md
index 72058ec915..d951fb503e 100644
--- a/src/trees/full-binary-trees.lagda.md
+++ b/src/trees/full-binary-trees.lagda.md
@@ -7,12 +7,25 @@ module trees.full-binary-trees where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 
-open import foundation.empty-types
+open import foundation.action-on-identifications-binary-functions
+open import foundation.decidable-equality
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.torsorial-type-families
+open import foundation.unit-type
 open import foundation.universe-levels
 
-open import univalent-combinatorics.standard-finite-types
+open import foundation-core.cartesian-product-types
+open import foundation-core.coproduct-types
+open import foundation-core.empty-types
+open import foundation-core.equivalences
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.sets
 ```
 
 </details>
@@ -35,3 +48,138 @@ data full-binary-tree : UU lzero where
   leaf-full-binary-tree : full-binary-tree
   join-full-binary-tree : (s t : full-binary-tree) → full-binary-tree
 ```
+
+### The nodes of a full binary tree
+
+```agda
+node-full-binary-tree : full-binary-tree → UU lzero
+node-full-binary-tree leaf-full-binary-tree = unit
+node-full-binary-tree (join-full-binary-tree G H) =
+  node-full-binary-tree G + node-full-binary-tree H
+```
+
+### The weight of a full binary tree
+
+This counts the number of nodes in `T : full-binary-tree` and can be thought of
+as an arboreal version of the length of a [list](lists.lists.md).
+
+```agda
+weight-full-binary-tree : full-binary-tree → ℕ
+weight-full-binary-tree leaf-full-binary-tree = 1
+weight-full-binary-tree (join-full-binary-tree T U) =
+  weight-full-binary-tree T +ℕ weight-full-binary-tree U
+```
+
+### Characterizing the identity type of full binary trees
+
+```agda
+Eq-full-binary-tree : full-binary-tree → full-binary-tree → UU lzero
+Eq-full-binary-tree leaf-full-binary-tree leaf-full-binary-tree = unit
+Eq-full-binary-tree leaf-full-binary-tree (join-full-binary-tree V V₁) = empty
+Eq-full-binary-tree (join-full-binary-tree U U₁) leaf-full-binary-tree = empty
+Eq-full-binary-tree (join-full-binary-tree U U₁) (join-full-binary-tree V V₁) =
+  Eq-full-binary-tree U V × Eq-full-binary-tree U₁ V₁
+
+is-prop-Eq-full-binary-tree :
+  (U V : full-binary-tree) → is-prop (Eq-full-binary-tree U V)
+is-prop-Eq-full-binary-tree leaf-full-binary-tree leaf-full-binary-tree =
+  is-prop-unit
+is-prop-Eq-full-binary-tree leaf-full-binary-tree (join-full-binary-tree V V₁) =
+  is-prop-empty
+is-prop-Eq-full-binary-tree (join-full-binary-tree U U₁) leaf-full-binary-tree =
+  is-prop-empty
+is-prop-Eq-full-binary-tree
+  (join-full-binary-tree U U₁) (join-full-binary-tree V V₁) =
+    is-prop-product
+    ( is-prop-Eq-full-binary-tree U V)
+    ( is-prop-Eq-full-binary-tree U₁ V₁)
+
+refl-Eq-full-binary-tree : (U : full-binary-tree) → Eq-full-binary-tree U U
+refl-Eq-full-binary-tree leaf-full-binary-tree = star
+refl-Eq-full-binary-tree (join-full-binary-tree U U₁) =
+  refl-Eq-full-binary-tree U , refl-Eq-full-binary-tree U₁
+
+Eq-eq-full-binary-tree :
+  {U V : full-binary-tree} → U ＝ V → Eq-full-binary-tree U V
+Eq-eq-full-binary-tree {U} refl = refl-Eq-full-binary-tree U
+
+eq-Eq-full-binary-tree :
+  (U V : full-binary-tree) → Eq-full-binary-tree U V → U ＝ V
+eq-Eq-full-binary-tree leaf-full-binary-tree leaf-full-binary-tree _ = refl
+eq-Eq-full-binary-tree leaf-full-binary-tree (join-full-binary-tree V V₁) ()
+eq-Eq-full-binary-tree (join-full-binary-tree U U₁) leaf-full-binary-tree ()
+eq-Eq-full-binary-tree
+  (join-full-binary-tree U U₁) (join-full-binary-tree V V₁) (p , q) =
+  ap-binary join-full-binary-tree
+    ( eq-Eq-full-binary-tree U V p)
+    ( eq-Eq-full-binary-tree U₁ V₁ q)
+
+map-total-Eq-full-binary-tree :
+  (U V : full-binary-tree) →
+  Σ full-binary-tree (Eq-full-binary-tree U) →
+  Σ full-binary-tree (Eq-full-binary-tree V) →
+  Σ full-binary-tree (Eq-full-binary-tree (join-full-binary-tree U V))
+pr1 (map-total-Eq-full-binary-tree U V (W , p) (X , q)) =
+  join-full-binary-tree W X
+pr1 (pr2 (map-total-Eq-full-binary-tree U V (W , p) (X , q))) = p
+pr2 (pr2 (map-total-Eq-full-binary-tree U V (W , p) (X , q))) = q
+
+is-torsorial-Eq-full-binary-tree :
+  (T : full-binary-tree) → is-torsorial (Eq-full-binary-tree T)
+pr1 (is-torsorial-Eq-full-binary-tree T) = T , refl-Eq-full-binary-tree T
+pr2 (is-torsorial-Eq-full-binary-tree leaf-full-binary-tree)
+  (leaf-full-binary-tree , star) = refl
+pr2 (is-torsorial-Eq-full-binary-tree leaf-full-binary-tree)
+  (join-full-binary-tree U U₁ , ())
+pr2 (is-torsorial-Eq-full-binary-tree (join-full-binary-tree T T₁))
+  (leaf-full-binary-tree , ())
+pr2 (is-torsorial-Eq-full-binary-tree (join-full-binary-tree T T₁))
+  (join-full-binary-tree U U₁ , p , q) =
+    ap-binary (map-total-Eq-full-binary-tree T T₁)
+    ( pr2 (is-torsorial-Eq-full-binary-tree T) (U , p))
+    ( pr2 (is-torsorial-Eq-full-binary-tree T₁) (U₁ , q))
+
+is-equiv-Eq-eq-full-binary-tree :
+  {U V : full-binary-tree} → is-equiv (Eq-eq-full-binary-tree {U} {V})
+is-equiv-Eq-eq-full-binary-tree {U} {V} =
+  fundamental-theorem-id
+  ( is-torsorial-Eq-full-binary-tree U)
+  ( λ T p → Eq-eq-full-binary-tree p)
+  ( V)
+```
+
+### The type of full binary trees has decidable equality
+
+```agda
+is-decidable-Eq-full-binary-tree :
+  (U V : full-binary-tree) → is-decidable (Eq-full-binary-tree U V)
+is-decidable-Eq-full-binary-tree leaf-full-binary-tree leaf-full-binary-tree =
+  inl star
+is-decidable-Eq-full-binary-tree
+  leaf-full-binary-tree (join-full-binary-tree V V₁) =
+    inr (λ ())
+is-decidable-Eq-full-binary-tree
+  (join-full-binary-tree U U₁) leaf-full-binary-tree =
+    inr (λ ())
+is-decidable-Eq-full-binary-tree (join-full-binary-tree U U₁) (join-full-binary-tree V V₁) with is-decidable-Eq-full-binary-tree U V | is-decidable-Eq-full-binary-tree U₁ V₁
+... | inl p | inl q = inl (pair p q)
+... | inl p | inr q = inr (λ z → q (pr2 z))
+... | inr p | inl q = inr (λ z → p (pr1 z))
+... | inr p | inr q = inr (λ z → p (pr1 z))
+
+has-decidable-equality-full-binary-tree :
+  has-decidable-equality full-binary-tree
+has-decidable-equality-full-binary-tree U V =
+  is-decidable-iff
+  ( eq-Eq-full-binary-tree U V)
+  ( Eq-eq-full-binary-tree)
+  ( is-decidable-Eq-full-binary-tree U V)
+
+is-set-full-binary-tree : is-set full-binary-tree
+is-set-full-binary-tree =
+  is-set-has-decidable-equality has-decidable-equality-full-binary-tree
+
+full-binary-tree-Set : Set lzero
+pr1 full-binary-tree-Set = full-binary-tree
+pr2 full-binary-tree-Set = is-set-full-binary-tree
+```
diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md
new file mode 100644
index 0000000000..ee052ba36e
--- /dev/null
+++ b/src/trees/labeled-full-binary-trees.lagda.md
@@ -0,0 +1,301 @@
+# Labeled full binary trees
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module trees.labeled-full-binary-trees where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.function-extensionality
+open import foundation.homotopy-induction
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
+open import foundation.transport-along-higher-identifications
+open import foundation.transport-along-identifications-dependent-functions
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.cartesian-product-types
+open import foundation-core.coproduct-types
+open import foundation-core.contractible-types
+open import foundation-core.dependent-identifications
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+
+open import trees.full-binary-trees
+```
+
+</details>
+
+## Idea
+
+For a type `X`, an
+{{#concept "`X`-labeling" Disambiguation="of full binary trees" Agda=labeling-full-binary-tree}}
+of a [full binary tree](trees.full-binary-trees.md) `T` is a map from the nodes
+of `T` to `X`. A
+{{#concept "labeled full binary tree" Agda=labeled-full-binary-tree}} is a pair
+of a full binary tree and a labeling.
+
+## Definition
+
+```agda
+module _
+  {l : Level} (X : UU l)
+  where
+
+  labeling-full-binary-tree : (T : full-binary-tree) → UU l
+  labeling-full-binary-tree T = node-full-binary-tree T → X
+
+  labeled-full-binary-tree : UU l
+  labeled-full-binary-tree =
+    Σ full-binary-tree (λ T → labeling-full-binary-tree T)
+
+  tree-labeled-full-binary-tree : labeled-full-binary-tree → full-binary-tree
+  tree-labeled-full-binary-tree = pr1
+
+  labeling-labeled-full-binary-tree :
+    (T : labeled-full-binary-tree) →
+    labeling-full-binary-tree (tree-labeled-full-binary-tree T)
+  labeling-labeled-full-binary-tree T = pr2 T
+```
+
+### The weight of a labeled full binary tree
+
+This is simply the weight of its underlying full binary tree.
+
+```agda
+  weight-labeled-full-binary-tree : labeled-full-binary-tree → ℕ
+  weight-labeled-full-binary-tree (T , _) = weight-full-binary-tree T
+```
+
+### Characterizing identifications of labeled full binary trees
+
+```agda
+module _
+  {l : Level} (X : UU l)
+  where
+
+  {-# TERMINATING #-}
+  htpy-labeled-full-binary-tree :
+    (U V : labeled-full-binary-tree X) →
+    Eq-full-binary-tree
+      (tree-labeled-full-binary-tree X U)
+      (tree-labeled-full-binary-tree X V) →
+    UU l
+  htpy-labeled-full-binary-tree
+    (leaf-full-binary-tree , f) (leaf-full-binary-tree , g) star =
+      f star ＝ g star
+  htpy-labeled-full-binary-tree
+    (join-full-binary-tree U U₁ , f) (join-full-binary-tree V V₁ , g) (p , q) =
+      ( htpy-labeled-full-binary-tree
+        ( U , (λ z → f (inl z))) (V , (λ z → g (inl z))) p) ×
+      ( htpy-labeled-full-binary-tree
+        ( U₁ , (λ z → f (inr z))) (V₁ , (λ z → g (inr z))) q)
+
+  {-# TERMINATING #-}
+  refl-htpy-labeled-full-binary-tree :
+    (T : labeled-full-binary-tree X) →
+    htpy-labeled-full-binary-tree T T
+      (refl-Eq-full-binary-tree (tree-labeled-full-binary-tree X T))
+  refl-htpy-labeled-full-binary-tree (leaf-full-binary-tree , f) = refl
+  pr1 (refl-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) =
+    refl-htpy-labeled-full-binary-tree (T , λ z → f (inl z))
+  pr2 (refl-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) =
+    refl-htpy-labeled-full-binary-tree (T₁ , λ z → f (inr z))
+
+  Eq-labeled-full-binary-tree :
+    labeled-full-binary-tree X → labeled-full-binary-tree X → UU l
+  Eq-labeled-full-binary-tree U V =
+    Σ ( Eq-full-binary-tree
+        ( tree-labeled-full-binary-tree X U)
+        ( tree-labeled-full-binary-tree X V))
+      ( htpy-labeled-full-binary-tree U V)
+
+  refl-Eq-labeled-full-binary-tree :
+    (T : labeled-full-binary-tree X) → Eq-labeled-full-binary-tree T T
+  refl-Eq-labeled-full-binary-tree (leaf-full-binary-tree , f) = (star , refl)
+  pr1 (refl-Eq-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) =
+    ( refl-Eq-full-binary-tree T , refl-Eq-full-binary-tree T₁)
+  pr2 (refl-Eq-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) =
+    refl-htpy-labeled-full-binary-tree ((join-full-binary-tree T T₁) , f)
+
+  Eq-eq-labeled-full-binary-tree :
+    (U V : labeled-full-binary-tree X) → U ＝ V →
+    Eq-labeled-full-binary-tree U V
+  Eq-eq-labeled-full-binary-tree U .U refl = refl-Eq-labeled-full-binary-tree U
+
+  htpy-eq-labeled-full-binary-tree :
+    (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → f ＝ g →
+    htpy-labeled-full-binary-tree (T , f) (T , g) (refl-Eq-full-binary-tree T)
+  htpy-eq-labeled-full-binary-tree T f .f refl =
+    refl-htpy-labeled-full-binary-tree (T , f)
+
+  htpy-refl-labeled-full-binary-tree :
+    (T : full-binary-tree) (f g : labeling-full-binary-tree X T) →
+    htpy-labeled-full-binary-tree (T , f) (T , g) (refl-Eq-full-binary-tree T) →
+    f ~ g
+  htpy-refl-labeled-full-binary-tree leaf-full-binary-tree f g p star = p
+  htpy-refl-labeled-full-binary-tree (join-full-binary-tree T T₁) f g (p , q) (inl x) =
+    htpy-refl-labeled-full-binary-tree
+      ( T)
+      ( λ z → f (inl z))
+      ( λ z → g (inl z))
+      ( p)
+      ( x)
+  htpy-refl-labeled-full-binary-tree (join-full-binary-tree T T₁) f g (p , q) (inr x) =
+    htpy-refl-labeled-full-binary-tree
+      ( T₁)
+      ( λ z → f (inr z))
+      ( λ z → g (inr z))
+      ( q)
+      ( x)
+
+  htpy'-refl-labeled-full-binary-tree :
+    (T : full-binary-tree) (f g : labeling-full-binary-tree X T) →
+    f ~ g →
+    htpy-labeled-full-binary-tree (T , f) (T , g) (refl-Eq-full-binary-tree T)
+  htpy'-refl-labeled-full-binary-tree leaf-full-binary-tree f g p = p star
+  pr1 (htpy'-refl-labeled-full-binary-tree (join-full-binary-tree T T₁) f g p) =
+    htpy'-refl-labeled-full-binary-tree
+      ( T)
+      ( λ z → f (inl z))
+      ( λ z → g (inl z))
+      ( λ x → p (inl x))
+  pr2 (htpy'-refl-labeled-full-binary-tree (join-full-binary-tree T T₁) f g p) =
+    htpy'-refl-labeled-full-binary-tree
+      ( T₁)
+      ( λ z → f (inr z))
+      ( λ z → g (inr z))
+      ( λ x → p (inr x))
+
+  lemma-refl-htpy-labeled-full-binary-tree :
+    (T : full-binary-tree) (f : labeling-full-binary-tree X T) →
+    htpy-refl-labeled-full-binary-tree T f f
+      (htpy'-refl-labeled-full-binary-tree T f f refl-htpy) ~
+    refl-htpy
+  lemma-refl-htpy-labeled-full-binary-tree leaf-full-binary-tree f star = refl
+  lemma-refl-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁) f (inl x) =
+    lemma-refl-htpy-labeled-full-binary-tree T (λ z → f (inl z)) x
+  lemma-refl-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁) f (inr x) =
+    lemma-refl-htpy-labeled-full-binary-tree T₁ (λ z → f (inr z)) x
+
+  equiv-htpy'-refl-labeled-full-binary-tree :
+    (T : full-binary-tree) (f g : labeling-full-binary-tree X T) →
+    (f ~ g) ≃
+    htpy-labeled-full-binary-tree (T , f) (T , g) (refl-Eq-full-binary-tree T)
+  pr1 (equiv-htpy'-refl-labeled-full-binary-tree T f g) =
+    htpy'-refl-labeled-full-binary-tree T f g
+  pr1 (pr1 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree T f g))) =
+    htpy-refl-labeled-full-binary-tree T f g
+  pr2 (pr1 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree
+    leaf-full-binary-tree f g))) p = refl
+  pr2 (pr1 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree
+    (join-full-binary-tree T T₁) f g))) (p , q) =
+    eq-pair
+    ( pr2
+      ( pr1
+        ( pr2
+          ( equiv-htpy'-refl-labeled-full-binary-tree T (λ z → f (inl z))
+            ( λ z → g (inl z)))))
+      ( p))
+    ( pr2
+      ( pr1
+        ( pr2
+          ( equiv-htpy'-refl-labeled-full-binary-tree T₁ (λ z → f (inr z))
+            ( λ z → g (inr z)))))
+      ( q))
+  pr1 (pr2 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree T f g))) =
+    htpy-refl-labeled-full-binary-tree T f g
+  pr2 (pr2 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree
+    leaf-full-binary-tree f g))) p =
+    eq-htpy (λ x → refl)
+  pr2 (pr2 (pr2 (equiv-htpy'-refl-labeled-full-binary-tree
+    (join-full-binary-tree T T₁) f g))) =
+    ind-htpy
+      ( f)
+      ( λ h q →
+        htpy-refl-labeled-full-binary-tree
+          ( join-full-binary-tree T T₁)
+          ( f)
+          ( h)
+          ( htpy'-refl-labeled-full-binary-tree
+            ( join-full-binary-tree T T₁)
+            ( f)
+            ( h)
+            ( q)) ＝
+        q)
+      ( eq-htpy
+        ( lemma-refl-htpy-labeled-full-binary-tree
+          ( join-full-binary-tree T T₁)
+          ( f)))
+
+  abstract
+    is-torsorial-htpy-labeled-full-binary-tree :
+      (T : full-binary-tree) (f : labeling-full-binary-tree X T) →
+      is-torsorial (λ g → htpy-labeled-full-binary-tree (T , f) (T , g)
+        (refl-Eq-full-binary-tree T))
+    is-torsorial-htpy-labeled-full-binary-tree T f =
+      is-contr-equiv'
+        ( Σ (labeling-full-binary-tree X T) (_~_ f))
+        ( equiv-tot (equiv-htpy'-refl-labeled-full-binary-tree T f))
+        ( is-torsorial-htpy f)
+
+  is-equiv-htpy-eq-labeled-full-binary-tree :
+    (T : full-binary-tree) (f g : labeling-full-binary-tree X T) →
+    is-equiv (htpy-eq-labeled-full-binary-tree T f g)
+  is-equiv-htpy-eq-labeled-full-binary-tree T f =
+    fundamental-theorem-id
+    ( is-torsorial-htpy-labeled-full-binary-tree T f)
+    ( htpy-eq-labeled-full-binary-tree T f)
+
+  is-equiv-Eq-eq-labeled-full-binary-tree :
+    (U V : labeled-full-binary-tree X) →
+    is-equiv (Eq-eq-labeled-full-binary-tree U V)
+  is-equiv-Eq-eq-labeled-full-binary-tree (U , f) =
+    structure-identity-principle
+    ( λ {V} g → htpy-labeled-full-binary-tree (U , f) (V , g))
+    ( refl-Eq-full-binary-tree U)
+    ( refl-htpy-labeled-full-binary-tree (U , f))
+    ( Eq-eq-labeled-full-binary-tree (U , f))
+    ( λ _ → is-equiv-Eq-eq-full-binary-tree)
+    ( is-equiv-htpy-eq-labeled-full-binary-tree U f)
+
+  equiv-Eq-eq-labeled-full-binary-tree :
+    (U V : labeled-full-binary-tree X) →
+    (U ＝ V) ≃ Eq-labeled-full-binary-tree U V
+  pr1 (equiv-Eq-eq-labeled-full-binary-tree U V) =
+    Eq-eq-labeled-full-binary-tree U V
+  pr2 (equiv-Eq-eq-labeled-full-binary-tree U V) =
+    is-equiv-Eq-eq-labeled-full-binary-tree U V
+
+  eq-Eq-labeled-full-binary-tree :
+    (U V : labeled-full-binary-tree X) →
+    Eq-labeled-full-binary-tree U V → U ＝ V
+  eq-Eq-labeled-full-binary-tree U V =
+    map-inv-equiv (equiv-Eq-eq-labeled-full-binary-tree U V)
+
+  compute-Eq-eq-labeled-full-binary-tree :
+    (U : labeled-full-binary-tree X) →
+    Eq-eq-labeled-full-binary-tree U U refl ＝
+    refl-Eq-labeled-full-binary-tree U
+  compute-Eq-eq-labeled-full-binary-tree _ = refl
+```