From 37236bc616d56ee32d484bf1a37faca9501e1701 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 16 Nov 2024 11:20:31 -0700 Subject: [PATCH 01/63] changed apostrophes to breves in incidence algebras file --- src/order-theory/incidence-algebras.lagda.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/order-theory/incidence-algebras.lagda.md b/src/order-theory/incidence-algebras.lagda.md index 3ce4a89e69..f96b061659 100644 --- a/src/order-theory/incidence-algebras.lagda.md +++ b/src/order-theory/incidence-algebras.lagda.md @@ -24,13 +24,13 @@ open import order-theory.posets ## Idea -For a [locally finite poset](order-theory.locally-finite-posets.md) 'P' and -[commutative ring](commutative-algebra.commutative-rings.md) 'R', there is a -canonical 'R'-associative algebra whose underlying 'R'-module are the set-maps -from the nonempty [intervals](order-theory.interval-subposets.md) of 'P' to 'R' +For a [locally finite poset](order-theory.locally-finite-posets.md) `P` and +[commutative ring](commutative-algebra.commutative-rings.md) `R`, there is a +canonical `R`-associative algebra whose underlying `R`-module are the set-maps +from the nonempty [intervals](order-theory.interval-subposets.md) of `P` to `R` (which we constructify as the inhabited intervals), and whose multiplication is -given by a "convolution" of maps. This is the **incidence algebra** of 'P' over -'R'. +given by a "convolution" of maps. This is the **incidence algebra** of `P` over +`R`. ## Definition From 60d18785f918b18a3e353fe51a1289e6a5a9ceb5 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:14:30 -0600 Subject: [PATCH 02/63] punctuation --- src/structured-types/morphisms-magmas.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/structured-types/morphisms-magmas.lagda.md b/src/structured-types/morphisms-magmas.lagda.md index e5d3920e3b..3061cd01f5 100644 --- a/src/structured-types/morphisms-magmas.lagda.md +++ b/src/structured-types/morphisms-magmas.lagda.md @@ -19,7 +19,7 @@ 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 +preserves the binary operation. ## Definition From 70672b73cea04ad3abc5906fe2fa03e04a70a4a5 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:14:40 -0600 Subject: [PATCH 03/63] added nodes of full binary trees --- src/trees/full-binary-trees.lagda.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 72058ec915..a4aa1ed079 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -10,8 +10,11 @@ module trees.full-binary-trees where open import elementary-number-theory.natural-numbers open import foundation.empty-types +open import foundation.unit-type open import foundation.universe-levels +open import foundation-core.coproduct-types + open import univalent-combinatorics.standard-finite-types ``` @@ -35,3 +38,12 @@ 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 +``` From 96931db2896711ffbb3be29f398b1c0a1122a8ce Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:14:57 -0600 Subject: [PATCH 04/63] the combinator of full binary trees, and of labeled full binary trees --- .../combinator-full-binary-trees.lagda.md | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 src/trees/combinator-full-binary-trees.lagda.md 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..31b8eb0c1f --- /dev/null +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -0,0 +1,87 @@ +# The combinator of full binary trees + +```agda +module trees.combinator-full-binary-trees where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.isolated-elements +open import foundation.maybe +open import foundation.negation +open import foundation.propositions +open import foundation.universe-levels + +open import graph-theory.directed-graphs +open import graph-theory.morphisms-directed-graphs +open import graph-theory.walks-directed-graphs + +open import trees.bases-directed-trees +open import trees.directed-trees +open import trees.equivalences-directed-trees +open import trees.fibers-directed-trees +open import trees.full-binary-trees +open import trees.labeled-full-binary-trees +open import trees.morphisms-directed-trees + +open import elementary-number-theory.natural-numbers + +open import foundation.empty-types +open import foundation.universe-levels + +open import univalent-combinatorics.standard-finite-types + +open import structured-types.magmas +``` + +
+ +## 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). + +## 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 +``` From 4d66fdd6460249479a215540b7a0159291ba7d00 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:15:03 -0600 Subject: [PATCH 05/63] labeled full binary trees --- src/trees/labeled-full-binary-trees.lagda.md | 43 ++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 src/trees/labeled-full-binary-trees.lagda.md 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..b1c283e3c9 --- /dev/null +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -0,0 +1,43 @@ +# Labeled full binary trees + +```agda +module trees.labeled-full-binary-trees where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.universe-levels + +open import trees.full-binary-trees + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +For a type `X`, an **`X`-labeling** of a +[full binary tree](trees.full-binary-trees.md) `T` is a map from the nodes of +`T` to `X`. A **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) +``` From fb0267156acac5ef4b4978a8a267c2209399c110 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:19:16 -0600 Subject: [PATCH 06/63] the free magma on one generator (the hard direction is left!) --- .../free-magma-on-one-generator.lagda.md | 108 ++++++++++++++++++ 1 file changed, 108 insertions(+) create mode 100644 src/trees/free-magma-on-one-generator.lagda.md 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..69a6d61111 --- /dev/null +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -0,0 +1,108 @@ +# The free magma on one generator + +```agda +module trees.free-magma-on-one-generator where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.function-extensionality +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.isolated-elements +open import foundation.maybe +open import foundation.negation +open import foundation.propositions +open import foundation.universe-levels + +open import graph-theory.directed-graphs +open import graph-theory.morphisms-directed-graphs +open import graph-theory.walks-directed-graphs + +open import trees.bases-directed-trees +open import trees.combinator-full-binary-trees +open import trees.directed-trees +open import trees.equivalences-directed-trees +open import trees.fibers-directed-trees +open import trees.full-binary-trees +open import trees.labeled-full-binary-trees +open import trees.morphisms-directed-trees + +open import elementary-number-theory.natural-numbers + +open import foundation.empty-types +open import foundation.universe-levels + +open import foundation-core.dependent-identifications +open import foundation-core.retractions +open import foundation-core.sections + +open import univalent-combinatorics.standard-finite-types + +open import structured-types.magmas +open import structured-types.morphisms-magmas +``` + +
+ +## Idea + +The [magma of full binary trees](trees.combinator-full-binary-trees.md) is the +**free magma on one generator**. That is, there is an equivalence +`hom-Magma full-binary-tree-Magma M ≃ M` for any +[magma](structured-types.magmas.md) `M`. + +## 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-equiv-image-of-leaf : is-equiv image-of-leaf + pr1 (pr1 is-equiv-image-of-leaf) = + extension-of-point-hom-full-binary-tree-Magma + pr2 (pr1 is-equiv-image-of-leaf) = λ x → refl + pr1 (pr2 is-equiv-image-of-leaf) = + extension-of-point-hom-full-binary-tree-Magma + pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = eq-pair-Σ (eq-htpy htpy) {! !} + where + htpy : + pr1 (extension-of-point-hom-full-binary-tree-Magma + ( image-of-leaf (f , f-preserves))) ~ f + htpy leaf-full-binary-tree = refl + htpy (join-full-binary-tree L R) = {! !} +``` From 6c210aac758f106a7d304ba2f6b0b311dc88a8cf Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:19:29 -0600 Subject: [PATCH 07/63] formatting --- src/trees/free-magma-on-one-generator.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 69a6d61111..5c132c3174 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -98,7 +98,8 @@ module _ pr2 (pr1 is-equiv-image-of-leaf) = λ x → refl pr1 (pr2 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma - pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = eq-pair-Σ (eq-htpy htpy) {! !} + pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = + eq-pair-Σ (eq-htpy htpy) {! !} where htpy : pr1 (extension-of-point-hom-full-binary-tree-Magma From 2448542a29a4f55296169610be305d4ea02d2ea1 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:30:09 -0600 Subject: [PATCH 08/63] why can I not just apply f-preserves to the goal in htpy?... --- src/trees/free-magma-on-one-generator.lagda.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 5c132c3174..415d1eae8d 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -58,7 +58,8 @@ open import structured-types.morphisms-magmas ## Idea -The [magma of full binary trees](trees.combinator-full-binary-trees.md) is the +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 is an equivalence `hom-Magma full-binary-tree-Magma M ≃ M` for any [magma](structured-types.magmas.md) `M`. @@ -99,11 +100,16 @@ module _ pr1 (pr2 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = - eq-pair-Σ (eq-htpy htpy) {! !} + eq-pair-Σ (eq-htpy htpy) dep where htpy : pr1 (extension-of-point-hom-full-binary-tree-Magma ( image-of-leaf (f , f-preserves))) ~ f htpy leaf-full-binary-tree = refl - htpy (join-full-binary-tree L R) = {! !} + htpy (join-full-binary-tree L R) = inv {! f-preserves !} + + dep : + dependent-identification (preserves-mul-Magma full-binary-tree-Magma M) + ( eq-htpy htpy) (λ T U → refl) f-preserves + dep = {! !} ``` From cbdd7cc6f405a6c04660b254667fabc47858a645 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:33:53 -0600 Subject: [PATCH 09/63] formatting --- src/trees/free-magma-on-one-generator.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 415d1eae8d..689b421c98 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -96,7 +96,7 @@ module _ is-equiv-image-of-leaf : is-equiv image-of-leaf pr1 (pr1 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma - pr2 (pr1 is-equiv-image-of-leaf) = λ x → refl + pr2 (pr1 is-equiv-image-of-leaf) _ = refl pr1 (pr2 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = From 81ab2d71a0865ae51073e460da1c0c3a25aa93c8 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:35:51 -0600 Subject: [PATCH 10/63] commented out one attempt. could still work, but may be useful to factor out an eq-htpy-hom-Magma block in morphisms-magmas --- src/trees/free-magma-on-one-generator.lagda.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 689b421c98..64ea90073e 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -99,7 +99,9 @@ module _ pr2 (pr1 is-equiv-image-of-leaf) _ = refl pr1 (pr2 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma - pr2 (pr2 is-equiv-image-of-leaf) (f , f-preserves) = + pr2 (pr2 is-equiv-image-of-leaf) f = {! !} + +{- eq-pair-Σ (eq-htpy htpy) dep where htpy : @@ -112,4 +114,5 @@ module _ dependent-identification (preserves-mul-Magma full-binary-tree-Magma M) ( eq-htpy htpy) (λ T U → refl) f-preserves dep = {! !} +-} ``` From 98ab6fe8157e1154bf5f686e3b3dcebc58284cfe Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 21:40:38 -0600 Subject: [PATCH 11/63] pre-commit, with goals commented out, and pruned imports --- src/trees.lagda.md | 3 ++ .../combinator-full-binary-trees.lagda.md | 31 +--------------- .../free-magma-on-one-generator.lagda.md | 36 +++++-------------- src/trees/full-binary-trees.lagda.md | 5 --- src/trees/labeled-full-binary-trees.lagda.md | 5 --- 5 files changed, 12 insertions(+), 68 deletions(-) diff --git a/src/trees.lagda.md b/src/trees.lagda.md index 4da5e8d445..75bfbc3648 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,7 @@ 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.full-binary-trees public open import trees.functoriality-combinator-directed-trees public open import trees.functoriality-fiber-directed-tree public @@ -37,6 +39,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 index 31b8eb0c1f..3d6e382f75 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -7,44 +7,15 @@ module trees.combinator-full-binary-trees where
Imports ```agda -open import foundation.action-on-identifications-functions -open import foundation.contractible-types open import foundation.coproduct-types -open import foundation.decidable-types open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.equality-dependent-pair-types -open import foundation.equivalences -open import foundation.function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.identity-types -open import foundation.isolated-elements -open import foundation.maybe -open import foundation.negation -open import foundation.propositions open import foundation.universe-levels -open import graph-theory.directed-graphs -open import graph-theory.morphisms-directed-graphs -open import graph-theory.walks-directed-graphs +open import structured-types.magmas -open import trees.bases-directed-trees -open import trees.directed-trees -open import trees.equivalences-directed-trees -open import trees.fibers-directed-trees open import trees.full-binary-trees open import trees.labeled-full-binary-trees -open import trees.morphisms-directed-trees - -open import elementary-number-theory.natural-numbers - -open import foundation.empty-types -open import foundation.universe-levels - -open import univalent-combinatorics.standard-finite-types - -open import structured-types.magmas ```
diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 64ea90073e..caed54d4ba 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -8,50 +8,26 @@ module trees.free-magma-on-one-generator where ```agda open import foundation.action-on-identifications-functions -open import foundation.contractible-types open import foundation.coproduct-types -open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.function-types open import foundation.function-extensionality -open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types -open import foundation.isolated-elements -open import foundation.maybe -open import foundation.negation -open import foundation.propositions -open import foundation.universe-levels - -open import graph-theory.directed-graphs -open import graph-theory.morphisms-directed-graphs -open import graph-theory.walks-directed-graphs - -open import trees.bases-directed-trees -open import trees.combinator-full-binary-trees -open import trees.directed-trees -open import trees.equivalences-directed-trees -open import trees.fibers-directed-trees -open import trees.full-binary-trees -open import trees.labeled-full-binary-trees -open import trees.morphisms-directed-trees - -open import elementary-number-theory.natural-numbers - -open import foundation.empty-types open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.retractions open import foundation-core.sections -open import univalent-combinatorics.standard-finite-types - 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 ``` @@ -93,6 +69,8 @@ module _ pr2 (extension-of-point-hom-full-binary-tree-Magma m) = is-hom-extension-of-point-full-binary-tree-Magma m +{- + is-equiv-image-of-leaf : is-equiv image-of-leaf pr1 (pr1 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma @@ -101,6 +79,8 @@ module _ extension-of-point-hom-full-binary-tree-Magma pr2 (pr2 is-equiv-image-of-leaf) f = {! !} +-} + {- eq-pair-Σ (eq-htpy htpy) dep where diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index a4aa1ed079..d0db428966 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -7,15 +7,10 @@ module trees.full-binary-trees where
Imports ```agda -open import elementary-number-theory.natural-numbers - -open import foundation.empty-types open import foundation.unit-type open import foundation.universe-levels open import foundation-core.coproduct-types - -open import univalent-combinatorics.standard-finite-types ```
diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index b1c283e3c9..2d954c624d 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -7,15 +7,10 @@ module trees.labeled-full-binary-trees where
Imports ```agda -open import elementary-number-theory.natural-numbers - open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.universe-levels open import trees.full-binary-trees - -open import univalent-combinatorics.standard-finite-types ```
From c3d619e244ef2d42bdb2c08a3505d1607747ca4d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 22:20:17 -0600 Subject: [PATCH 12/63] for some reason, the termination checker really dislikes the recursive definition for extension-of-map-labeled-full-binary-tree-Magma... --- src/trees/free-magmas-on-a-type.lagda.md | 70 ++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 src/trees/free-magmas-on-a-type.lagda.md diff --git a/src/trees/free-magmas-on-a-type.lagda.md b/src/trees/free-magmas-on-a-type.lagda.md new file mode 100644 index 0000000000..8d47af8296 --- /dev/null +++ b/src/trees/free-magmas-on-a-type.lagda.md @@ -0,0 +1,70 @@ +# The free magma on `X` + +```agda +module trees.free-magmas-on-a-type where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-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.unit-type +open import foundation.universe-levels + +open import foundation-core.dependent-identifications +open import foundation-core.retractions +open import foundation-core.sections + +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 +``` + +
+ +## 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 [`X`-labeled full binary trees](trees.labeled-full-binary-trees.md) +the \*\*free magma on `X`. That is, for any [magma](structured-types.magmas.md) +`M` and any type `X`, the map +`(hom-Magma (labeled-full-binary-tree-Magma X) M) → (X → type-Magma M)` pulling +back the label of `leaf-full-binary-tree` is an equivalence. + +## Proof + +```agda +module _ + {l1 l2 : Level} (X : UU l1) (M : Magma l2) + where + + label-of-leaf : + hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) + label-of-leaf (f , _) x = f (leaf-full-binary-tree , λ _ → x) + + 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) = f (label star) + extension-of-map-labeled-full-binary-tree-Magma f + ( join-full-binary-tree L R , label) = + mul-Magma M (extension-of-map-labeled-full-binary-tree-Magma f (L , λ z → label (inl z))) (extension-of-map-labeled-full-binary-tree-Magma f (R , λ z → label (inr z))) + + 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 f T U = {! !} +``` From 89eec7609a2b6146ee87e75b9ae3c6ddfaf75d9d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 22:20:55 -0600 Subject: [PATCH 13/63] formatting --- src/trees/free-magmas-on-a-type.lagda.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/trees/free-magmas-on-a-type.lagda.md b/src/trees/free-magmas-on-a-type.lagda.md index 8d47af8296..1db0ec26ea 100644 --- a/src/trees/free-magmas-on-a-type.lagda.md +++ b/src/trees/free-magmas-on-a-type.lagda.md @@ -60,7 +60,11 @@ module _ ( leaf-full-binary-tree , label) = f (label star) extension-of-map-labeled-full-binary-tree-Magma f ( join-full-binary-tree L R , label) = - mul-Magma M (extension-of-map-labeled-full-binary-tree-Magma f (L , λ z → label (inl z))) (extension-of-map-labeled-full-binary-tree-Magma f (R , λ z → label (inr z))) + mul-Magma M + ( extension-of-map-labeled-full-binary-tree-Magma f + ( L , λ z → label (inl z))) + ( extension-of-map-labeled-full-binary-tree-Magma f + ( R , λ z → label (inr z))) is-hom-extension-of-map-labeled-full-binary-tree-Magma : ( f : X → type-Magma M) → preserves-mul-Magma From 976e8492926fa64ab7019a5117206bad77c852d0 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 22:23:54 -0600 Subject: [PATCH 14/63] reopened goal --- src/trees/free-magma-on-one-generator.lagda.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index caed54d4ba..1512c162a7 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -69,8 +69,6 @@ module _ pr2 (extension-of-point-hom-full-binary-tree-Magma m) = is-hom-extension-of-point-full-binary-tree-Magma m -{- - is-equiv-image-of-leaf : is-equiv image-of-leaf pr1 (pr1 is-equiv-image-of-leaf) = extension-of-point-hom-full-binary-tree-Magma @@ -79,8 +77,6 @@ module _ extension-of-point-hom-full-binary-tree-Magma pr2 (pr2 is-equiv-image-of-leaf) f = {! !} --} - {- eq-pair-Σ (eq-htpy htpy) dep where From 37f3ab0937f2ca77e50a5d85341eb6e2cac9a08d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 26 Jul 2025 22:59:41 -0600 Subject: [PATCH 15/63] so odd... --- .../free-magma-on-one-generator.lagda.md | 30 +++++++++---------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 1512c162a7..46c82ef03a 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -21,6 +21,8 @@ open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.retractions open import foundation-core.sections +open import foundation-core.propositions +open import foundation-core.sets open import structured-types.magmas open import structured-types.morphisms-magmas @@ -36,9 +38,10 @@ open import trees.labeled-full-binary-trees 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 is an equivalence -`hom-Magma full-binary-tree-Magma M ≃ M` for any -[magma](structured-types.magmas.md) `M`. +**free magma on one generator**. That is, there are natural maps +`hom-Magma full-binary-tree-Magma M → M, M → hom-Magma full-binary-tree-Magma M` +for any [magma](structured-types.magmas.md) `M`, and when `M` is a set, we may +prove these form an equivalence. ## Proof @@ -69,26 +72,21 @@ module _ pr2 (extension-of-point-hom-full-binary-tree-Magma m) = is-hom-extension-of-point-full-binary-tree-Magma m - is-equiv-image-of-leaf : is-equiv image-of-leaf - pr1 (pr1 is-equiv-image-of-leaf) = - extension-of-point-hom-full-binary-tree-Magma - pr2 (pr1 is-equiv-image-of-leaf) _ = refl - pr1 (pr2 is-equiv-image-of-leaf) = - extension-of-point-hom-full-binary-tree-Magma - pr2 (pr2 is-equiv-image-of-leaf) f = {! !} - -{- + is-equiv-image-of-leaf : is-set (type-Magma M) → is-equiv image-of-leaf + pr1 (pr1 (is-equiv-image-of-leaf _)) = extension-of-point-hom-full-binary-tree-Magma + pr2 (pr1 (is-equiv-image-of-leaf _)) _ = refl + pr1 (pr2 (is-equiv-image-of-leaf _)) = extension-of-point-hom-full-binary-tree-Magma + pr2 (pr2 (is-equiv-image-of-leaf M-set)) (f , f-hom) = eq-pair-Σ (eq-htpy htpy) dep where htpy : pr1 (extension-of-point-hom-full-binary-tree-Magma - ( image-of-leaf (f , f-preserves))) ~ f + ( image-of-leaf (f , f-hom))) ~ f htpy leaf-full-binary-tree = refl - htpy (join-full-binary-tree L R) = inv {! f-preserves !} + htpy (join-full-binary-tree L R) = inv {! f-hom L R !} dep : dependent-identification (preserves-mul-Magma full-binary-tree-Magma M) - ( eq-htpy htpy) (λ T U → refl) f-preserves + ( eq-htpy htpy) (λ T U → refl) f-hom dep = {! !} --} ``` From 64110344baa5b7a9b1d547032bd1bac21e64152e Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 11:18:41 -0600 Subject: [PATCH 16/63] the free magma on one generator! its universal property is only proved for set-magmas, unfortunately, though I don't know how to upgrade this --- .../free-magma-on-one-generator.lagda.md | 91 +++++++++++++++---- 1 file changed, 71 insertions(+), 20 deletions(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 46c82ef03a..49f38260a4 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -7,6 +7,7 @@ module trees.free-magma-on-one-generator where
Imports ```agda +open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types @@ -19,10 +20,12 @@ open import foundation.identity-types open import foundation.universe-levels open import foundation-core.dependent-identifications +open import foundation-core.function-types open import foundation-core.retractions open import foundation-core.sections open import foundation-core.propositions open import foundation-core.sets +open import foundation-core.transport-along-identifications open import structured-types.magmas open import structured-types.morphisms-magmas @@ -39,9 +42,12 @@ open import trees.labeled-full-binary-trees 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 -`hom-Magma full-binary-tree-Magma M → M, M → hom-Magma full-binary-tree-Magma M` -for any [magma](structured-types.magmas.md) `M`, and when `M` is a set, we may -prove these form an equivalence. +`image-of-leaf : hom-Magma full-binary-tree-Magma M → M, extension-of-point-hom-full-binary-tree-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 @@ -72,21 +78,66 @@ module _ pr2 (extension-of-point-hom-full-binary-tree-Magma m) = is-hom-extension-of-point-full-binary-tree-Magma m - is-equiv-image-of-leaf : is-set (type-Magma M) → is-equiv image-of-leaf - pr1 (pr1 (is-equiv-image-of-leaf _)) = extension-of-point-hom-full-binary-tree-Magma - pr2 (pr1 (is-equiv-image-of-leaf _)) _ = refl - pr1 (pr2 (is-equiv-image-of-leaf _)) = extension-of-point-hom-full-binary-tree-Magma - pr2 (pr2 (is-equiv-image-of-leaf M-set)) (f , f-hom) = - eq-pair-Σ (eq-htpy htpy) dep - where - htpy : - pr1 (extension-of-point-hom-full-binary-tree-Magma - ( image-of-leaf (f , f-hom))) ~ f - htpy leaf-full-binary-tree = refl - htpy (join-full-binary-tree L R) = inv {! f-hom L R !} - - dep : - dependent-identification (preserves-mul-Magma full-binary-tree-Magma M) - ( eq-htpy htpy) (λ T U → refl) f-hom - dep = {! !} + 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 ``` From 8c778629e18ad500430e707ab1cd272321d2a717 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 11:19:29 -0600 Subject: [PATCH 17/63] pre-commit hooks --- src/trees.lagda.md | 1 + src/trees/free-magma-on-one-generator.lagda.md | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/trees.lagda.md b/src/trees.lagda.md index 75bfbc3648..e6e10c49c5 100644 --- a/src/trees.lagda.md +++ b/src/trees.lagda.md @@ -31,6 +31,7 @@ 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-a-type public open import trees.full-binary-trees public open import trees.functoriality-combinator-directed-trees public open import trees.functoriality-fiber-directed-tree public diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 49f38260a4..729a535200 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -21,9 +21,9 @@ open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.function-types +open import foundation-core.propositions open import foundation-core.retractions open import foundation-core.sections -open import foundation-core.propositions open import foundation-core.sets open import foundation-core.transport-along-identifications @@ -110,7 +110,8 @@ module _ 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 → + 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 From 7f824d39dfcee291063f387a85d40d6b14d1319c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 11:28:45 -0600 Subject: [PATCH 18/63] formatting, removing free magma on a general type (for now, hopefully) --- .../combinator-full-binary-trees.lagda.md | 3 +- .../free-magma-on-one-generator.lagda.md | 7 ----- src/trees/free-magmas-on-a-type.lagda.md | 30 ++----------------- src/trees/labeled-full-binary-trees.lagda.md | 9 +++--- 4 files changed, 9 insertions(+), 40 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 3d6e382f75..40fc9f21ae 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -25,7 +25,8 @@ open import trees.labeled-full-binary-trees 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). +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). ## Definition diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 729a535200..885bb82291 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -8,10 +8,7 @@ module trees.free-magma-on-one-generator where ```agda open import foundation.action-on-identifications-binary-functions -open import foundation.action-on-identifications-functions -open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.empty-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality @@ -20,10 +17,6 @@ open import foundation.identity-types open import foundation.universe-levels open import foundation-core.dependent-identifications -open import foundation-core.function-types -open import foundation-core.propositions -open import foundation-core.retractions -open import foundation-core.sections open import foundation-core.sets open import foundation-core.transport-along-identifications diff --git a/src/trees/free-magmas-on-a-type.lagda.md b/src/trees/free-magmas-on-a-type.lagda.md index 1db0ec26ea..e26ea32f8b 100644 --- a/src/trees/free-magmas-on-a-type.lagda.md +++ b/src/trees/free-magmas-on-a-type.lagda.md @@ -38,37 +38,11 @@ open import trees.labeled-full-binary-trees 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 [`X`-labeled full binary trees](trees.labeled-full-binary-trees.md) -the \*\*free magma on `X`. That is, for any [magma](structured-types.magmas.md) +the **free magma on `X`**. That is, for any [magma](structured-types.magmas.md) `M` and any type `X`, the map `(hom-Magma (labeled-full-binary-tree-Magma X) M) → (X → type-Magma M)` pulling back the label of `leaf-full-binary-tree` is an equivalence. ## Proof -```agda -module _ - {l1 l2 : Level} (X : UU l1) (M : Magma l2) - where - - label-of-leaf : - hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) - label-of-leaf (f , _) x = f (leaf-full-binary-tree , λ _ → x) - - 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) = f (label star) - extension-of-map-labeled-full-binary-tree-Magma f - ( join-full-binary-tree L R , label) = - mul-Magma M - ( extension-of-map-labeled-full-binary-tree-Magma f - ( L , λ z → label (inl z))) - ( extension-of-map-labeled-full-binary-tree-Magma f - ( R , λ z → label (inr z))) - - 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 f T U = {! !} -``` +This remains to be shown. diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 2d954c624d..9703693d8c 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -17,10 +17,11 @@ open import trees.full-binary-trees ## Idea -For a type `X`, an **`X`-labeling** of a -[full binary tree](trees.full-binary-trees.md) `T` is a map from the nodes of -`T` to `X`. A **labeled full binary tree** is a pair of a full binary tree and a -labeling. +For a type `X`, an {{concept "`X`-labeling" 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 From d218fe63394f17159f5f919a1f0c9488354b238f Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 11:33:05 -0600 Subject: [PATCH 19/63] link to the free magma on one generator subarticle in the nLab --- src/trees/free-magma-on-one-generator.lagda.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 885bb82291..a18412b604 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -135,3 +135,7 @@ module _ 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 ``` + +## External links + +[Free magmas](https://ncatlab.org/nlab/show/magma#free_magmas) at $n$Lab From d932f1c4f95dacb3010e4083fc43a4e58b3cad51 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 11:43:45 -0600 Subject: [PATCH 20/63] changed `M` to `type-Magma M` in Idea --- src/trees/free-magma-on-one-generator.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index a18412b604..c01d85dcfa 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -35,7 +35,7 @@ open import trees.labeled-full-binary-trees 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 → M, extension-of-point-hom-full-binary-tree-Magma : M → hom-Magma full-binary-tree-Magma M` +`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 From a42eaf687288b4c7f8eca782f46fa7efb13bb4e6 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 12:16:31 -0600 Subject: [PATCH 21/63] whoops --- src/trees/combinator-full-binary-trees.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 40fc9f21ae..8c1677a172 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -26,7 +26,7 @@ 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). +[the free magma on one generator](trees.free-magma-on-one-generator.md). ## Definition From 221cb1009cf20d248c91df16fd221f24650a3027 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 12:25:18 -0600 Subject: [PATCH 22/63] deleted incomplete "free magmas on a type" file; termination checker was unhappy and I'd like to contribute what is working --- src/trees/free-magmas-on-a-type.lagda.md | 48 ------------------------ 1 file changed, 48 deletions(-) delete mode 100644 src/trees/free-magmas-on-a-type.lagda.md diff --git a/src/trees/free-magmas-on-a-type.lagda.md b/src/trees/free-magmas-on-a-type.lagda.md deleted file mode 100644 index e26ea32f8b..0000000000 --- a/src/trees/free-magmas-on-a-type.lagda.md +++ /dev/null @@ -1,48 +0,0 @@ -# The free magma on `X` - -```agda -module trees.free-magmas-on-a-type where -``` - -
Imports - -```agda -open import foundation.action-on-identifications-functions -open import foundation.coproduct-types -open import foundation.dependent-pair-types -open import foundation.empty-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.unit-type -open import foundation.universe-levels - -open import foundation-core.dependent-identifications -open import foundation-core.retractions -open import foundation-core.sections - -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 -``` - -
- -## 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 [`X`-labeled full binary trees](trees.labeled-full-binary-trees.md) -the **free magma on `X`**. That is, for any [magma](structured-types.magmas.md) -`M` and any type `X`, the map -`(hom-Magma (labeled-full-binary-tree-Magma X) M) → (X → type-Magma M)` pulling -back the label of `leaf-full-binary-tree` is an equivalence. - -## Proof - -This remains to be shown. From 927b88fead39f96acae0db04892ba89b02ac3c8a Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 27 Jul 2025 12:28:06 -0600 Subject: [PATCH 23/63] pre-commit hooks --- src/trees.lagda.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/trees.lagda.md b/src/trees.lagda.md index e6e10c49c5..75bfbc3648 100644 --- a/src/trees.lagda.md +++ b/src/trees.lagda.md @@ -31,7 +31,6 @@ 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-a-type public open import trees.full-binary-trees public open import trees.functoriality-combinator-directed-trees public open import trees.functoriality-fiber-directed-tree public From 901aa879c546e24b41d5f4bdbd17bceb024f23a2 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 2 Aug 2025 13:24:44 -0600 Subject: [PATCH 24/63] pruned unnecessary import --- src/trees/combinator-full-binary-trees.lagda.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 8c1677a172..ae5b9cd6de 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -9,7 +9,6 @@ module trees.combinator-full-binary-trees where ```agda open import foundation.coproduct-types open import foundation.dependent-pair-types -open import foundation.equality-dependent-pair-types open import foundation.universe-levels open import structured-types.magmas @@ -46,7 +45,7 @@ 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 +### The magmas of full binary trees and labeled full binary trees ```agda full-binary-tree-Magma : Magma lzero From f2561a0f8987aee52f2fe0571200aad7fd347c3c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 2 Aug 2025 13:37:28 -0600 Subject: [PATCH 25/63] introducing free magmas on types (with terminating flags, and again only when `M` is a set sadly) --- .../combinator-full-binary-trees.lagda.md | 3 +- .../free-magma-on-one-generator.lagda.md | 7 + src/trees/free-magmas-on-types.lagda.md | 178 ++++++++++++++++++ 3 files changed, 187 insertions(+), 1 deletion(-) create mode 100644 src/trees/free-magmas-on-types.lagda.md diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index ae5b9cd6de..6b49818fc7 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -25,7 +25,8 @@ 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). +[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 diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index c01d85dcfa..e99b8c1556 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -136,6 +136,13 @@ module _ 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 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..d6f6e4a2c4 --- /dev/null +++ b/src/trees/free-magmas-on-types.lagda.md @@ -0,0 +1,178 @@ +# Free magmas on types + +```agda +module trees.free-magmas-on-types where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-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.unit-type + +open import foundation-core.dependent-identifications +open import foundation-core.coproduct-types +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 +``` + +
+ +## 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 +`label-of-leaf : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M), extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M` +for any [magma](structured-types.magmas.md) `M` and type `X`. +`extension-of-map-labeled-full-binary-tree-Magma` is always a +[section](foundation-core.sections.md) of `label-of-leaf`, and when `M` is a +set, we may prove it is also a [retraction](foundation-core.retractions.md), +i.e. that `label-of-leaf` is an [equivalence](foundation-core.equivalences.md). + +## Proof + +```agda +module _ + {l1 l2 : Level} (X : UU l1) (M : Magma l2) + where + + label-of-leaf : + hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) + label-of-leaf (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 + + extension-of-map-hom-labeled-full-binary-tree-Magma : + ( X → type-Magma M) → hom-Magma (labeled-full-binary-tree-Magma X) M + extension-of-map-hom-labeled-full-binary-tree-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 (label-of-leaf 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 lem + where + lem : + combinator-labeled-full-binary-tree X + ( L , (λ x → label-T (inl x))) (R , (λ x → label-T (inr x))) = + (( join-full-binary-tree L R) , label-T) + lem = eq-pair-Σ refl (eq-htpy htpy) + where + htpy : + tr (labeling-full-binary-tree X) refl (pr2 + ( combinator-labeled-full-binary-tree X + ( L , (λ x → label-T (inl x))) (R , (λ x → label-T (inr x))))) ~ + label-T + htpy (inl _) = refl + htpy (inr _) = refl + + is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma : + ( f : hom-Magma (labeled-full-binary-tree-Magma X) M) → + is-set (type-Magma 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) (pr2 f) + is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma + f is-set-M = + eq-htpy htpy + where + htpy : + tr (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) ~ pr2 f + htpy T = eq-htpy htpy2 + where + htpy2 : + tr (preserves-mul-Magma (labeled-full-binary-tree-Magma X) M) (eq-htpy + ( λ U → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma U f)) + ( λ U V → refl) T ~ pr2 f T + htpy2 U = + pr1 (is-set-M (map-hom-Magma (labeled-full-binary-tree-Magma X) M f + ( pr2 (labeled-full-binary-tree-Magma X) T U)) + ( pr2 M (map-hom-Magma (labeled-full-binary-tree-Magma X) M f T) + ( map-hom-Magma (labeled-full-binary-tree-Magma X) M f U)) + ( tr (preserves-mul-Magma (labeled-full-binary-tree-Magma X) M) + ( eq-htpy (λ V → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma V f)) + ( λ V W → refl) T U) (pr2 f T U)) + + is-set-is-equiv-label-of-leaf-full-binary-tree-Magma : + is-set (type-Magma M) → is-equiv label-of-leaf + pr1 (pr1 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) = + extension-of-map-hom-labeled-full-binary-tree-Magma + pr2 (pr1 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) _ = refl + pr1 (pr2 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) = + extension-of-map-hom-labeled-full-binary-tree-Magma + pr2 (pr2 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma is-set-M)) f = + eq-pair-Σ (eq-htpy (λ T → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) + ( is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma + f is-set-M) + + is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma : + is-set (type-Magma M) → + hom-Magma (labeled-full-binary-tree-Magma X) M ≃ (X → type-Magma M) + pr1 (is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma _) = + label-of-leaf + pr2 (is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma is-set-M) = + is-set-is-equiv-label-of-leaf-full-binary-tree-Magma is-set-M +``` + +## External links + +[Free magmas](https://ncatlab.org/nlab/show/magma#free_magmas) at $n$Lab From f48e78373dc37b7d47e040e585b4b5b25f78f10f Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 2 Aug 2025 13:38:50 -0600 Subject: [PATCH 26/63] pre-commit hooks --- src/trees.lagda.md | 1 + src/trees/free-magmas-on-types.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/trees.lagda.md b/src/trees.lagda.md index 75bfbc3648..eaea988e6c 100644 --- a/src/trees.lagda.md +++ b/src/trees.lagda.md @@ -31,6 +31,7 @@ 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 diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index d6f6e4a2c4..0176115de3 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -15,11 +15,11 @@ 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.unit-type +open import foundation.universe-levels -open import foundation-core.dependent-identifications open import foundation-core.coproduct-types +open import foundation-core.dependent-identifications open import foundation-core.sets open import foundation-core.transport-along-identifications From db5840d50327949fc973de604ee558bf3cc47e41 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 2 Aug 2025 13:55:25 -0600 Subject: [PATCH 27/63] s --- src/structured-types/morphisms-magmas.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/structured-types/morphisms-magmas.lagda.md b/src/structured-types/morphisms-magmas.lagda.md index 3061cd01f5..20b5d7f596 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 From 84df00c0a71e16a7fd8b817b77241017b7aaad8f Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 2 Aug 2025 13:57:23 -0600 Subject: [PATCH 28/63] " --- src/trees/free-magmas-on-types.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 0176115de3..278c3ef163 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -41,7 +41,8 @@ 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 +What is meant by the "free magma on `X`" is the following. There are natural +maps `label-of-leaf : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M), extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M` for any [magma](structured-types.magmas.md) `M` and type `X`. `extension-of-map-labeled-full-binary-tree-Magma` is always a From 6d2b937f4b10d36061f6e4aa11cf78e8e2b4387f Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 11:41:00 -0600 Subject: [PATCH 29/63] weights of full binary trees --- src/trees/full-binary-trees.lagda.md | 15 +++++++++++++++ src/trees/labeled-full-binary-trees.lagda.md | 11 +++++++++++ 2 files changed, 26 insertions(+) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index d0db428966..69aff06e68 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -7,6 +7,9 @@ module trees.full-binary-trees where
Imports ```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.natural-numbers + open import foundation.unit-type open import foundation.universe-levels @@ -42,3 +45,15 @@ 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 = zero-ℕ +weight-full-binary-tree (join-full-binary-tree T U) = + weight-full-binary-tree T +ℕ weight-full-binary-tree U +``` diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 9703693d8c..971999611a 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -7,6 +7,8 @@ module trees.labeled-full-binary-trees where
Imports ```agda +open import elementary-number-theory.natural-numbers + open import foundation.dependent-pair-types open import foundation.universe-levels @@ -37,3 +39,12 @@ module _ labeled-full-binary-tree = Σ full-binary-tree (λ T → labeling-full-binary-tree 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 +``` From d38c33c8814b66e7541a8f3c065e065b0fc5475c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 11:41:15 -0600 Subject: [PATCH 30/63] the magma of a wild monoid --- src/structured-types/wild-monoids.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md index 250cabb823..0c5c5c7bde 100644 --- a/src/structured-types/wild-monoids.lagda.md +++ b/src/structured-types/wild-monoids.lagda.md @@ -13,6 +13,7 @@ open import foundation.identity-types open import foundation.unit-type open import foundation.universe-levels +open import structured-types.magmas open import structured-types.h-spaces 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 From ddf6ba12598bd842fc72d82a7e0bdaeb47c2877d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 11:49:20 -0600 Subject: [PATCH 31/63] flattenings of labeled full binary trees to lists --- .../flattening-free-magmas-lists.lagda.md | 100 ++++++++++++++++++ src/trees/full-binary-trees.lagda.md | 2 +- 2 files changed, 101 insertions(+), 1 deletion(-) create mode 100644 src/lists/flattening-free-magmas-lists.lagda.md 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..4cdb77ddf6 --- /dev/null +++ b/src/lists/flattening-free-magmas-lists.lagda.md @@ -0,0 +1,100 @@ +# The flattening morphisms from free magmas to free monoids + +```agda +module lists.flattening-free-magmas-lists where +``` + +
Imports + +```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 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-magmas +open import structured-types.wild-monoids + +open import trees.free-magmas-on-types +open import trees.labeled-full-binary-trees +open import trees.full-binary-trees +open import trees.combinator-full-binary-trees +``` + +
+ +## 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 initial 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 +``` diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 69aff06e68..156ced599a 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -53,7 +53,7 @@ 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 = zero-ℕ +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 ``` From b372e5c315e6f7c5248604d2be5c3665f6430c48 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 12:43:50 -0600 Subject: [PATCH 32/63] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit adding #'s to concept blocks Co-authored-by: Vojtěch Štěpančík --- src/trees/labeled-full-binary-trees.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 971999611a..82e05d49bc 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -19,10 +19,10 @@ open import trees.full-binary-trees ## Idea -For a type `X`, an {{concept "`X`-labeling" Agda=labeling-full-binary-tree}} of +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 +{{#concept "labeled full binary tree" Agda=labeled-full-binary-tree}} is a pair of a full binary tree and a labeling. ## Definition From 9a8d5b2b09663856ff2e6c95ced0fd4ef5fcd4a6 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 12:50:55 -0600 Subject: [PATCH 33/63] workinonit --- .../flattening-free-magmas-lists.lagda.md | 39 ++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/src/lists/flattening-free-magmas-lists.lagda.md b/src/lists/flattening-free-magmas-lists.lagda.md index 4cdb77ddf6..cede6030f0 100644 --- a/src/lists/flattening-free-magmas-lists.lagda.md +++ b/src/lists/flattening-free-magmas-lists.lagda.md @@ -17,12 +17,18 @@ 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-magmas +open import structured-types.morphisms-h-spaces +open import structured-types.morphisms-wild-monoids +open import structured-types.pointed-maps open import structured-types.wild-monoids open import trees.free-magmas-on-types @@ -41,7 +47,7 @@ For any type `X`, there is a natural [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 initial among magma maps from +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). @@ -98,3 +104,34 @@ of `T`. (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) = + {! !} +``` From 91e551fe73721598aa09217f6f9a8cd79625c368 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 3 Aug 2025 12:53:22 -0600 Subject: [PATCH 34/63] removed "abstract nonsense" quip --- src/trees/combinator-full-binary-trees.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 6b49818fc7..3f7cf56303 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -22,9 +22,9 @@ open import trees.labeled-full-binary-trees ## 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. +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). From c02a011150fbce6c38f2acdcf42620fbd3daf2ff Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 10:42:44 -0600 Subject: [PATCH 35/63] adding helper modules for the proof --- ...inary-homotopies-binary-functions.lagda.md | 37 +++++++++++++++++++ ...entifications-dependent-functions.lagda.md | 28 ++++++++++++++ 2 files changed, 65 insertions(+) create mode 100644 src/foundation/action-on-binary-homotopies-binary-functions.lagda.md create mode 100644 src/foundation/transport-along-identifications-dependent-functions.lagda.md 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..d30cc2cc60 --- /dev/null +++ b/src/foundation/action-on-binary-homotopies-binary-functions.lagda.md @@ -0,0 +1,37 @@ +# The action on binary homotopies + +```agda +module foundation.action-on-binary-homotopies-binary-functions where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.homotopy-induction +open import foundation.function-extensionality +open import foundation.universe-levels + +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## 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..b9a5e4a43f --- /dev/null +++ b/src/foundation/transport-along-identifications-dependent-functions.lagda.md @@ -0,0 +1,28 @@ +# Transport along identifications in dependent functions + +```agda +module foundation.transport-along-identifications-dependent-functions where +``` + +
Imports + +```agda +open import foundation.universe-levels +open import foundation-core.identity-types +open import foundation-core.transport-along-identifications +``` + +
+ +## 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 +``` From def5e23b79805538f713a3720ccf63c161e03c72 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 10:53:46 -0600 Subject: [PATCH 36/63] the univerrsal property of the free magma on one generator!! --- .../morphisms-magmas.lagda.md | 13 ++ .../free-magma-on-one-generator.lagda.md | 137 +++++++++++------- 2 files changed, 96 insertions(+), 54 deletions(-) diff --git a/src/structured-types/morphisms-magmas.lagda.md b/src/structured-types/morphisms-magmas.lagda.md index 20b5d7f596..f5068cdf37 100644 --- a/src/structured-types/morphisms-magmas.lagda.md +++ b/src/structured-types/morphisms-magmas.lagda.md @@ -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/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index e99b8c1556..9e936f3d77 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -8,6 +8,8 @@ module trees.free-magma-on-one-generator where ```agda open import foundation.action-on-identifications-binary-functions +open import foundation.transport-along-identifications-dependent-functions +open import foundation.action-on-binary-homotopies-binary-functions open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences @@ -15,6 +17,11 @@ open import foundation.function-extensionality open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels +open import foundation.binary-homotopies +open import foundation.action-on-identifications-functions +open import foundation.functoriality-cartesian-product-types +open import foundation.evaluation-functions +open import foundation.function-types open import foundation-core.dependent-identifications open import foundation-core.sets @@ -35,12 +42,26 @@ open import trees.labeled-full-binary-trees 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). +`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`. `map-inv-ev-leaf-hom-Magma` is +always a [section](foundation-core.sections.md) of `ev-leaf-hom-Magma`, and when +`M` is a set, we may prove it is also a +[retraction](foundation-core.retractions.md), i.e. that `ev-leaf-hom-Magma` is +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 @@ -49,8 +70,8 @@ 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 + 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 @@ -64,16 +85,16 @@ module _ ( 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 : + map-inv-ev-leaf-hom-Magma : type-Magma M → hom-Magma full-binary-tree-Magma M - pr1 (extension-of-point-hom-full-binary-tree-Magma m) = + pr1 (map-inv-ev-leaf-hom-Magma m) = extension-of-point-full-binary-tree-Magma m - pr2 (extension-of-point-hom-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 (image-of-leaf f) T = + 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 @@ -86,54 +107,62 @@ module _ ( 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-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) - 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 = + 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) + ( pr2 f U V) + ( ( ap + ( _∙ pr2 f U V) + ( htpy-eq (is-section-eq-htpy _) _)) ∙ + ( is-section-inv-concat' (pr2 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)) - ( 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 + ( 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 From 2fde9fe400cc5b8a0ee73db6b2079d9046d857ca Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 12:56:11 -0600 Subject: [PATCH 37/63] abstracted out the lemma that combinating commutes with labeling --- .../combinator-full-binary-trees.lagda.md | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 3f7cf56303..b5d85b8578 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -8,9 +8,16 @@ module trees.combinator-full-binary-trees where ```agda open import foundation.coproduct-types +open import foundation.equality-dependent-pair-types open import foundation.dependent-pair-types +open import foundation.function-extensionality 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 @@ -57,3 +64,39 @@ 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 +module _ + {l : Level} (X : UU l) (L R : full-binary-tree) + (lab : labeling-full-binary-tree X (join-full-binary-tree L R)) + where + + htpy-combinator-commutes-with-labelings-full-binary-tree : + tr (labeling-full-binary-tree X) refl + ( pr2 (combinator-labeled-full-binary-tree X + ( L , λ x → lab (inl x)) (R , (λ x → lab (inr x))))) ~ + lab + htpy-combinator-commutes-with-labelings-full-binary-tree (inl x) = refl + htpy-combinator-commutes-with-labelings-full-binary-tree (inr x) = refl + + combinator-commutes-with-labelings-full-binary-tree : + 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 = + eq-pair-Σ refl + ( eq-htpy htpy-combinator-commutes-with-labelings-full-binary-tree) +``` From bea9e04fc03ea866357f4604cd60411b0b2e59b6 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 13:25:34 -0600 Subject: [PATCH 38/63] workinonit --- ...ersal-property-lists-wild-monoids.lagda.md | 102 ++++++----- src/trees/free-magmas-on-types.lagda.md | 161 ++++++++++-------- 2 files changed, 149 insertions(+), 114 deletions(-) diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md index 67c4735fec..89dda97c19 100644 --- a/src/lists/universal-property-lists-wild-monoids.lagda.md +++ b/src/lists/universal-property-lists-wild-monoids.lagda.md @@ -9,11 +9,17 @@ module lists.universal-property-lists-wild-monoids where ```agda open import foundation.action-on-identifications-functions 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.unit-type open import foundation.universe-levels open import foundation.whiskering-higher-homotopies-composition +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.function-types + open import group-theory.homomorphisms-semigroups open import lists.concatenation-lists @@ -23,6 +29,7 @@ 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-maps +open import structured-types.pointed-homotopies open import structured-types.pointed-types open import structured-types.wild-monoids ``` @@ -31,11 +38,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 _ + {l : Level} (X : UU l) (M : Wild-Monoid l) (f : X → type-Wild-Monoid M) + where + + is-free-wild-monoid-on-type : UUω + is-free-wild-monoid-on-type = + {l2 : Level} (N : Wild-Monoid l2) → + is-equiv (λ g → map-hom-Wild-Monoid M N g ∘ f) +``` + ### The pointed type of lists of elements of `X` ```agda @@ -301,48 +327,36 @@ 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: - -```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) + + 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-Σ + {! !} + {! !} + pr1 (pr2 is-equiv-elim-list-Wild-Monoid) = map-inv-elim-list-Wild-Monoid + pr2 (pr2 is-equiv-elim-list-Wild-Monoid) x = + eq-htpy (λ y → pr1 (pr2 (pr2 (pr2 (pr1 M)))) (x y)) + + 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/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 278c3ef163..819afbe1ff 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -17,6 +17,13 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.unit-type open import foundation.universe-levels +open import foundation.binary-homotopies +open import foundation.transport-along-identifications-dependent-functions +open import foundation.action-on-binary-homotopies-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.functoriality-cartesian-product-types +open import foundation.evaluation-functions +open import foundation.function-types open import foundation-core.coproduct-types open import foundation-core.dependent-identifications @@ -43,12 +50,27 @@ 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 -`label-of-leaf : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M), extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M` +`ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M), extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M` for any [magma](structured-types.magmas.md) `M` and type `X`. `extension-of-map-labeled-full-binary-tree-Magma` is always a -[section](foundation-core.sections.md) of `label-of-leaf`, and when `M` is a -set, we may prove it is also a [retraction](foundation-core.retractions.md), -i.e. that `label-of-leaf` is an [equivalence](foundation-core.equivalences.md). +[section](foundation-core.sections.md) of `ev-label-leaf-hom-Magma`, and when +`M` is a set, we may prove it is also a +[retraction](foundation-core.retractions.md), i.e. that +`ev-label-leaf-hom-Magma` is an [equivalence](foundation-core.equivalences.md). + +## Definition + +### The universal property of free magmas on types + +```agda +module _ + {l : Level} (M : Magma l) (X : UU l) (f : X → type-Magma M) + where + + is-free-magma-on-type : UUω + is-free-magma-on-type = + {l2 : Level} (N : Magma l2) → is-equiv (λ g → map-hom-Magma M N g ∘ f) +``` ## Proof @@ -57,9 +79,9 @@ module _ {l1 l2 : Level} (X : UU l1) (M : Magma l2) where - label-of-leaf : + ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) - label-of-leaf (f , _) x = f (leaf-full-binary-tree , λ _ → x) + ev-label-leaf-hom-Magma (f , _) x = f (leaf-full-binary-tree , λ _ → x) {-# TERMINATING #-} extension-of-map-labeled-full-binary-tree-Magma : @@ -79,9 +101,9 @@ module _ ( extension-of-map-labeled-full-binary-tree-Magma f) is-hom-extension-of-map-labeled-full-binary-tree-Magma _ _ _ = refl - extension-of-map-hom-labeled-full-binary-tree-Magma : + map-inv-ev-label-leaf-hom-Magma : ( X → type-Magma M) → hom-Magma (labeled-full-binary-tree-Magma X) M - extension-of-map-hom-labeled-full-binary-tree-Magma f = + 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 @@ -89,7 +111,8 @@ module _ 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 (label-of-leaf f) T = + 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 @@ -102,76 +125,74 @@ module _ ( 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 lem - where - lem : - combinator-labeled-full-binary-tree X - ( L , (λ x → label-T (inl x))) (R , (λ x → label-T (inr x))) = - (( join-full-binary-tree L R) , label-T) - lem = eq-pair-Σ refl (eq-htpy htpy) - where - htpy : - tr (labeling-full-binary-tree X) refl (pr2 - ( combinator-labeled-full-binary-tree X - ( L , (λ x → label-T (inl x))) (R , (λ x → label-T (inr x))))) ~ - label-T - htpy (inl _) = refl - htpy (inr _) = refl - - is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma : + ∙ 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) → - is-set (type-Magma M) → dependent-identification ( preserves-mul-Magma (labeled-full-binary-tree-Magma X) M) - (eq-htpy + ( eq-htpy ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) ( λ T U → refl) (pr2 f) - is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma - f is-set-M = - eq-htpy htpy - where - htpy : - tr (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) ~ pr2 f - htpy T = eq-htpy htpy2 - where - htpy2 : - tr (preserves-mul-Magma (labeled-full-binary-tree-Magma X) M) (eq-htpy - ( λ U → - is-retraction-extension-of-map-labeled-full-binary-tree-Magma U f)) - ( λ U V → refl) T ~ pr2 f T - htpy2 U = - pr1 (is-set-M (map-hom-Magma (labeled-full-binary-tree-Magma X) M f - ( pr2 (labeled-full-binary-tree-Magma X) T U)) - ( pr2 M (map-hom-Magma (labeled-full-binary-tree-Magma X) M f T) - ( map-hom-Magma (labeled-full-binary-tree-Magma X) M f U)) - ( tr (preserves-mul-Magma (labeled-full-binary-tree-Magma X) M) - ( eq-htpy (λ V → - is-retraction-extension-of-map-labeled-full-binary-tree-Magma V f)) - ( λ V W → refl) T U) (pr2 f T U)) - - is-set-is-equiv-label-of-leaf-full-binary-tree-Magma : - is-set (type-Magma M) → is-equiv label-of-leaf - pr1 (pr1 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) = - extension-of-map-hom-labeled-full-binary-tree-Magma - pr2 (pr1 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) _ = refl - pr1 (pr2 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma _)) = - extension-of-map-hom-labeled-full-binary-tree-Magma - pr2 (pr2 (is-set-is-equiv-label-of-leaf-full-binary-tree-Magma is-set-M)) f = + dependent-identification-preserves-mul-labeled-full-binary-tree-Magma f = + eq-binary-htpy _ _ (λ U V → htpy-eq + ( tr-Π (eq-htpy + ( λ T → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) + ( λ T U → refl) U) V ∙ tr-Π (eq-htpy + ( λ T → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) + ( λ 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) + ( pr2 f U V) + ( ap (λ p → p ∙ pr2 f U V) (htpy-eq (is-section-eq-htpy + ( λ T → + is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) + ( combinator-labeled-full-binary-tree X U V)) ∙ + ( ap (λ p → ap-binary (pr2 M) + ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma + ( pr1 U , (λ x → pr2 U x)) (pr1 f , pr2 f)) + ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma + ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) + ∙ inv (pr2 f (pr1 U , (λ x → pr2 U x)) (pr1 V , (λ x → pr2 V x))) + ∙ p ∙ pr2 f U V) {! !} ∙ {! !} ∙ + is-section-inv-concat' (pr2 f U V) (ap-binary (pr2 M) + ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma U f) + ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma V f))) ∙ + ap-binary-htpy + ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f) + ( 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)) - ( is-set-dependent-identification-preserves-mul-labeled-full-binary-tree-Magma - f is-set-M) + ( dependent-identification-preserves-mul-labeled-full-binary-tree-Magma f) - is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma : - is-set (type-Magma M) → + 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 (is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma _) = - label-of-leaf - pr2 (is-set-equiv-label-of-leaf-labeled-full-binary-tree-Magma is-set-M) = - is-set-is-equiv-label-of-leaf-full-binary-tree-Magma is-set-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 From 3b9f6dd27546b55dd4624c16130c38df87958877 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 13:46:11 -0600 Subject: [PATCH 39/63] pre-commit run to keep things sanitary --- src/foundation.lagda.md | 2 + ...inary-homotopies-binary-functions.lagda.md | 3 +- ...entifications-dependent-functions.lagda.md | 1 + src/lists.lagda.md | 1 + .../flattening-free-magmas-lists.lagda.md | 6 +-- ...ersal-property-lists-wild-monoids.lagda.md | 13 +++--- src/structured-types/wild-monoids.lagda.md | 2 +- .../combinator-full-binary-trees.lagda.md | 2 +- .../free-magma-on-one-generator.lagda.md | 40 +++++++++++-------- src/trees/free-magmas-on-types.lagda.md | 36 ++++++++--------- src/trees/labeled-full-binary-trees.lagda.md | 7 ++-- 11 files changed, 60 insertions(+), 53 deletions(-) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 0a5a201e83..f74ec26175 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 @@ -437,6 +438,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 index d30cc2cc60..605252453b 100644 --- a/src/foundation/action-on-binary-homotopies-binary-functions.lagda.md +++ b/src/foundation/action-on-binary-homotopies-binary-functions.lagda.md @@ -9,8 +9,8 @@ module foundation.action-on-binary-homotopies-binary-functions where ```agda open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions -open import foundation.homotopy-induction open import foundation.function-extensionality +open import foundation.homotopy-induction open import foundation.universe-levels open import foundation-core.homotopies @@ -33,5 +33,4 @@ ap-binary-htpy {f = f} H m {x = x} {y = y} = ( 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 index b9a5e4a43f..4a838dbe11 100644 --- a/src/foundation/transport-along-identifications-dependent-functions.lagda.md +++ b/src/foundation/transport-along-identifications-dependent-functions.lagda.md @@ -8,6 +8,7 @@ module foundation.transport-along-identifications-dependent-functions where ```agda open import foundation.universe-levels + open import foundation-core.identity-types open import foundation-core.transport-along-identifications ``` diff --git a/src/lists.lagda.md b/src/lists.lagda.md index bb36916d48..f317886b7f 100644 --- a/src/lists.lagda.md +++ b/src/lists.lagda.md @@ -9,6 +9,7 @@ open import lists.arrays public open import lists.concatenation-lists 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 index cede6030f0..114159ee2f 100644 --- a/src/lists/flattening-free-magmas-lists.lagda.md +++ b/src/lists/flattening-free-magmas-lists.lagda.md @@ -25,16 +25,16 @@ open import lists.lists open import lists.universal-property-lists-wild-monoids open import structured-types.magmas -open import structured-types.morphisms-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.labeled-full-binary-trees open import trees.full-binary-trees -open import trees.combinator-full-binary-trees +open import trees.labeled-full-binary-trees ```
diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md index 89dda97c19..d7b3ddd00c 100644 --- a/src/lists/universal-property-lists-wild-monoids.lagda.md +++ b/src/lists/universal-property-lists-wild-monoids.lagda.md @@ -17,8 +17,8 @@ open import foundation.universe-levels open import foundation.whiskering-higher-homotopies-composition open import foundation-core.equivalences -open import foundation-core.homotopies open import foundation-core.function-types +open import foundation-core.homotopies open import group-theory.homomorphisms-semigroups @@ -28,8 +28,8 @@ 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-maps open import structured-types.pointed-homotopies +open import structured-types.pointed-maps open import structured-types.pointed-types open import structured-types.wild-monoids ``` @@ -53,12 +53,12 @@ for any wild monoid `M`, there is an equivalence: ```agda module _ - {l : Level} (X : UU l) (M : Wild-Monoid l) (f : X → type-Wild-Monoid M) + {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 = - {l2 : Level} (N : Wild-Monoid l2) → + {l3 : Level} (N : Wild-Monoid l3) → is-equiv (λ g → map-hom-Wild-Monoid M N g ∘ f) ``` @@ -341,10 +341,7 @@ module _ 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-Σ - {! !} - {! !} + pr2 (pr1 is-equiv-elim-list-Wild-Monoid) f = {! !} pr1 (pr2 is-equiv-elim-list-Wild-Monoid) = map-inv-elim-list-Wild-Monoid pr2 (pr2 is-equiv-elim-list-Wild-Monoid) x = eq-htpy (λ y → pr1 (pr2 (pr2 (pr2 (pr1 M)))) (x y)) diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md index 0c5c5c7bde..143fb8a38e 100644 --- a/src/structured-types/wild-monoids.lagda.md +++ b/src/structured-types/wild-monoids.lagda.md @@ -13,8 +13,8 @@ open import foundation.identity-types open import foundation.unit-type open import foundation.universe-levels -open import structured-types.magmas open import structured-types.h-spaces +open import structured-types.magmas open import structured-types.pointed-types ``` diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index b5d85b8578..b5a4bed278 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -8,8 +8,8 @@ module trees.combinator-full-binary-trees where ```agda open import foundation.coproduct-types -open import foundation.equality-dependent-pair-types open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types open import foundation.function-extensionality open import foundation.universe-levels diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 9e936f3d77..4506e2561d 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -7,21 +7,21 @@ module trees.free-magma-on-one-generator where
Imports ```agda -open import foundation.action-on-identifications-binary-functions -open import foundation.transport-along-identifications-dependent-functions 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.evaluation-functions open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types 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.binary-homotopies -open import foundation.action-on-identifications-functions -open import foundation.functoriality-cartesian-product-types -open import foundation.evaluation-functions -open import foundation.function-types open import foundation-core.dependent-identifications open import foundation-core.sets @@ -42,12 +42,14 @@ open import trees.labeled-full-binary-trees 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 -`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`. `map-inv-ev-leaf-hom-Magma` is -always a [section](foundation-core.sections.md) of `ev-leaf-hom-Magma`, and when -`M` is a set, we may prove it is also a -[retraction](foundation-core.retractions.md), i.e. that `ev-leaf-hom-Magma` is -an [equivalence](foundation-core.equivalences.md). + +```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 @@ -118,19 +120,22 @@ module _ ( λ U V → ( htpy-eq ( tr-Π - ( eq-htpy (λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f)) + ( 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)) + ( 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)) + ( λ T → + is-retraction-extension-of-point-full-binary-tree-Magma T f)) ( refl) ( pr2 f U V) ( ( ap @@ -138,7 +143,8 @@ module _ ( htpy-eq (is-section-eq-htpy _) _)) ∙ ( is-section-inv-concat' (pr2 f U V) _) ∙ ( ap-binary-htpy - ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f) + ( λ 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 : diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 819afbe1ff..1b0c001274 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -7,23 +7,22 @@ module trees.free-magmas-on-types where
Imports ```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.evaluation-functions open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-cartesian-product-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.binary-homotopies -open import foundation.transport-along-identifications-dependent-functions -open import foundation.action-on-binary-homotopies-binary-functions -open import foundation.action-on-identifications-functions -open import foundation.functoriality-cartesian-product-types -open import foundation.evaluation-functions -open import foundation.function-types open import foundation-core.coproduct-types open import foundation-core.dependent-identifications @@ -50,13 +49,14 @@ 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 -`ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M), extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree X → type-Magma M` -for any [magma](structured-types.magmas.md) `M` and type `X`. -`extension-of-map-labeled-full-binary-tree-Magma` is always a -[section](foundation-core.sections.md) of `ev-label-leaf-hom-Magma`, and when -`M` is a set, we may prove it is also a -[retraction](foundation-core.retractions.md), i.e. that -`ev-label-leaf-hom-Magma` is an [equivalence](foundation-core.equivalences.md). + +```text + ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) + extension-of-map-labeled-full-binary-tree-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 @@ -64,12 +64,12 @@ for any [magma](structured-types.magmas.md) `M` and type `X`. ```agda module _ - {l : Level} (M : Magma l) (X : UU l) (f : X → type-Magma M) + {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 = - {l2 : Level} (N : Magma l2) → is-equiv (λ g → map-hom-Magma M N g ∘ f) + {l3 : Level} (N : Magma l3) → is-equiv (λ g → map-hom-Magma M N g ∘ f) ``` ## Proof @@ -156,9 +156,9 @@ module _ ( combinator-labeled-full-binary-tree X U V)) ∙ ( ap (λ p → ap-binary (pr2 M) ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma - ( pr1 U , (λ x → pr2 U x)) (pr1 f , pr2 f)) + ( pr1 U , (λ x → pr2 U x)) (pr1 f , pr2 f)) ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma - ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) + ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) ∙ inv (pr2 f (pr1 U , (λ x → pr2 U x)) (pr1 V , (λ x → pr2 V x))) ∙ p ∙ pr2 f U V) {! !} ∙ {! !} ∙ is-section-inv-concat' (pr2 f U V) (ap-binary (pr2 M) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 82e05d49bc..01f0940bf2 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -19,9 +19,10 @@ open import trees.full-binary-trees ## 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 +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. From 076b4e8eaafff180998409920efcbd1bac453568 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 13:46:55 -0600 Subject: [PATCH 40/63] fixed function name in idea --- src/trees/free-magmas-on-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 1b0c001274..9e35ff7aa4 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -52,7 +52,7 @@ maps ```text ev-label-leaf-hom-Magma : hom-Magma (labeled-full-binary-tree-Magma X) M → (X → type-Magma M) - extension-of-map-labeled-full-binary-tree-Magma : (X → type-Magma M) → labeled-full-binary-tree 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 From 57da25791ae6c0b912d7d44c8c4b0dbe2bdc887b Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 13:51:06 -0600 Subject: [PATCH 41/63] pruning imports --- src/trees/free-magma-on-one-generator.lagda.md | 6 ------ src/trees/free-magmas-on-types.lagda.md | 3 --- 2 files changed, 9 deletions(-) diff --git a/src/trees/free-magma-on-one-generator.lagda.md b/src/trees/free-magma-on-one-generator.lagda.md index 4506e2561d..f8f659a026 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -14,25 +14,19 @@ 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.evaluation-functions open import foundation.function-extensionality -open import foundation.function-types -open import foundation.functoriality-cartesian-product-types 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 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 ```
diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 9e35ff7aa4..12ba1ba055 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -14,10 +14,8 @@ 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.evaluation-functions open import foundation.function-extensionality open import foundation.function-types -open import foundation.functoriality-cartesian-product-types open import foundation.homotopies open import foundation.identity-types open import foundation.transport-along-identifications-dependent-functions @@ -26,7 +24,6 @@ open import foundation.universe-levels open import foundation-core.coproduct-types open import foundation-core.dependent-identifications -open import foundation-core.sets open import foundation-core.transport-along-identifications open import structured-types.magmas From 026ddf02663d048a371bc6314c205e98cb37b3d2 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 19:05:14 -0600 Subject: [PATCH 42/63] workinonit --- src/trees/combinator-full-binary-trees.lagda.md | 4 ++++ src/trees/free-magmas-on-types.lagda.md | 7 +++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index b5a4bed278..1694240a8d 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -99,4 +99,8 @@ module _ combinator-commutes-with-labelings-full-binary-tree = eq-pair-Σ refl ( eq-htpy htpy-combinator-commutes-with-labelings-full-binary-tree) + + is-refl-htpy-combinator-commutes-with-labelings-full-binary-tree : + htpy-combinator-commutes-with-labelings-full-binary-tree = {! !} -- this should fill with refl-htpy but somehow the LHS doesn't judgementally rewrite to the RHS - why are they not definitionally equal? is there another way? + is-refl-htpy-combinator-commutes-with-labelings-full-binary-tree = {! !} ``` diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 12ba1ba055..7516e5f9a3 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -157,10 +157,9 @@ module _ ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) ∙ inv (pr2 f (pr1 U , (λ x → pr2 U x)) (pr1 V , (λ x → pr2 V x))) - ∙ p ∙ pr2 f U V) {! !} ∙ {! !} ∙ - is-section-inv-concat' (pr2 f U V) (ap-binary (pr2 M) - ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma U f) - ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma V f))) ∙ + ∙ p ∙ pr2 f U V) {! !} ∙ -- this goal *should* be filed with a path that combinator-commutes-with-labelings.. is refl but this isn't judgementally so... + {! !} ∙ + is-section-inv-concat' (pr2 f U V) _) ∙ ap-binary-htpy ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f) ( mul-Magma M)))) From 4c5ef351465edd95060b2df6e9a4c178e30c4210 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 4 Aug 2025 19:07:35 -0600 Subject: [PATCH 43/63] continuing to build this but it's expanding the scope of this fork quite a bit - may stash this one or comment it out with a note, we'll see later --- ...ersal-property-lists-wild-monoids.lagda.md | 65 ++++++++++++++++++- 1 file changed, 62 insertions(+), 3 deletions(-) diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md index d7b3ddd00c..6969cef6b9 100644 --- a/src/lists/universal-property-lists-wild-monoids.lagda.md +++ b/src/lists/universal-property-lists-wild-monoids.lagda.md @@ -7,18 +7,24 @@ module lists.universal-property-lists-wild-monoids where
Imports ```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 @@ -339,12 +345,65 @@ module _ 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 = {! !} + 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) x = - eq-htpy (λ y → pr1 (pr2 (pr2 (pr2 (pr1 M)))) (x y)) + 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 From 4f9c62b7e1ba659411bc0c8a47919851ae845f59 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 17:42:27 -0600 Subject: [PATCH 44/63] characterizing identifications of full binary trees --- src/trees/full-binary-trees.lagda.md | 111 +++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 156ced599a..0b7962e9dc 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -10,10 +10,21 @@ module trees.full-binary-trees where 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.dependent-pair-types open import foundation.unit-type +open import foundation.decidable-equality +open import foundation.decidable-types open import foundation.universe-levels +open import foundation.torsorial-type-families +open import foundation.fundamental-theorem-of-identity-types +open import foundation-core.cartesian-product-types +open import foundation-core.empty-types +open import foundation-core.equivalences +open import foundation-core.sets open import foundation-core.coproduct-types +open import foundation-core.identity-types ```
@@ -57,3 +68,103 @@ 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₁ + +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 +``` From 15bb5bb1778e9451d98ab59b736839780831cf16 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 19:48:06 -0600 Subject: [PATCH 45/63] pre-commit hooks --- src/trees/full-binary-trees.lagda.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 0b7962e9dc..474a30525a 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -11,20 +11,20 @@ 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.dependent-pair-types -open import foundation.unit-type open import foundation.decidable-equality open import foundation.decidable-types -open import foundation.universe-levels -open import foundation.torsorial-type-families +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 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.sets -open import foundation-core.coproduct-types open import foundation-core.identity-types +open import foundation-core.sets ```
From 2c405f3cae811322c9dd48388dab982c3bea783a Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 19:48:23 -0600 Subject: [PATCH 46/63] removed the dead end --- src/trees/combinator-full-binary-trees.lagda.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index 1694240a8d..b5a4bed278 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -99,8 +99,4 @@ module _ combinator-commutes-with-labelings-full-binary-tree = eq-pair-Σ refl ( eq-htpy htpy-combinator-commutes-with-labelings-full-binary-tree) - - is-refl-htpy-combinator-commutes-with-labelings-full-binary-tree : - htpy-combinator-commutes-with-labelings-full-binary-tree = {! !} -- this should fill with refl-htpy but somehow the LHS doesn't judgementally rewrite to the RHS - why are they not definitionally equal? is there another way? - is-refl-htpy-combinator-commutes-with-labelings-full-binary-tree = {! !} ``` From 97274c3e87a93f835dd7d7928108128890cefddd Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 19:48:34 -0600 Subject: [PATCH 47/63] workinonit --- src/trees/free-magmas-on-types.lagda.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 7516e5f9a3..24bad0a9c4 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -1,6 +1,8 @@ # Free magmas on types ```agda +{-# OPTIONS --lossy-unification #-} + module trees.free-magmas-on-types where ``` @@ -157,12 +159,19 @@ module _ ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) ∙ inv (pr2 f (pr1 U , (λ x → pr2 U x)) (pr1 V , (λ x → pr2 V x))) - ∙ p ∙ pr2 f U V) {! !} ∙ -- this goal *should* be filed with a path that combinator-commutes-with-labelings.. is refl but this isn't judgementally so... - {! !} ∙ + ∙ p ∙ pr2 f U V) (lem U V) ∙ -- this goal *should* be filled with a path that combinator-commutes-with-labelings-_ is refl but this isn't judgementally so... + {! !} ∙ is-section-inv-concat' (pr2 f U V) _) ∙ ap-binary-htpy ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f) ( mul-Magma M)))) + where + lem : (U V : labeled-full-binary-tree X) → + ap (pr1 f) + (combinator-commutes-with-labelings-full-binary-tree X (pr1 U) + (pr1 V) (pr2 (combinator-labeled-full-binary-tree X U V))) = + refl + lem U V = {! !} is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma : is-equiv ev-label-leaf-hom-Magma From a396d95e544a9f40ce618264d0117e1bdcc68031 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 19:48:56 -0600 Subject: [PATCH 48/63] characterizing identifications of labeled full binary trees --- src/trees/labeled-full-binary-trees.lagda.md | 201 +++++++++++++++++++ 1 file changed, 201 insertions(+) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 01f0940bf2..07b0e7385c 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -9,9 +9,23 @@ module trees.labeled-full-binary-trees where ```agda open import elementary-number-theory.natural-numbers +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +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.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections + open import trees.full-binary-trees ``` @@ -49,3 +63,190 @@ This is simply the weight of its underlying full binary tree. weight-labeled-full-binary-tree : labeled-full-binary-tree → ℕ weight-labeled-full-binary-tree (T , _) = weight-full-binary-tree T ``` + +### Computing transport of labelings along identifications of full binary trees + +```agda +module _ + {l : Level} (X : UU l) + where + + compute-tr-Eq-labeling-full-binary-tree : + (U : labeled-full-binary-tree X) → + (V : full-binary-tree) → + Eq-full-binary-tree (pr1 U) V → + labeling-full-binary-tree X V + compute-tr-Eq-labeling-full-binary-tree + (leaf-full-binary-tree , lab-U) leaf-full-binary-tree star star = lab-U star + compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree U U₁ , lab-U) + (join-full-binary-tree V V₁) (p , q) (inl x) = + compute-tr-Eq-labeling-full-binary-tree (U , λ y → lab-U (inl y)) V p x + compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree U U₁ , lab-U) + (join-full-binary-tree V V₁) (p , q) (inr x) = + compute-tr-Eq-labeling-full-binary-tree (U₁ , λ y → lab-U (inr y)) V₁ q x +``` + +### Characterizing the identity type of labeled full binary trees + +```agda +module _ + {l : Level} (X : UU l) + where + + Eq-htpy-labeled-full-binary-tree : + (U V : labeled-full-binary-tree X) → + Eq-full-binary-tree (pr1 U) (pr1 V) → + UU l + Eq-htpy-labeled-full-binary-tree U V p = + compute-tr-Eq-labeling-full-binary-tree X U (pr1 V) p ~ pr2 V + + refl-compute-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → f = g → + Eq-htpy-labeled-full-binary-tree (T , f) (T , g) + (refl-Eq-full-binary-tree T) + refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f f refl star = + refl + refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f f refl (inl x) = + refl-compute-tr-Eq-labeling-full-binary-tree T + ( λ y → f (inl y)) (λ y → f (inl y)) refl x + refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f f refl (inr x) = + refl-compute-tr-Eq-labeling-full-binary-tree T₁ + ( λ y → f (inr y)) (λ y → f (inr y)) refl x + + eq-inl-compute-tr-Eq-labeling-full-binary-tree : + (U V : full-binary-tree) + (f : labeling-full-binary-tree X (join-full-binary-tree U V)) + (x : node-full-binary-tree U) → + f (inl x) = compute-tr-Eq-labeling-full-binary-tree X + (U , λ y → f (inl y)) U + (refl-Eq-full-binary-tree U) x + eq-inl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree _ f star = refl + eq-inl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree U U₁) _ f (inl x) = + eq-inl-compute-tr-Eq-labeling-full-binary-tree U U₁ (λ z → f (inl z)) x + eq-inl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree U U₁) _ f (inr x) = + eq-inl-compute-tr-Eq-labeling-full-binary-tree U₁ U lab x + where + lab : labeling-full-binary-tree X (join-full-binary-tree U₁ U) + lab (inl y) = f (inl (inr y)) + lab (inr y) = f (inl (inl y)) + + eq-inr-compute-tr-Eq-labeling-full-binary-tree : (U V : full-binary-tree) + (f : labeling-full-binary-tree X (join-full-binary-tree U V)) + (x : node-full-binary-tree V) → + f (inr x) = compute-tr-Eq-labeling-full-binary-tree X + (V , λ y → f (inr y)) V + (refl-Eq-full-binary-tree V) x + eq-inr-compute-tr-Eq-labeling-full-binary-tree + _ leaf-full-binary-tree f star = refl + eq-inr-compute-tr-Eq-labeling-full-binary-tree + _ (join-full-binary-tree V V₁) f (inl x) = + eq-inr-compute-tr-Eq-labeling-full-binary-tree V₁ V lab x + where + lab : labeling-full-binary-tree X (join-full-binary-tree V₁ V) + lab (inl y) = f (inr (inl x)) + lab (inr y) = f (inr (inl y)) + eq-inr-compute-tr-Eq-labeling-full-binary-tree + _ (join-full-binary-tree V V₁) f (inr x) = + eq-inr-compute-tr-Eq-labeling-full-binary-tree V V₁ (λ z → f (inr z)) x + + inv-refl-compute-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + Eq-htpy-labeled-full-binary-tree (T , f) (T , g) + (refl-Eq-full-binary-tree T) → + f = g + inv-refl-compute-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f g p = + eq-htpy (λ x → p star) + inv-refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g p = + eq-htpy htpy + where + htpy : f ~ g + htpy (inl x) = + eq-inl-compute-tr-Eq-labeling-full-binary-tree T T₁ f x ∙ p (inl x) + htpy (inr x) = + eq-inr-compute-tr-Eq-labeling-full-binary-tree T T₁ f x ∙ p (inr x) + + is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + is-equiv (refl-compute-tr-Eq-labeling-full-binary-tree T f g) + pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = + inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g + pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f g)) p = + eq-htpy htpy + where + htpy : + (refl-compute-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f g ∘ + pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f g))) p ~ + p + htpy star = {! !} + pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g)) p = + eq-htpy htpy + where + htpy : + (refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g ∘ + pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g))) p ~ + p + htpy (inl x) = {! !} + htpy (inr x) = {! !} + pr1 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = + inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g + pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f f)) refl = {! !} + pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f f)) refl = {! !} + + Eq-labeled-full-binary-tree : + labeled-full-binary-tree X → labeled-full-binary-tree X → UU l + Eq-labeled-full-binary-tree (U , lab-U) (V , lab-V) = + Σ + ( Eq-full-binary-tree U V) + ( Eq-htpy-labeled-full-binary-tree (U , lab-U) (V , lab-V)) + + {-# TERMINATING #-} + refl-Eq-htpy-labeled-full-binary-tree : + (U : labeled-full-binary-tree X) → + Eq-htpy-labeled-full-binary-tree U U (refl-Eq-full-binary-tree (pr1 U)) + refl-Eq-htpy-labeled-full-binary-tree (leaf-full-binary-tree , lab-U) star = + refl + refl-Eq-htpy-labeled-full-binary-tree + (join-full-binary-tree U V , lab-U) (inl x) = + refl-Eq-htpy-labeled-full-binary-tree (U , (λ y → lab-U (inl y))) x + refl-Eq-htpy-labeled-full-binary-tree + (join-full-binary-tree U V , lab-U) (inr x) = + refl-Eq-htpy-labeled-full-binary-tree (V , (λ y → lab-U (inr y))) x + + Eq-eq-labeled-full-binary-tree : + (U V : labeled-full-binary-tree X) → + U = V → + Eq-labeled-full-binary-tree U V + pr1 (Eq-eq-labeled-full-binary-tree U U refl) = + refl-Eq-full-binary-tree (pr1 U) + pr2 (Eq-eq-labeled-full-binary-tree U U refl) = + refl-Eq-htpy-labeled-full-binary-tree U + + 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 = + structure-identity-principle + ( λ {x} f p → Eq-htpy-labeled-full-binary-tree U (x , f) p) + ( refl-Eq-full-binary-tree (pr1 U)) + ( refl-Eq-htpy-labeled-full-binary-tree U) + ( Eq-eq-labeled-full-binary-tree U) + ( λ _ → is-equiv-Eq-eq-full-binary-tree) + ( λ y → is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + ( pr1 U) (pr2 U) y) +``` From bc2794be7d27c404750359119039b91b4f969d3c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 19:59:11 -0600 Subject: [PATCH 49/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 22 ++------------------ 1 file changed, 2 insertions(+), 20 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 07b0e7385c..919fbf0b24 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -180,27 +180,9 @@ module _ pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g)) p = - eq-htpy htpy - where - htpy : - (refl-compute-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f g ∘ - pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g))) p ~ - p - htpy star = {! !} + leaf-full-binary-tree f g)) p = {! !} pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g)) p = - eq-htpy htpy - where - htpy : - (refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g ∘ - pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g))) p ~ - p - htpy (inl x) = {! !} - htpy (inr x) = {! !} + (join-full-binary-tree T T₁) f g)) p = {! !} pr1 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree From 269a87bb75b267aa54236e05e60840c1b0505db9 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 20:15:36 -0600 Subject: [PATCH 50/63] workinonit --- src/trees/free-magmas-on-types.lagda.md | 7 --- src/trees/labeled-full-binary-trees.lagda.md | 49 ++++++++++++++++---- 2 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index 24bad0a9c4..d4e1992853 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -165,13 +165,6 @@ module _ ap-binary-htpy ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f) ( mul-Magma M)))) - where - lem : (U V : labeled-full-binary-tree X) → - ap (pr1 f) - (combinator-commutes-with-labelings-full-binary-tree X (pr1 U) - (pr1 V) (pr2 (combinator-labeled-full-binary-tree X U V))) = - refl - lem U V = {! !} is-equiv-ev-label-leaf-hom-Magma-full-binary-tree-Magma : is-equiv ev-label-leaf-hom-Magma diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 919fbf0b24..556cfda4f9 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -180,9 +180,26 @@ module _ pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g)) p = {! !} + leaf-full-binary-tree f g)) p = eq-htpy htpy + where + htpy : + (refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f g ∘ + pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + leaf-full-binary-tree f g))) p ~ + p + htpy star = ap {! !} {! !} ∙ {! !} pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g)) p = {! !} + (join-full-binary-tree T T₁) f g)) p = eq-htpy htpy + where + htpy : + (refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g ∘ + pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree T T₁) f g))) p ~ + p + htpy (inl x) = {! !} + htpy (inr x) = {! !} pr1 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree @@ -204,11 +221,11 @@ module _ refl-Eq-htpy-labeled-full-binary-tree (leaf-full-binary-tree , lab-U) star = refl refl-Eq-htpy-labeled-full-binary-tree - (join-full-binary-tree U V , lab-U) (inl x) = - refl-Eq-htpy-labeled-full-binary-tree (U , (λ y → lab-U (inl y))) x + (join-full-binary-tree U V , lab) (inl x) = + refl-Eq-htpy-labeled-full-binary-tree (U , (λ y → lab (inl y))) x refl-Eq-htpy-labeled-full-binary-tree - (join-full-binary-tree U V , lab-U) (inr x) = - refl-Eq-htpy-labeled-full-binary-tree (V , (λ y → lab-U (inr y))) x + (join-full-binary-tree U V , lab) (inr x) = + refl-Eq-htpy-labeled-full-binary-tree (V , (λ y → lab (inr y))) x Eq-eq-labeled-full-binary-tree : (U V : labeled-full-binary-tree X) → @@ -220,8 +237,8 @@ module _ refl-Eq-htpy-labeled-full-binary-tree U 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) + (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 = structure-identity-principle ( λ {x} f p → Eq-htpy-labeled-full-binary-tree U (x , f) p) @@ -231,4 +248,20 @@ module _ ( λ _ → is-equiv-Eq-eq-full-binary-tree) ( λ y → is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree ( pr1 U) (pr2 U) y) + + 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) ``` From bdc04cfbecb8b8544107651d6ffe182d268c201c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 22:43:47 -0600 Subject: [PATCH 51/63] propositional equality in full binary trees --- src/trees/full-binary-trees.lagda.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 474a30525a..513a617184 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -22,6 +22,7 @@ open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.coproduct-types open import foundation-core.empty-types +open import foundation-core.propositions open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.sets @@ -79,6 +80,20 @@ 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₁) = From d1410c84b7d4c46a80fff4756324e0a1da44baf3 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 9 Aug 2025 22:44:34 -0600 Subject: [PATCH 52/63] commented out, for now --- src/lists/universal-property-lists-wild-monoids.lagda.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md index 6969cef6b9..748b6132f2 100644 --- a/src/lists/universal-property-lists-wild-monoids.lagda.md +++ b/src/lists/universal-property-lists-wild-monoids.lagda.md @@ -335,7 +335,11 @@ elim-list-Wild-Monoid M f = ### Pulling back `hom (list X) M` along the inclusion `X → list X` is an equivalence +This remains to be formalized. Below is some work towards this goal: + ```agda +{- + module _ {l1 l2 : Level} (X : UU l1) (M : Wild-Monoid l2) where @@ -415,4 +419,6 @@ is-free-wild-monoid-on-type-list-Wild-Monoid : 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) + +-} ``` From 0b406fea96e307e9947f06f1a494e3381f347167 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 10 Aug 2025 00:10:49 -0600 Subject: [PATCH 53/63] workinonit --- src/trees/full-binary-trees.lagda.md | 2 +- src/trees/labeled-full-binary-trees.lagda.md | 316 ++++++++++--------- 2 files changed, 167 insertions(+), 151 deletions(-) diff --git a/src/trees/full-binary-trees.lagda.md b/src/trees/full-binary-trees.lagda.md index 513a617184..d951fb503e 100644 --- a/src/trees/full-binary-trees.lagda.md +++ b/src/trees/full-binary-trees.lagda.md @@ -22,9 +22,9 @@ open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.coproduct-types open import foundation-core.empty-types -open import foundation-core.propositions open import foundation-core.equivalences open import foundation-core.identity-types +open import foundation-core.propositions open import foundation-core.sets ``` diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 556cfda4f9..68c5af82d3 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -1,6 +1,8 @@ # Labeled full binary trees ```agda +{-# OPTIONS --lossy-unification #-} + module trees.labeled-full-binary-trees where ``` @@ -9,22 +11,30 @@ module trees.labeled-full-binary-trees where ```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.equality-cartesian-product-types open import foundation.function-extensionality 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.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.transport-along-identifications open import trees.full-binary-trees ``` @@ -71,24 +81,24 @@ module _ {l : Level} (X : UU l) where - compute-tr-Eq-labeling-full-binary-tree : - (U : labeled-full-binary-tree X) → + tr-Eq-labeling-full-binary-tree : + (U : labeled-full-binary-tree X) (V : full-binary-tree) → Eq-full-binary-tree (pr1 U) V → labeling-full-binary-tree X V - compute-tr-Eq-labeling-full-binary-tree + tr-Eq-labeling-full-binary-tree (leaf-full-binary-tree , lab-U) leaf-full-binary-tree star star = lab-U star - compute-tr-Eq-labeling-full-binary-tree + tr-Eq-labeling-full-binary-tree (join-full-binary-tree U U₁ , lab-U) (join-full-binary-tree V V₁) (p , q) (inl x) = - compute-tr-Eq-labeling-full-binary-tree (U , λ y → lab-U (inl y)) V p x - compute-tr-Eq-labeling-full-binary-tree + tr-Eq-labeling-full-binary-tree (U , λ y → lab-U (inl y)) V p x + tr-Eq-labeling-full-binary-tree (join-full-binary-tree U U₁ , lab-U) (join-full-binary-tree V V₁) (p , q) (inr x) = - compute-tr-Eq-labeling-full-binary-tree (U₁ , λ y → lab-U (inr y)) V₁ q x + tr-Eq-labeling-full-binary-tree (U₁ , λ y → lab-U (inr y)) V₁ q x ``` -### Characterizing the identity type of labeled full binary trees +### Characterizing identifications of labeled full binary trees ```agda module _ @@ -100,168 +110,174 @@ module _ Eq-full-binary-tree (pr1 U) (pr1 V) → UU l Eq-htpy-labeled-full-binary-tree U V p = - compute-tr-Eq-labeling-full-binary-tree X U (pr1 V) p ~ pr2 V + tr-Eq-labeling-full-binary-tree X U (pr1 V) p ~ pr2 V + + 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 (pr1 U) (pr1 V)) + ( Eq-htpy-labeled-full-binary-tree U V) - refl-compute-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → f = g → + refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + f = g → Eq-htpy-labeled-full-binary-tree (T , f) (T , g) (refl-Eq-full-binary-tree T) - refl-compute-tr-Eq-labeling-full-binary-tree + refl-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f f refl star = refl - refl-compute-tr-Eq-labeling-full-binary-tree + refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree T T₁) f f refl (inl x) = - refl-compute-tr-Eq-labeling-full-binary-tree T + refl-tr-Eq-labeling-full-binary-tree T ( λ y → f (inl y)) (λ y → f (inl y)) refl x - refl-compute-tr-Eq-labeling-full-binary-tree + refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree T T₁) f f refl (inr x) = - refl-compute-tr-Eq-labeling-full-binary-tree T₁ + refl-tr-Eq-labeling-full-binary-tree T₁ ( λ y → f (inr y)) (λ y → f (inr y)) refl x - eq-inl-compute-tr-Eq-labeling-full-binary-tree : - (U V : full-binary-tree) - (f : labeling-full-binary-tree X (join-full-binary-tree U V)) - (x : node-full-binary-tree U) → - f (inl x) = compute-tr-Eq-labeling-full-binary-tree X - (U , λ y → f (inl y)) U - (refl-Eq-full-binary-tree U) x - eq-inl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree _ f star = refl - eq-inl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree U U₁) _ f (inl x) = - eq-inl-compute-tr-Eq-labeling-full-binary-tree U U₁ (λ z → f (inl z)) x - eq-inl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree U U₁) _ f (inr x) = - eq-inl-compute-tr-Eq-labeling-full-binary-tree U₁ U lab x - where - lab : labeling-full-binary-tree X (join-full-binary-tree U₁ U) - lab (inl y) = f (inl (inr y)) - lab (inr y) = f (inl (inl y)) - - eq-inr-compute-tr-Eq-labeling-full-binary-tree : (U V : full-binary-tree) - (f : labeling-full-binary-tree X (join-full-binary-tree U V)) - (x : node-full-binary-tree V) → - f (inr x) = compute-tr-Eq-labeling-full-binary-tree X - (V , λ y → f (inr y)) V - (refl-Eq-full-binary-tree V) x - eq-inr-compute-tr-Eq-labeling-full-binary-tree - _ leaf-full-binary-tree f star = refl - eq-inr-compute-tr-Eq-labeling-full-binary-tree - _ (join-full-binary-tree V V₁) f (inl x) = - eq-inr-compute-tr-Eq-labeling-full-binary-tree V₁ V lab x - where - lab : labeling-full-binary-tree X (join-full-binary-tree V₁ V) - lab (inl y) = f (inr (inl x)) - lab (inr y) = f (inr (inl y)) - eq-inr-compute-tr-Eq-labeling-full-binary-tree - _ (join-full-binary-tree V V₁) f (inr x) = - eq-inr-compute-tr-Eq-labeling-full-binary-tree V V₁ (λ z → f (inr z)) x - - inv-refl-compute-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - Eq-htpy-labeled-full-binary-tree (T , f) (T , g) - (refl-Eq-full-binary-tree T) → - f = g - inv-refl-compute-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f g p = - eq-htpy (λ x → p star) - inv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g p = - eq-htpy htpy - where - htpy : f ~ g - htpy (inl x) = - eq-inl-compute-tr-Eq-labeling-full-binary-tree T T₁ f x ∙ p (inl x) - htpy (inr x) = - eq-inr-compute-tr-Eq-labeling-full-binary-tree T T₁ f x ∙ p (inr x) - - is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - is-equiv (refl-compute-tr-Eq-labeling-full-binary-tree T f g) - pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = - inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g - pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g)) p = eq-htpy htpy - where - htpy : - (refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g ∘ - pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f g))) p ~ - p - htpy star = ap {! !} {! !} ∙ {! !} - pr2 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g)) p = eq-htpy htpy - where - htpy : - (refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g ∘ - pr1 (pr1 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f g))) p ~ - p - htpy (inl x) = {! !} - htpy (inr x) = {! !} - pr1 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree T f g)) = - inv-refl-compute-tr-Eq-labeling-full-binary-tree T f g - pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f f)) refl = {! !} - pr2 (pr2 (is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f f)) refl = {! !} - - Eq-labeled-full-binary-tree : - labeled-full-binary-tree X → labeled-full-binary-tree X → UU l - Eq-labeled-full-binary-tree (U , lab-U) (V , lab-V) = - Σ - ( Eq-full-binary-tree U V) - ( Eq-htpy-labeled-full-binary-tree (U , lab-U) (V , lab-V)) - {-# TERMINATING #-} - refl-Eq-htpy-labeled-full-binary-tree : + compute-tr-refl-Eq-labeling-full-binary-tree : (U : labeled-full-binary-tree X) → - Eq-htpy-labeled-full-binary-tree U U (refl-Eq-full-binary-tree (pr1 U)) - refl-Eq-htpy-labeled-full-binary-tree (leaf-full-binary-tree , lab-U) star = - refl - refl-Eq-htpy-labeled-full-binary-tree - (join-full-binary-tree U V , lab) (inl x) = - refl-Eq-htpy-labeled-full-binary-tree (U , (λ y → lab (inl y))) x - refl-Eq-htpy-labeled-full-binary-tree - (join-full-binary-tree U V , lab) (inr x) = - refl-Eq-htpy-labeled-full-binary-tree (V , (λ y → lab (inr y))) x + pr2 U ~ + tr-Eq-labeling-full-binary-tree X U (pr1 U) + (refl-Eq-full-binary-tree (pr1 U)) + compute-tr-refl-Eq-labeling-full-binary-tree + (leaf-full-binary-tree , _) star = refl + compute-tr-refl-Eq-labeling-full-binary-tree + (join-full-binary-tree L R , lab) (inl x) = + compute-tr-refl-Eq-labeling-full-binary-tree (L , (λ y → lab (inl y))) x + compute-tr-refl-Eq-labeling-full-binary-tree + (join-full-binary-tree L R , lab) (inr x) = + compute-tr-refl-Eq-labeling-full-binary-tree (R , (λ y → lab (inr y))) x + + compute-tr-Eq-labeling-full-binary-tree' : + (U : labeled-full-binary-tree X) + (V : full-binary-tree) + (p : pr1 U = V) → + tr (labeling-full-binary-tree X) p (pr2 U) ~ + tr-Eq-labeling-full-binary-tree X U V (Eq-eq-full-binary-tree p) + compute-tr-Eq-labeling-full-binary-tree' + (leaf-full-binary-tree , lab) leaf-full-binary-tree refl star = refl + compute-tr-Eq-labeling-full-binary-tree' + (join-full-binary-tree V W , lab) + (join-full-binary-tree V W) refl = + compute-tr-refl-Eq-labeling-full-binary-tree + ( join-full-binary-tree V W , lab) + + refl-Eq-labeled-full-binary-tree : + (T : labeled-full-binary-tree X) → Eq-labeled-full-binary-tree T T + pr1 (refl-Eq-labeled-full-binary-tree (T , _)) = refl-Eq-full-binary-tree T + pr2 (refl-Eq-labeled-full-binary-tree (T , lab)) = + refl-tr-Eq-labeling-full-binary-tree T lab lab refl + + compute-tr-Eq-labeling-full-binary-tree : + (U V : labeled-full-binary-tree X) (p : Eq-labeled-full-binary-tree U V) → + dependent-identification + (labeling-full-binary-tree X) + (eq-Eq-full-binary-tree (pr1 U) (pr1 V) (pr1 p)) + (pr2 U) (pr2 V) + compute-tr-Eq-labeling-full-binary-tree + (leaf-full-binary-tree , lab-U) (leaf-full-binary-tree , lab-V) (star , p) = + eq-htpy (λ x → p star) + compute-tr-Eq-labeling-full-binary-tree + (join-full-binary-tree U U₁ , lab-U) (join-full-binary-tree V V₁ , lab-V) + (p , q) = + eq-htpy htpy + where + htpy : + tr (labeling-full-binary-tree X) + (eq-Eq-full-binary-tree + (join-full-binary-tree U U₁) + (join-full-binary-tree V V₁) p) + lab-U ~ + lab-V + htpy = + compute-tr-Eq-labeling-full-binary-tree' + ( join-full-binary-tree U U₁ , lab-U) + ( join-full-binary-tree V V₁) + ( eq-Eq-full-binary-tree + ( join-full-binary-tree U U₁) + ( join-full-binary-tree V V₁) + p) ∙h + ( λ x → ap (λ r → tr-Eq-labeling-full-binary-tree X + ( join-full-binary-tree U U₁ , lab-U) + ( join-full-binary-tree V V₁) r x) + ( eq-is-prop (is-prop-Eq-full-binary-tree + ( join-full-binary-tree U U₁) + ( join-full-binary-tree V V₁)))) ∙h + q Eq-eq-labeled-full-binary-tree : (U V : labeled-full-binary-tree X) → U = V → Eq-labeled-full-binary-tree U V - pr1 (Eq-eq-labeled-full-binary-tree U U refl) = - refl-Eq-full-binary-tree (pr1 U) - pr2 (Eq-eq-labeled-full-binary-tree U U refl) = - refl-Eq-htpy-labeled-full-binary-tree U - - 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 = - structure-identity-principle - ( λ {x} f p → Eq-htpy-labeled-full-binary-tree U (x , f) p) - ( refl-Eq-full-binary-tree (pr1 U)) - ( refl-Eq-htpy-labeled-full-binary-tree U) - ( Eq-eq-labeled-full-binary-tree U) - ( λ _ → is-equiv-Eq-eq-full-binary-tree) - ( λ y → is-equiv-refl-compute-tr-Eq-labeling-full-binary-tree - ( pr1 U) (pr2 U) y) - - 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 U refl = refl-Eq-labeled-full-binary-tree U 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) + eq-Eq-labeled-full-binary-tree (U , lab-U) (V , lab-V) (p , q) = + eq-pair-Σ + ( eq-Eq-full-binary-tree U V p) + ( compute-tr-Eq-labeling-full-binary-tree (U , lab-U) (V , lab-V) (p , q)) + + dependent-identification-Eq-labeled-full-binary-tree : + (T U : labeled-full-binary-tree X) (p : Eq-labeled-full-binary-tree T U) → + dependent-identification + (Eq-labeled-full-binary-tree T) + (eq-Eq-labeled-full-binary-tree T U p) + (refl-Eq-labeled-full-binary-tree T) + p + dependent-identification-Eq-labeled-full-binary-tree + (leaf-full-binary-tree , lab-T) (leaf-full-binary-tree , lab-U) (star , p) = + eq-pair-Σ refl (eq-htpy htpy) + where + htpy : + tr (Eq-htpy-labeled-full-binary-tree + ( leaf-full-binary-tree , lab-T) + ( leaf-full-binary-tree , lab-U)) + refl (pr2 (tr (Eq-labeled-full-binary-tree + ( leaf-full-binary-tree , lab-T)) + ( eq-Eq-labeled-full-binary-tree (leaf-full-binary-tree , lab-T) + ( leaf-full-binary-tree , lab-U) (star , p)) + ( refl-Eq-labeled-full-binary-tree + ( leaf-full-binary-tree , lab-T)))) ~ p + htpy star = {! !} + dependent-identification-Eq-labeled-full-binary-tree + (join-full-binary-tree T T₁ , lab-T) + (join-full-binary-tree U U₁ , lab-U) ((p , q) , r) = + eq-pair-Σ + ( eq-pair + ( eq-is-prop (is-prop-Eq-full-binary-tree T U)) + ( eq-is-prop (is-prop-Eq-full-binary-tree T₁ U₁))) + ( eq-htpy htpy) + where + htpy : + tr + (Eq-htpy-labeled-full-binary-tree + (join-full-binary-tree T T₁ , lab-T) + (join-full-binary-tree U U₁ , lab-U)) + (eq-pair (eq-is-prop (is-prop-Eq-full-binary-tree T U)) + (eq-is-prop (is-prop-Eq-full-binary-tree T₁ U₁))) + (pr2 + (tr + (Eq-labeled-full-binary-tree (join-full-binary-tree T T₁ , lab-T)) + (eq-Eq-labeled-full-binary-tree + (join-full-binary-tree T T₁ , lab-T) + (join-full-binary-tree U U₁ , lab-U) ((p , q) , r)) + (refl-Eq-labeled-full-binary-tree + (join-full-binary-tree T T₁ , lab-T)))) ~ r + htpy (inl x) = {! !} + htpy (inr x) = {! !} + + is-torsorial-Eq-labeled-full-binary-tree : + (T : labeled-full-binary-tree X) → + is-torsorial (Eq-labeled-full-binary-tree T) + pr1 (is-torsorial-Eq-labeled-full-binary-tree T) = + T , (refl-Eq-labeled-full-binary-tree T) + pr2 (is-torsorial-Eq-labeled-full-binary-tree T) (U , p) = + eq-pair-Σ + ( eq-Eq-labeled-full-binary-tree T U p) + (dependent-identification-Eq-labeled-full-binary-tree T U p) ``` From 42e3ded668e76b02815e7a1b444c46912066cc03 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 10 Aug 2025 20:02:43 -0600 Subject: [PATCH 54/63] going back to structure identity principle formalism. lots of cleaning up to do, three goals remain, but I think it was the right decision --- src/trees/labeled-full-binary-trees.lagda.md | 166 ++++++++++++------- 1 file changed, 108 insertions(+), 58 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 68c5af82d3..4d5045cce7 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -150,6 +150,29 @@ module _ (join-full-binary-tree L R , lab) (inr x) = compute-tr-refl-Eq-labeling-full-binary-tree (R , (λ y → lab (inr y))) x + refl-Eq-htpy-labeled-full-binary-tree : + (T : full-binary-tree) (f : labeling-full-binary-tree X T) → + Eq-htpy-labeled-full-binary-tree (T , f) (T , f) (refl-Eq-full-binary-tree T) + refl-Eq-htpy-labeled-full-binary-tree T f = + inv-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f)) + + compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree : + (T : full-binary-tree) (f : labeling-full-binary-tree X T) → + refl-tr-Eq-labeling-full-binary-tree T f f refl = + refl-Eq-htpy-labeled-full-binary-tree T f + compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree leaf-full-binary-tree f = + refl + compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree + (join-full-binary-tree L R) f = + eq-htpy htpy + where + htpy : + refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree L R) + f f refl ~ + refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree L R) f + htpy (inl x) = htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree L (λ y → f (inl y))) x + htpy (inr x) = htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree R (λ y → f (inr y))) x + compute-tr-Eq-labeling-full-binary-tree' : (U : labeled-full-binary-tree X) (V : full-binary-tree) @@ -222,62 +245,89 @@ module _ ( eq-Eq-full-binary-tree U V p) ( compute-tr-Eq-labeling-full-binary-tree (U , lab-U) (V , lab-V) (p , q)) - dependent-identification-Eq-labeled-full-binary-tree : - (T U : labeled-full-binary-tree X) (p : Eq-labeled-full-binary-tree T U) → - dependent-identification - (Eq-labeled-full-binary-tree T) - (eq-Eq-labeled-full-binary-tree T U p) - (refl-Eq-labeled-full-binary-tree T) - p - dependent-identification-Eq-labeled-full-binary-tree - (leaf-full-binary-tree , lab-T) (leaf-full-binary-tree , lab-U) (star , p) = - eq-pair-Σ refl (eq-htpy htpy) - where - htpy : - tr (Eq-htpy-labeled-full-binary-tree - ( leaf-full-binary-tree , lab-T) - ( leaf-full-binary-tree , lab-U)) - refl (pr2 (tr (Eq-labeled-full-binary-tree - ( leaf-full-binary-tree , lab-T)) - ( eq-Eq-labeled-full-binary-tree (leaf-full-binary-tree , lab-T) - ( leaf-full-binary-tree , lab-U) (star , p)) - ( refl-Eq-labeled-full-binary-tree - ( leaf-full-binary-tree , lab-T)))) ~ p - htpy star = {! !} - dependent-identification-Eq-labeled-full-binary-tree - (join-full-binary-tree T T₁ , lab-T) - (join-full-binary-tree U U₁ , lab-U) ((p , q) , r) = - eq-pair-Σ - ( eq-pair - ( eq-is-prop (is-prop-Eq-full-binary-tree T U)) - ( eq-is-prop (is-prop-Eq-full-binary-tree T₁ U₁))) - ( eq-htpy htpy) - where - htpy : - tr - (Eq-htpy-labeled-full-binary-tree - (join-full-binary-tree T T₁ , lab-T) - (join-full-binary-tree U U₁ , lab-U)) - (eq-pair (eq-is-prop (is-prop-Eq-full-binary-tree T U)) - (eq-is-prop (is-prop-Eq-full-binary-tree T₁ U₁))) - (pr2 - (tr - (Eq-labeled-full-binary-tree (join-full-binary-tree T T₁ , lab-T)) - (eq-Eq-labeled-full-binary-tree - (join-full-binary-tree T T₁ , lab-T) - (join-full-binary-tree U U₁ , lab-U) ((p , q) , r)) - (refl-Eq-labeled-full-binary-tree - (join-full-binary-tree T T₁ , lab-T)))) ~ r - htpy (inl x) = {! !} - htpy (inr x) = {! !} - - is-torsorial-Eq-labeled-full-binary-tree : - (T : labeled-full-binary-tree X) → - is-torsorial (Eq-labeled-full-binary-tree T) - pr1 (is-torsorial-Eq-labeled-full-binary-tree T) = - T , (refl-Eq-labeled-full-binary-tree T) - pr2 (is-torsorial-Eq-labeled-full-binary-tree T) (U , p) = - eq-pair-Σ - ( eq-Eq-labeled-full-binary-tree T U p) - (dependent-identification-Eq-labeled-full-binary-tree T U p) + inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + Eq-htpy-labeled-full-binary-tree (T , f) (T , g) + (refl-Eq-full-binary-tree T) → + f = g + inv-refl-tr-Eq-labeling-full-binary-tree T f g p = + eq-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h p) + + htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f : labeling-full-binary-tree X T) → + compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h refl-Eq-htpy-labeled-full-binary-tree T f = refl-htpy + htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f = refl + htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree L R) f = eq-htpy htpy + where + htpy : compute-tr-refl-Eq-labeling-full-binary-tree (join-full-binary-tree L R , f) ∙h refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree L R) f ~ refl-htpy + htpy (inl x) = {! !} + htpy (inr x) = {! !} + + compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f : labeling-full-binary-tree X T) → + inv-refl-tr-Eq-labeling-full-binary-tree T f f + (refl-Eq-htpy-labeled-full-binary-tree T f) = + refl + compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f = + ap eq-htpy (htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f) ∙ eq-htpy-refl-htpy f + + compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) + (p : Eq-htpy-labeled-full-binary-tree + (T , f) (T , g) (refl-Eq-full-binary-tree T)) → + (refl-tr-Eq-labeling-full-binary-tree T f g ∘ + inv-refl-tr-Eq-labeling-full-binary-tree T f g) p ~ + p + compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p x = {! !} + + is-section-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + is-section + (refl-tr-Eq-labeling-full-binary-tree T f g) + (inv-refl-tr-Eq-labeling-full-binary-tree T f g) + is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = + eq-htpy + ( compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p) + + is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f : labeling-full-binary-tree X T) → + (inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ + refl-tr-Eq-labeling-full-binary-tree T f f) + refl = + refl + is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree T f = + equational-reasoning + ( inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ + refl-tr-Eq-labeling-full-binary-tree T f f) + refl + = inv-refl-tr-Eq-labeling-full-binary-tree T f f + ( refl-Eq-htpy-labeled-full-binary-tree T f) + by ap (inv-refl-tr-Eq-labeling-full-binary-tree T f f) + ( compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree T f) + = refl + by compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f + + is-equiv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → + is-equiv (refl-tr-Eq-labeling-full-binary-tree T f g) + pr1 (pr1 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = + inv-refl-tr-Eq-labeling-full-binary-tree T f g + pr2 (pr1 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = + is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g + pr1 (pr2 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = + inv-refl-tr-Eq-labeling-full-binary-tree T f g + pr2 (pr2 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f f)) refl = + is-retraction-inv-refl-tr-Eq-labeling-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 = + structure-identity-principle + ( λ {T} lab p → Eq-htpy-labeled-full-binary-tree U (T , lab) p) + ( refl-Eq-full-binary-tree (pr1 U)) + ( refl-tr-Eq-labeling-full-binary-tree (pr1 U) (pr2 U) (pr2 U) refl) + ( Eq-eq-labeled-full-binary-tree U) + ( λ T → is-equiv-Eq-eq-full-binary-tree) + ( λ lab → is-equiv-refl-tr-Eq-labeling-full-binary-tree (pr1 U) (pr2 U) lab) ``` From ab59e764bf45782741cba9f1124c3b2dbf6c9f71 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 11 Aug 2025 13:20:24 -0600 Subject: [PATCH 55/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 41 +------------------- 1 file changed, 2 insertions(+), 39 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 4d5045cce7..bf433e27bc 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -236,15 +236,6 @@ module _ Eq-labeled-full-binary-tree U V Eq-eq-labeled-full-binary-tree U U refl = refl-Eq-labeled-full-binary-tree U - 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 , lab-U) (V , lab-V) (p , q) = - eq-pair-Σ - ( eq-Eq-full-binary-tree U V p) - ( compute-tr-Eq-labeling-full-binary-tree (U , lab-U) (V , lab-V) (p , q)) - inv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → Eq-htpy-labeled-full-binary-tree (T , f) (T , g) @@ -253,41 +244,13 @@ module _ inv-refl-tr-Eq-labeling-full-binary-tree T f g p = eq-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h p) - htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f : labeling-full-binary-tree X T) → - compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h refl-Eq-htpy-labeled-full-binary-tree T f = refl-htpy - htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree leaf-full-binary-tree f = refl - htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree L R) f = eq-htpy htpy - where - htpy : compute-tr-refl-Eq-labeling-full-binary-tree (join-full-binary-tree L R , f) ∙h refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree L R) f ~ refl-htpy - htpy (inl x) = {! !} - htpy (inr x) = {! !} - - compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f : labeling-full-binary-tree X T) → - inv-refl-tr-Eq-labeling-full-binary-tree T f f - (refl-Eq-htpy-labeled-full-binary-tree T f) = - refl - compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f = - ap eq-htpy (htpy-compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f) ∙ eq-htpy-refl-htpy f - - compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) - (p : Eq-htpy-labeled-full-binary-tree - (T , f) (T , g) (refl-Eq-full-binary-tree T)) → - (refl-tr-Eq-labeling-full-binary-tree T f g ∘ - inv-refl-tr-Eq-labeling-full-binary-tree T f g) p ~ - p - compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p x = {! !} - is-section-inv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → is-section (refl-tr-Eq-labeling-full-binary-tree T f g) (inv-refl-tr-Eq-labeling-full-binary-tree T f g) is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = - eq-htpy - ( compute-htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p) + eq-htpy {! !} is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f : labeling-full-binary-tree X T) → @@ -305,7 +268,7 @@ module _ by ap (inv-refl-tr-Eq-labeling-full-binary-tree T f f) ( compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree T f) = refl - by compute-refl-Eq-htpy-inv-refl-tr-Eq-labeling-full-binary-tree T f + by {! !} is-equiv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → From 13dfb8816d97b544ad2558cc3445a65c64efcffb Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Tue, 12 Aug 2025 17:07:18 -0600 Subject: [PATCH 56/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 21 ++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index bf433e27bc..8c4a3f412a 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -170,8 +170,12 @@ module _ refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree L R) f f refl ~ refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree L R) f - htpy (inl x) = htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree L (λ y → f (inl y))) x - htpy (inr x) = htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree R (λ y → f (inr y))) x + htpy (inl x) = + htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree L + ( λ y → f (inl y))) x + htpy (inr x) = + htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree R + ( λ y → f (inr y))) x compute-tr-Eq-labeling-full-binary-tree' : (U : labeled-full-binary-tree X) @@ -244,13 +248,22 @@ module _ inv-refl-tr-Eq-labeling-full-binary-tree T f g p = eq-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h p) + htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree : + (T : full-binary-tree) (f g : labeling-full-binary-tree X T) + (p : Eq-htpy-labeled-full-binary-tree (T , f) (T , g) + (refl-Eq-full-binary-tree T)) → + (refl-tr-Eq-labeling-full-binary-tree T f g ∘ + inv-refl-tr-Eq-labeling-full-binary-tree T f g) p ~ + p + htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = {! !} + is-section-inv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → is-section (refl-tr-Eq-labeling-full-binary-tree T f g) (inv-refl-tr-Eq-labeling-full-binary-tree T f g) is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = - eq-htpy {! !} + eq-htpy (htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p) is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree : (T : full-binary-tree) (f : labeling-full-binary-tree X T) → @@ -260,7 +273,7 @@ module _ refl is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree T f = equational-reasoning - ( inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ + ( inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ refl-tr-Eq-labeling-full-binary-tree T f f) refl = inv-refl-tr-Eq-labeling-full-binary-tree T f f From b5f85cfc408b0937d318c9d2ea615bcdf705771a Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 14:32:48 -0600 Subject: [PATCH 57/63] refactoring everything to not use tr (hard to compute with!) --- src/trees/labeled-full-binary-trees.lagda.md | 255 ++++--------------- 1 file changed, 49 insertions(+), 206 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 8c4a3f412a..03784088db 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -63,6 +63,14 @@ module _ 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 @@ -74,30 +82,6 @@ This is simply the weight of its underlying full binary tree. weight-labeled-full-binary-tree (T , _) = weight-full-binary-tree T ``` -### Computing transport of labelings along identifications of full binary trees - -```agda -module _ - {l : Level} (X : UU l) - where - - tr-Eq-labeling-full-binary-tree : - (U : labeled-full-binary-tree X) - (V : full-binary-tree) → - Eq-full-binary-tree (pr1 U) V → - labeling-full-binary-tree X V - tr-Eq-labeling-full-binary-tree - (leaf-full-binary-tree , lab-U) leaf-full-binary-tree star star = lab-U star - tr-Eq-labeling-full-binary-tree - (join-full-binary-tree U U₁ , lab-U) - (join-full-binary-tree V V₁) (p , q) (inl x) = - tr-Eq-labeling-full-binary-tree (U , λ y → lab-U (inl y)) V p x - tr-Eq-labeling-full-binary-tree - (join-full-binary-tree U U₁ , lab-U) - (join-full-binary-tree V V₁) (p , q) (inr x) = - tr-Eq-labeling-full-binary-tree (U₁ , λ y → lab-U (inr y)) V₁ q x -``` - ### Characterizing identifications of labeled full binary trees ```agda @@ -105,205 +89,64 @@ module _ {l : Level} (X : UU l) where + {-# TERMINATING #-} Eq-htpy-labeled-full-binary-tree : (U V : labeled-full-binary-tree X) → - Eq-full-binary-tree (pr1 U) (pr1 V) → + Eq-full-binary-tree + (tree-labeled-full-binary-tree X U) + (tree-labeled-full-binary-tree X V) → UU l - Eq-htpy-labeled-full-binary-tree U V p = - tr-Eq-labeling-full-binary-tree X U (pr1 V) p ~ pr2 V + Eq-htpy-labeled-full-binary-tree + (leaf-full-binary-tree , f) (leaf-full-binary-tree , g) star = + f star = g star + Eq-htpy-labeled-full-binary-tree + (join-full-binary-tree U U₁ , f) (join-full-binary-tree V V₁ , g) (p , q) = + ( Eq-htpy-labeled-full-binary-tree + ( U , (λ z → f (inl z))) (V , (λ z → g (inl z))) p) × + ( Eq-htpy-labeled-full-binary-tree + ( U₁ , (λ z → f (inr z))) (V₁ , (λ z → g (inr z))) q) + + {-# TERMINATING #-} + refl-Eq-htpy-labeled-full-binary-tree : + (T : labeled-full-binary-tree X) → + Eq-htpy-labeled-full-binary-tree T T + (refl-Eq-full-binary-tree (tree-labeled-full-binary-tree X T)) + refl-Eq-htpy-labeled-full-binary-tree (leaf-full-binary-tree , f) = refl + pr1 (refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) = + refl-Eq-htpy-labeled-full-binary-tree (T , λ z → f (inl z)) + pr2 (refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) = + refl-Eq-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 (pr1 U) (pr1 V)) + Σ ( Eq-full-binary-tree + ( tree-labeled-full-binary-tree X U) + ( tree-labeled-full-binary-tree X V)) ( Eq-htpy-labeled-full-binary-tree U V) - refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - f = g → - Eq-htpy-labeled-full-binary-tree (T , f) (T , g) - (refl-Eq-full-binary-tree T) - refl-tr-Eq-labeling-full-binary-tree - leaf-full-binary-tree f f refl star = - refl - refl-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f f refl (inl x) = - refl-tr-Eq-labeling-full-binary-tree T - ( λ y → f (inl y)) (λ y → f (inl y)) refl x - refl-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree T T₁) f f refl (inr x) = - refl-tr-Eq-labeling-full-binary-tree T₁ - ( λ y → f (inr y)) (λ y → f (inr y)) refl x - - {-# TERMINATING #-} - compute-tr-refl-Eq-labeling-full-binary-tree : - (U : labeled-full-binary-tree X) → - pr2 U ~ - tr-Eq-labeling-full-binary-tree X U (pr1 U) - (refl-Eq-full-binary-tree (pr1 U)) - compute-tr-refl-Eq-labeling-full-binary-tree - (leaf-full-binary-tree , _) star = refl - compute-tr-refl-Eq-labeling-full-binary-tree - (join-full-binary-tree L R , lab) (inl x) = - compute-tr-refl-Eq-labeling-full-binary-tree (L , (λ y → lab (inl y))) x - compute-tr-refl-Eq-labeling-full-binary-tree - (join-full-binary-tree L R , lab) (inr x) = - compute-tr-refl-Eq-labeling-full-binary-tree (R , (λ y → lab (inr y))) x - - refl-Eq-htpy-labeled-full-binary-tree : - (T : full-binary-tree) (f : labeling-full-binary-tree X T) → - Eq-htpy-labeled-full-binary-tree (T , f) (T , f) (refl-Eq-full-binary-tree T) - refl-Eq-htpy-labeled-full-binary-tree T f = - inv-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f)) - - compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree : - (T : full-binary-tree) (f : labeling-full-binary-tree X T) → - refl-tr-Eq-labeling-full-binary-tree T f f refl = - refl-Eq-htpy-labeled-full-binary-tree T f - compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree leaf-full-binary-tree f = - refl - compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree - (join-full-binary-tree L R) f = - eq-htpy htpy - where - htpy : - refl-tr-Eq-labeling-full-binary-tree (join-full-binary-tree L R) - f f refl ~ - refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree L R) f - htpy (inl x) = - htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree L - ( λ y → f (inl y))) x - htpy (inr x) = - htpy-eq (compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree R - ( λ y → f (inr y))) x - - compute-tr-Eq-labeling-full-binary-tree' : - (U : labeled-full-binary-tree X) - (V : full-binary-tree) - (p : pr1 U = V) → - tr (labeling-full-binary-tree X) p (pr2 U) ~ - tr-Eq-labeling-full-binary-tree X U V (Eq-eq-full-binary-tree p) - compute-tr-Eq-labeling-full-binary-tree' - (leaf-full-binary-tree , lab) leaf-full-binary-tree refl star = refl - compute-tr-Eq-labeling-full-binary-tree' - (join-full-binary-tree V W , lab) - (join-full-binary-tree V W) refl = - compute-tr-refl-Eq-labeling-full-binary-tree - ( join-full-binary-tree V W , lab) - refl-Eq-labeled-full-binary-tree : (T : labeled-full-binary-tree X) → Eq-labeled-full-binary-tree T T - pr1 (refl-Eq-labeled-full-binary-tree (T , _)) = refl-Eq-full-binary-tree T - pr2 (refl-Eq-labeled-full-binary-tree (T , lab)) = - refl-tr-Eq-labeling-full-binary-tree T lab lab refl - - compute-tr-Eq-labeling-full-binary-tree : - (U V : labeled-full-binary-tree X) (p : Eq-labeled-full-binary-tree U V) → - dependent-identification - (labeling-full-binary-tree X) - (eq-Eq-full-binary-tree (pr1 U) (pr1 V) (pr1 p)) - (pr2 U) (pr2 V) - compute-tr-Eq-labeling-full-binary-tree - (leaf-full-binary-tree , lab-U) (leaf-full-binary-tree , lab-V) (star , p) = - eq-htpy (λ x → p star) - compute-tr-Eq-labeling-full-binary-tree - (join-full-binary-tree U U₁ , lab-U) (join-full-binary-tree V V₁ , lab-V) - (p , q) = - eq-htpy htpy - where - htpy : - tr (labeling-full-binary-tree X) - (eq-Eq-full-binary-tree - (join-full-binary-tree U U₁) - (join-full-binary-tree V V₁) p) - lab-U ~ - lab-V - htpy = - compute-tr-Eq-labeling-full-binary-tree' - ( join-full-binary-tree U U₁ , lab-U) - ( join-full-binary-tree V V₁) - ( eq-Eq-full-binary-tree - ( join-full-binary-tree U U₁) - ( join-full-binary-tree V V₁) - p) ∙h - ( λ x → ap (λ r → tr-Eq-labeling-full-binary-tree X - ( join-full-binary-tree U U₁ , lab-U) - ( join-full-binary-tree V V₁) r x) - ( eq-is-prop (is-prop-Eq-full-binary-tree - ( join-full-binary-tree U U₁) - ( join-full-binary-tree V V₁)))) ∙h - q + 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-Eq-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 → + (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 - - inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - Eq-htpy-labeled-full-binary-tree (T , f) (T , g) - (refl-Eq-full-binary-tree T) → - f = g - inv-refl-tr-Eq-labeling-full-binary-tree T f g p = - eq-htpy (compute-tr-refl-Eq-labeling-full-binary-tree (T , f) ∙h p) - - htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) - (p : Eq-htpy-labeled-full-binary-tree (T , f) (T , g) - (refl-Eq-full-binary-tree T)) → - (refl-tr-Eq-labeling-full-binary-tree T f g ∘ - inv-refl-tr-Eq-labeling-full-binary-tree T f g) p ~ - p - htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = {! !} - - is-section-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - is-section - (refl-tr-Eq-labeling-full-binary-tree T f g) - (inv-refl-tr-Eq-labeling-full-binary-tree T f g) - is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p = - eq-htpy (htpy-is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g p) - - is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f : labeling-full-binary-tree X T) → - (inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ - refl-tr-Eq-labeling-full-binary-tree T f f) - refl = - refl - is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree T f = - equational-reasoning - ( inv-refl-tr-Eq-labeling-full-binary-tree T f f ∘ - refl-tr-Eq-labeling-full-binary-tree T f f) - refl - = inv-refl-tr-Eq-labeling-full-binary-tree T f f - ( refl-Eq-htpy-labeled-full-binary-tree T f) - by ap (inv-refl-tr-Eq-labeling-full-binary-tree T f f) - ( compute-refl-Eq-refl-tr-Eq-labeled-full-binary-tree T f) - = refl - by {! !} - - is-equiv-refl-tr-Eq-labeling-full-binary-tree : - (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → - is-equiv (refl-tr-Eq-labeling-full-binary-tree T f g) - pr1 (pr1 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = - inv-refl-tr-Eq-labeling-full-binary-tree T f g - pr2 (pr1 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = - is-section-inv-refl-tr-Eq-labeling-full-binary-tree T f g - pr1 (pr2 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f g)) = - inv-refl-tr-Eq-labeling-full-binary-tree T f g - pr2 (pr2 (is-equiv-refl-tr-Eq-labeling-full-binary-tree T f f)) refl = - is-retraction-inv-refl-tr-Eq-labeling-full-binary-tree T f + Eq-eq-labeled-full-binary-tree U .U refl = refl-Eq-labeled-full-binary-tree U 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 = + is-equiv-Eq-eq-labeled-full-binary-tree (U , f) = structure-identity-principle - ( λ {T} lab p → Eq-htpy-labeled-full-binary-tree U (T , lab) p) - ( refl-Eq-full-binary-tree (pr1 U)) - ( refl-tr-Eq-labeling-full-binary-tree (pr1 U) (pr2 U) (pr2 U) refl) - ( Eq-eq-labeled-full-binary-tree U) - ( λ T → is-equiv-Eq-eq-full-binary-tree) - ( λ lab → is-equiv-refl-tr-Eq-labeling-full-binary-tree (pr1 U) (pr2 U) lab) + {! !} + ( refl-Eq-full-binary-tree U) + ( refl-Eq-htpy-labeled-full-binary-tree (U , f)) + {! !} + {! !} + {! !} ``` From e139114196d5723c9017a4b060702d968aabd53b Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 14:54:05 -0600 Subject: [PATCH 58/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 64 ++++++++++++++------ 1 file changed, 45 insertions(+), 19 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 03784088db..3d404fdfba 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -15,6 +15,7 @@ open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.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.structure-identity-principle open import foundation.torsorial-type-families @@ -34,6 +35,7 @@ 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 @@ -90,32 +92,32 @@ module _ where {-# TERMINATING #-} - Eq-htpy-labeled-full-binary-tree : + 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 - Eq-htpy-labeled-full-binary-tree + htpy-labeled-full-binary-tree (leaf-full-binary-tree , f) (leaf-full-binary-tree , g) star = f star = g star - Eq-htpy-labeled-full-binary-tree + htpy-labeled-full-binary-tree (join-full-binary-tree U U₁ , f) (join-full-binary-tree V V₁ , g) (p , q) = - ( Eq-htpy-labeled-full-binary-tree + ( htpy-labeled-full-binary-tree ( U , (λ z → f (inl z))) (V , (λ z → g (inl z))) p) × - ( Eq-htpy-labeled-full-binary-tree + ( htpy-labeled-full-binary-tree ( U₁ , (λ z → f (inr z))) (V₁ , (λ z → g (inr z))) q) {-# TERMINATING #-} - refl-Eq-htpy-labeled-full-binary-tree : + refl-htpy-labeled-full-binary-tree : (T : labeled-full-binary-tree X) → - Eq-htpy-labeled-full-binary-tree T T + htpy-labeled-full-binary-tree T T (refl-Eq-full-binary-tree (tree-labeled-full-binary-tree X T)) - refl-Eq-htpy-labeled-full-binary-tree (leaf-full-binary-tree , f) = refl - pr1 (refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) = - refl-Eq-htpy-labeled-full-binary-tree (T , λ z → f (inl z)) - pr2 (refl-Eq-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁ , f)) = - refl-Eq-htpy-labeled-full-binary-tree (T₁ , λ z → f (inr z)) + 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 @@ -123,7 +125,7 @@ module _ Σ ( Eq-full-binary-tree ( tree-labeled-full-binary-tree X U) ( tree-labeled-full-binary-tree X V)) - ( Eq-htpy-labeled-full-binary-tree U 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 @@ -131,22 +133,46 @@ module _ 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-Eq-htpy-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) + + 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)) + pr1 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = f + pr2 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = + refl-htpy-labeled-full-binary-tree (T , f) + pr2 (is-torsorial-htpy-labeled-full-binary-tree T f) (g , p) = {! !} + + 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-Eq-htpy-labeled-full-binary-tree (U , f)) - {! !} - {! !} - {! !} + ( 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) ``` From a25cb11ccfaf1a06264c6549f53528dd847f1f3f Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 15:21:55 -0600 Subject: [PATCH 59/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 3d404fdfba..9a60ddc31a 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -154,7 +154,8 @@ module _ pr1 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = f pr2 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = refl-htpy-labeled-full-binary-tree (T , f) - pr2 (is-torsorial-htpy-labeled-full-binary-tree T f) (g , p) = {! !} + pr2 (is-torsorial-htpy-labeled-full-binary-tree leaf-full-binary-tree f) (g , p) = ? + pr2 (is-torsorial-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁) f) (g , p) = {! !} is-equiv-htpy-eq-labeled-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → From 4302cc647c06f8664d53d60f5cbb707f28a83783 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 15:22:02 -0600 Subject: [PATCH 60/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 9a60ddc31a..267b654ece 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -154,7 +154,7 @@ module _ pr1 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = f pr2 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = refl-htpy-labeled-full-binary-tree (T , f) - pr2 (is-torsorial-htpy-labeled-full-binary-tree leaf-full-binary-tree f) (g , p) = ? + pr2 (is-torsorial-htpy-labeled-full-binary-tree leaf-full-binary-tree f) (g , p) = {! !} pr2 (is-torsorial-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁) f) (g , p) = {! !} is-equiv-htpy-eq-labeled-full-binary-tree : From f0fe1c9636a0154cc7ac2dcd821e791e6d11793b Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 16:53:10 -0600 Subject: [PATCH 61/63] workinonit --- src/trees/labeled-full-binary-trees.lagda.md | 70 ++++++++++++++++++-- 1 file changed, 65 insertions(+), 5 deletions(-) diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 267b654ece..4bdda4c621 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -14,6 +14,7 @@ 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 @@ -26,6 +27,7 @@ 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 @@ -146,16 +148,74 @@ module _ 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)) + + 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 + ( {! !}) + ( {! !}) + 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))) p = + eq-htpy {! !} + 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)) - pr1 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = f - pr2 (pr1 (is-torsorial-htpy-labeled-full-binary-tree T f)) = - refl-htpy-labeled-full-binary-tree (T , f) - pr2 (is-torsorial-htpy-labeled-full-binary-tree leaf-full-binary-tree f) (g , p) = {! !} - pr2 (is-torsorial-htpy-labeled-full-binary-tree (join-full-binary-tree T T₁) f) (g , p) = {! !} + 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)) + ( fundamental-theorem-id' (λ g → htpy-eq) (funext f)) is-equiv-htpy-eq-labeled-full-binary-tree : (T : full-binary-tree) (f g : labeling-full-binary-tree X T) → From c74dec930ae70883f7e4110c9d78856787fe27c9 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 20:47:19 -0600 Subject: [PATCH 62/63] sigh --- .../combinator-full-binary-trees.lagda.md | 52 ++++++++----- .../free-magma-on-one-generator.lagda.md | 8 +- src/trees/free-magmas-on-types.lagda.md | 60 +++++++------- src/trees/labeled-full-binary-trees.lagda.md | 78 +++++++++++++++++-- 4 files changed, 136 insertions(+), 62 deletions(-) diff --git a/src/trees/combinator-full-binary-trees.lagda.md b/src/trees/combinator-full-binary-trees.lagda.md index b5a4bed278..8e6a5c760e 100644 --- a/src/trees/combinator-full-binary-trees.lagda.md +++ b/src/trees/combinator-full-binary-trees.lagda.md @@ -7,10 +7,12 @@ module trees.combinator-full-binary-trees where
Imports ```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 @@ -79,24 +81,38 @@ That is, for binary trees `L R : full-binary-tree` and an `X`-labeling `lab` of ``` ```agda -module _ +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)) - where - - htpy-combinator-commutes-with-labelings-full-binary-tree : - tr (labeling-full-binary-tree X) refl - ( pr2 (combinator-labeled-full-binary-tree X - ( L , λ x → lab (inl x)) (R , (λ x → lab (inr x))))) ~ - lab - htpy-combinator-commutes-with-labelings-full-binary-tree (inl x) = refl - htpy-combinator-commutes-with-labelings-full-binary-tree (inr x) = refl - - combinator-commutes-with-labelings-full-binary-tree : - combinator-labeled-full-binary-tree X - ( L , (λ x → lab (inl x))) (R , (λ x → lab (inr x))) = + (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) - combinator-commutes-with-labelings-full-binary-tree = - eq-pair-Σ refl - ( eq-htpy htpy-combinator-commutes-with-labelings-full-binary-tree) + ( 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 index f8f659a026..8aaecdcfc0 100644 --- a/src/trees/free-magma-on-one-generator.lagda.md +++ b/src/trees/free-magma-on-one-generator.lagda.md @@ -131,11 +131,13 @@ module _ ( λ T → is-retraction-extension-of-point-full-binary-tree-Magma T f)) ( refl) - ( pr2 f U V) + ( preserves-mul-map-hom-Magma full-binary-tree-Magma M f U V) ( ( ap - ( _∙ pr2 f U V) + ( _∙ preserves-mul-map-hom-Magma full-binary-tree-Magma M f U V) ( htpy-eq (is-section-eq-htpy _) _)) ∙ - ( is-section-inv-concat' (pr2 f U V) _) ∙ + ( 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) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index d4e1992853..d9f2f0ba55 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -131,40 +131,34 @@ module _ 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) (pr2 f) + ( λ 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-Π (eq-htpy - ( λ T → - is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) - ( λ T U → refl) U) V ∙ tr-Π (eq-htpy - ( λ T → - is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) - ( λ 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) - ( pr2 f U V) - ( ap (λ p → p ∙ pr2 f U V) (htpy-eq (is-section-eq-htpy - ( λ T → - is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f)) - ( combinator-labeled-full-binary-tree X U V)) ∙ - ( ap (λ p → ap-binary (pr2 M) - ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma - ( pr1 U , (λ x → pr2 U x)) (pr1 f , pr2 f)) - ( is-retraction-extension-of-map-labeled-full-binary-tree-Magma - ( pr1 V , (λ x → pr2 V x)) (pr1 f , pr2 f)) - ∙ inv (pr2 f (pr1 U , (λ x → pr2 U x)) (pr1 V , (λ x → pr2 V x))) - ∙ p ∙ pr2 f U V) (lem U V) ∙ -- this goal *should* be filled with a path that combinator-commutes-with-labelings-_ is refl but this isn't judgementally so... - {! !} ∙ - is-section-inv-concat' (pr2 f U V) _) ∙ - ap-binary-htpy - ( λ T → is-retraction-extension-of-map-labeled-full-binary-tree-Magma T f) - ( mul-Magma M)))) + 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 diff --git a/src/trees/labeled-full-binary-trees.lagda.md b/src/trees/labeled-full-binary-trees.lagda.md index 4bdda4c621..ee052ba36e 100644 --- a/src/trees/labeled-full-binary-trees.lagda.md +++ b/src/trees/labeled-full-binary-trees.lagda.md @@ -18,6 +18,7 @@ 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 @@ -186,6 +187,17 @@ module _ ( λ 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) ≃ @@ -194,17 +206,47 @@ module _ 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) = + 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 = + 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))) p = - eq-htpy {! !} + 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 : @@ -215,7 +257,7 @@ module _ is-contr-equiv' ( Σ (labeling-full-binary-tree X T) (_~_ f)) ( equiv-tot (equiv-htpy'-refl-labeled-full-binary-tree T f)) - ( fundamental-theorem-id' (λ g → htpy-eq) (funext 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) → @@ -236,4 +278,24 @@ module _ ( 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 ``` From da7999daf8f958cf3900824b24df1b23ad66d6c4 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Mon, 18 Aug 2025 20:53:03 -0600 Subject: [PATCH 63/63] notation in the free magmas on types file --- src/trees/free-magmas-on-types.lagda.md | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/trees/free-magmas-on-types.lagda.md b/src/trees/free-magmas-on-types.lagda.md index d9f2f0ba55..9fafb3352a 100644 --- a/src/trees/free-magmas-on-types.lagda.md +++ b/src/trees/free-magmas-on-types.lagda.md @@ -88,11 +88,12 @@ module _ 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)))) + 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) → @@ -170,7 +171,7 @@ module _ 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) + ( 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) @@ -180,9 +181,10 @@ module _ 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) + {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 ```