Equivalences of enriched directed trees
module trees.equivalences-enriched-directed-trees where
Imports
open import foundation.commuting-squares-of-maps open import foundation.commuting-triangles-of-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.function-extensionality open import foundation.functions open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle open import foundation.universe-levels open import trees.enriched-directed-trees open import trees.equivalences-directed-trees open import trees.morphisms-directed-trees open import trees.morphisms-enriched-directed-trees open import trees.rooted-morphisms-enriched-directed-trees
Idea
An equivalence of (A,B)-enriched directed trees from S to T is a
shape-preserving equivalence between their underlying trees, which also
preserves the enrichment equivalences.
Definition
The condition of being an equivalence of enriched directed trees
module _ {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) (S : Enriched-Directed-Tree l3 l4 A B) (T : Enriched-Directed-Tree l5 l6 A B) where is-equiv-hom-Enriched-Directed-Tree : hom-Enriched-Directed-Tree A B S T → UU (l3 ⊔ l4 ⊔ l5 ⊔ l6) is-equiv-hom-Enriched-Directed-Tree f = is-equiv-hom-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( directed-tree-hom-Enriched-Directed-Tree A B S T f) preserves-root-is-equiv-node-hom-Enriched-Directed-Tree : ( f : hom-Enriched-Directed-Tree A B S T) → is-equiv ( node-hom-Enriched-Directed-Tree A B S T f) → preserves-root-hom-Enriched-Directed-Tree A B S T f preserves-root-is-equiv-node-hom-Enriched-Directed-Tree f = preserves-root-is-equiv-node-hom-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( directed-tree-hom-Enriched-Directed-Tree A B S T f)
Equivalences of enriched directed trees
equiv-Enriched-Directed-Tree : {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) → Enriched-Directed-Tree l3 l4 A B → Enriched-Directed-Tree l5 l6 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) equiv-Enriched-Directed-Tree A B S T = Σ ( equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T)) ( λ e → Σ ( coherence-triangle-maps ( shape-Enriched-Directed-Tree A B S) ( shape-Enriched-Directed-Tree A B T) ( node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( e))) ( λ H → (x : node-Enriched-Directed-Tree A B S) → htpy-equiv ( ( equiv-direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( e) ( x)) ∘e ( enrichment-Enriched-Directed-Tree A B S x)) ( ( enrichment-Enriched-Directed-Tree A B T ( node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( e) ( x))) ∘e ( equiv-tr B (H x))))) equiv-is-equiv-hom-Enriched-Directed-Tree : {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) (S : Enriched-Directed-Tree l3 l4 A B) (T : Enriched-Directed-Tree l5 l6 A B) → (f : hom-Enriched-Directed-Tree A B S T) → is-equiv-hom-Enriched-Directed-Tree A B S T f → equiv-Enriched-Directed-Tree A B S T equiv-is-equiv-hom-Enriched-Directed-Tree A B S T f H = map-Σ-map-base ( equiv-is-equiv-hom-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( directed-tree-hom-Enriched-Directed-Tree A B S T f)) ( _) ( H , shape-hom-Enriched-Directed-Tree A B S T f , enrichment-hom-Enriched-Directed-Tree A B S T f) module _ {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) (S : Enriched-Directed-Tree l3 l4 A B) (T : Enriched-Directed-Tree l5 l6 A B) (e : equiv-Enriched-Directed-Tree A B S T) where equiv-directed-tree-equiv-Enriched-Directed-Tree : equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) equiv-directed-tree-equiv-Enriched-Directed-Tree = pr1 e equiv-node-equiv-Enriched-Directed-Tree : node-Enriched-Directed-Tree A B S ≃ node-Enriched-Directed-Tree A B T equiv-node-equiv-Enriched-Directed-Tree = equiv-node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) node-equiv-Enriched-Directed-Tree : node-Enriched-Directed-Tree A B S → node-Enriched-Directed-Tree A B T node-equiv-Enriched-Directed-Tree = node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) equiv-edge-equiv-Enriched-Directed-Tree : (x y : node-Enriched-Directed-Tree A B S) → edge-Enriched-Directed-Tree A B S x y ≃ edge-Enriched-Directed-Tree A B T ( node-equiv-Enriched-Directed-Tree x) ( node-equiv-Enriched-Directed-Tree y) equiv-edge-equiv-Enriched-Directed-Tree = equiv-edge-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) edge-equiv-Enriched-Directed-Tree : (x y : node-Enriched-Directed-Tree A B S) → edge-Enriched-Directed-Tree A B S x y → edge-Enriched-Directed-Tree A B T ( node-equiv-Enriched-Directed-Tree x) ( node-equiv-Enriched-Directed-Tree y) edge-equiv-Enriched-Directed-Tree = edge-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) hom-directed-tree-equiv-Enriched-Directed-Tree : hom-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) hom-directed-tree-equiv-Enriched-Directed-Tree = hom-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) equiv-direct-predecessor-equiv-Enriched-Directed-Tree : ( x : node-Enriched-Directed-Tree A B S) → Σ ( node-Enriched-Directed-Tree A B S) ( λ y → edge-Enriched-Directed-Tree A B S y x) ≃ Σ ( node-Enriched-Directed-Tree A B T) ( λ y → edge-Enriched-Directed-Tree A B T y ( node-equiv-Enriched-Directed-Tree x)) equiv-direct-predecessor-equiv-Enriched-Directed-Tree = equiv-direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) direct-predecessor-equiv-Enriched-Directed-Tree : ( x : node-Enriched-Directed-Tree A B S) → Σ ( node-Enriched-Directed-Tree A B S) ( λ y → edge-Enriched-Directed-Tree A B S y x) → Σ ( node-Enriched-Directed-Tree A B T) ( λ y → edge-Enriched-Directed-Tree A B T y ( node-equiv-Enriched-Directed-Tree x)) direct-predecessor-equiv-Enriched-Directed-Tree = direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) shape-equiv-Enriched-Directed-Tree : ( shape-Enriched-Directed-Tree A B S) ~ ( shape-Enriched-Directed-Tree A B T ∘ node-equiv-Enriched-Directed-Tree) shape-equiv-Enriched-Directed-Tree = pr1 (pr2 e) enrichment-equiv-Enriched-Directed-Tree : ( x : node-Enriched-Directed-Tree A B S) → ( ( direct-predecessor-equiv-Enriched-Directed-Tree x) ∘ ( map-enrichment-Enriched-Directed-Tree A B S x)) ~ ( ( map-enrichment-Enriched-Directed-Tree A B T ( node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) ( x))) ∘ ( tr B (shape-equiv-Enriched-Directed-Tree x))) enrichment-equiv-Enriched-Directed-Tree = pr2 (pr2 e) hom-equiv-Enriched-Directed-Tree : hom-Enriched-Directed-Tree A B S T pr1 hom-equiv-Enriched-Directed-Tree = hom-directed-tree-equiv-Enriched-Directed-Tree pr1 (pr2 hom-equiv-Enriched-Directed-Tree) = shape-equiv-Enriched-Directed-Tree pr2 (pr2 hom-equiv-Enriched-Directed-Tree) = enrichment-equiv-Enriched-Directed-Tree preserves-root-equiv-Enriched-Directed-Tree : preserves-root-hom-Enriched-Directed-Tree A B S T hom-equiv-Enriched-Directed-Tree preserves-root-equiv-Enriched-Directed-Tree = preserves-root-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree) rooted-hom-equiv-Enriched-Directed-Tree : rooted-hom-Enriched-Directed-Tree A B S T pr1 rooted-hom-equiv-Enriched-Directed-Tree = hom-equiv-Enriched-Directed-Tree pr2 rooted-hom-equiv-Enriched-Directed-Tree = preserves-root-equiv-Enriched-Directed-Tree
The identity equivalence of enriched directed trees
id-equiv-Enriched-Directed-Tree : {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) → (T : Enriched-Directed-Tree l3 l4 A B) → equiv-Enriched-Directed-Tree A B T T pr1 (id-equiv-Enriched-Directed-Tree A B T) = id-equiv-Directed-Tree (directed-tree-Enriched-Directed-Tree A B T) pr1 (pr2 (id-equiv-Enriched-Directed-Tree A B T)) = refl-htpy pr2 (pr2 (id-equiv-Enriched-Directed-Tree A B T)) x = refl-htpy
Composition of equivalences of enriched directed trees
module _ {l1 l2 l3 l4 l5 l6 l7 l8 : Level} (A : UU l1) (B : A → UU l2) (R : Enriched-Directed-Tree l3 l4 A B) (S : Enriched-Directed-Tree l5 l6 A B) (T : Enriched-Directed-Tree l7 l8 A B) (g : equiv-Enriched-Directed-Tree A B S T) (f : equiv-Enriched-Directed-Tree A B R S) where equiv-directed-tree-comp-equiv-Enriched-Directed-Tree : equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) equiv-directed-tree-comp-equiv-Enriched-Directed-Tree = comp-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-equiv-Enriched-Directed-Tree A B S T g) ( equiv-directed-tree-equiv-Enriched-Directed-Tree A B R S f) equiv-node-comp-equiv-Enriched-Directed-Tree : node-Enriched-Directed-Tree A B R ≃ node-Enriched-Directed-Tree A B T equiv-node-comp-equiv-Enriched-Directed-Tree = equiv-node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) node-comp-equiv-Enriched-Directed-Tree : node-Enriched-Directed-Tree A B R → node-Enriched-Directed-Tree A B T node-comp-equiv-Enriched-Directed-Tree = node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) equiv-edge-comp-equiv-Enriched-Directed-Tree : (x y : node-Enriched-Directed-Tree A B R) → edge-Enriched-Directed-Tree A B R x y ≃ edge-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x) ( node-comp-equiv-Enriched-Directed-Tree y) equiv-edge-comp-equiv-Enriched-Directed-Tree = equiv-edge-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) edge-comp-equiv-Enriched-Directed-Tree : (x y : node-Enriched-Directed-Tree A B R) → edge-Enriched-Directed-Tree A B R x y → edge-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x) ( node-comp-equiv-Enriched-Directed-Tree y) edge-comp-equiv-Enriched-Directed-Tree = edge-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) equiv-direct-predecessor-comp-equiv-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B R) → direct-predecessor-Enriched-Directed-Tree A B R x ≃ direct-predecessor-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x) equiv-direct-predecessor-comp-equiv-Enriched-Directed-Tree = equiv-direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) direct-predecessor-comp-equiv-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B R) → direct-predecessor-Enriched-Directed-Tree A B R x → direct-predecessor-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x) direct-predecessor-comp-equiv-Enriched-Directed-Tree = direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B R) ( directed-tree-Enriched-Directed-Tree A B T) ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree) shape-comp-equiv-Enriched-Directed-Tree : ( shape-Enriched-Directed-Tree A B R) ~ ( shape-Enriched-Directed-Tree A B T ∘ node-comp-equiv-Enriched-Directed-Tree) shape-comp-equiv-Enriched-Directed-Tree = concat-coherence-triangle-maps ( shape-Enriched-Directed-Tree A B R) ( shape-Enriched-Directed-Tree A B S) ( shape-Enriched-Directed-Tree A B T) ( node-equiv-Enriched-Directed-Tree A B R S f) ( node-equiv-Enriched-Directed-Tree A B S T g) ( shape-equiv-Enriched-Directed-Tree A B R S f) ( shape-equiv-Enriched-Directed-Tree A B S T g) enrichment-comp-equiv-Enriched-Directed-Tree : ( x : node-Enriched-Directed-Tree A B R) → coherence-square-maps ( tr B (shape-comp-equiv-Enriched-Directed-Tree x)) ( map-enrichment-Enriched-Directed-Tree A B R x) ( map-enrichment-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x)) ( direct-predecessor-comp-equiv-Enriched-Directed-Tree x) enrichment-comp-equiv-Enriched-Directed-Tree x = pasting-horizontal-up-to-htpy-coherence-square-maps ( tr B (shape-equiv-Enriched-Directed-Tree A B R S f x)) ( tr B ( shape-equiv-Enriched-Directed-Tree A B S T g ( node-equiv-Enriched-Directed-Tree A B R S f x))) ( map-enrichment-Enriched-Directed-Tree A B R x) ( map-enrichment-Enriched-Directed-Tree A B S ( node-equiv-Enriched-Directed-Tree A B R S f x)) ( map-enrichment-Enriched-Directed-Tree A B T ( node-comp-equiv-Enriched-Directed-Tree x)) ( direct-predecessor-equiv-Enriched-Directed-Tree A B R S f x) ( direct-predecessor-equiv-Enriched-Directed-Tree A B S T g ( node-equiv-Enriched-Directed-Tree A B R S f x)) ( tr-concat ( shape-equiv-Enriched-Directed-Tree A B R S f x) ( shape-equiv-Enriched-Directed-Tree A B S T g ( node-equiv-Enriched-Directed-Tree A B R S f x))) ( refl-htpy) ( enrichment-equiv-Enriched-Directed-Tree A B R S f x) ( enrichment-equiv-Enriched-Directed-Tree A B S T g ( node-equiv-Enriched-Directed-Tree A B R S f x)) comp-equiv-Enriched-Directed-Tree : equiv-Enriched-Directed-Tree A B R T pr1 comp-equiv-Enriched-Directed-Tree = equiv-directed-tree-comp-equiv-Enriched-Directed-Tree pr1 (pr2 comp-equiv-Enriched-Directed-Tree) = shape-comp-equiv-Enriched-Directed-Tree pr2 (pr2 comp-equiv-Enriched-Directed-Tree) = enrichment-comp-equiv-Enriched-Directed-Tree
Homotopies of equivalences of enriched directed trees
htpy-equiv-Enriched-Directed-Tree : {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) → (S : Enriched-Directed-Tree l3 l4 A B) (T : Enriched-Directed-Tree l5 l6 A B) (e f : equiv-Enriched-Directed-Tree A B S T) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) htpy-equiv-Enriched-Directed-Tree A B S T e f = htpy-hom-Enriched-Directed-Tree A B S T ( hom-equiv-Enriched-Directed-Tree A B S T e) ( hom-equiv-Enriched-Directed-Tree A B S T f)
Properties
Equivalences characterize identifications of enriched directed trees
module _ {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) (T : Enriched-Directed-Tree l3 l4 A B) where extensionality-Enriched-Directed-Tree : (S : Enriched-Directed-Tree l3 l4 A B) → (T ＝ S) ≃ equiv-Enriched-Directed-Tree A B T S extensionality-Enriched-Directed-Tree = extensionality-Σ ( λ {S} (sh , enr) e → Σ ( ( shape-Enriched-Directed-Tree A B T) ~ ( ( sh) ∘ ( node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( S) ( e)))) ( λ H → ( x : node-Enriched-Directed-Tree A B T) → ( ( direct-predecessor-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( S) ( e) ( x)) ∘ ( map-enrichment-Enriched-Directed-Tree A B T x)) ~ ( ( map-equiv ( enr ( node-equiv-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( S) ( e) ( x)))) ∘ ( tr B (H x))))) ( id-equiv-Directed-Tree (directed-tree-Enriched-Directed-Tree A B T)) ( ( refl-htpy) , ( λ x → refl-htpy)) ( extensionality-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T)) ( extensionality-Σ ( λ {sh} enr H → ( x : node-Enriched-Directed-Tree A B T) → ( map-enrichment-Enriched-Directed-Tree A B T x) ~ ( map-equiv (enr x) ∘ tr B (H x))) ( refl-htpy) ( λ x → refl-htpy) ( λ sh → equiv-funext) ( extensionality-Π ( enrichment-Enriched-Directed-Tree A B T) ( λ x e → ( map-enrichment-Enriched-Directed-Tree A B T x) ~ ( map-equiv e)) ( λ x → extensionality-equiv ( enrichment-Enriched-Directed-Tree A B T x)))) equiv-eq-Enriched-Directed-Tree : (S : Enriched-Directed-Tree l3 l4 A B) → (T ＝ S) → equiv-Enriched-Directed-Tree A B T S equiv-eq-Enriched-Directed-Tree S = map-equiv (extensionality-Enriched-Directed-Tree S) eq-equiv-Enriched-Directed-Tree : (S : Enriched-Directed-Tree l3 l4 A B) → equiv-Enriched-Directed-Tree A B T S → T ＝ S eq-equiv-Enriched-Directed-Tree S = map-inv-equiv (extensionality-Enriched-Directed-Tree S) is-contr-total-equiv-Enriched-Directed-Tree : is-contr ( Σ ( Enriched-Directed-Tree l3 l4 A B) ( equiv-Enriched-Directed-Tree A B T)) is-contr-total-equiv-Enriched-Directed-Tree = is-contr-equiv' ( Σ (Enriched-Directed-Tree l3 l4 A B) (λ S → T ＝ S)) ( equiv-tot extensionality-Enriched-Directed-Tree) ( is-contr-total-path T)
A morphism of enriched directed trees is an equivalence if it is an equivalence on the nodes
module _ {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) (S : Enriched-Directed-Tree l3 l4 A B) (T : Enriched-Directed-Tree l5 l6 A B) (f : hom-Enriched-Directed-Tree A B S T) where is-equiv-is-equiv-node-hom-Enriched-Directed-Tree : is-equiv (node-hom-Enriched-Directed-Tree A B S T f) → is-equiv-hom-Enriched-Directed-Tree A B S T f is-equiv-is-equiv-node-hom-Enriched-Directed-Tree = is-equiv-is-equiv-node-hom-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B S) ( directed-tree-Enriched-Directed-Tree A B T) ( directed-tree-hom-Enriched-Directed-Tree A B S T f)