Bases of enriched directed trees
module trees.bases-enriched-directed-trees where
Imports
open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functions open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.negation open import foundation.type-arithmetic-empty-type open import foundation.universe-levels open import trees.bases-directed-trees open import trees.enriched-directed-trees
Idea
The base of an enriched directed tree consists of its nodes equipped with an edge to the root.
Definition
module _ {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) (T : Enriched-Directed-Tree l3 l4 A B) where base-Enriched-Directed-Tree : UU l2 base-Enriched-Directed-Tree = B (shape-root-Enriched-Directed-Tree A B T) compute-base-Enriched-Directed-Tree : base-Enriched-Directed-Tree ≃ direct-predecessor-Enriched-Directed-Tree A B T ( root-Enriched-Directed-Tree A B T) compute-base-Enriched-Directed-Tree = enrichment-Enriched-Directed-Tree A B T (root-Enriched-Directed-Tree A B T) map-compute-base-Enriched-Directed-Tree : base-Enriched-Directed-Tree → direct-predecessor-Enriched-Directed-Tree A B T ( root-Enriched-Directed-Tree A B T) map-compute-base-Enriched-Directed-Tree = map-enrichment-Enriched-Directed-Tree A B T ( root-Enriched-Directed-Tree A B T) module _ (b : base-Enriched-Directed-Tree) where node-base-Enriched-Directed-Tree : node-Enriched-Directed-Tree A B T node-base-Enriched-Directed-Tree = node-base-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( map-compute-base-Enriched-Directed-Tree b) edge-base-Enriched-Directed-Tree : edge-Enriched-Directed-Tree A B T ( node-base-Enriched-Directed-Tree) ( root-Enriched-Directed-Tree A B T) edge-base-Enriched-Directed-Tree = edge-base-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( map-compute-base-Enriched-Directed-Tree b)
Properties
The root is not a base element
module _ {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) (T : Enriched-Directed-Tree l3 l4 A B) where is-proper-node-base-Enriched-Directed-Tree : (b : base-Enriched-Directed-Tree A B T) → is-proper-node-Enriched-Directed-Tree A B T ( node-base-Enriched-Directed-Tree A B T b) is-proper-node-base-Enriched-Directed-Tree b = is-proper-node-base-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( map-compute-base-Enriched-Directed-Tree A B T b) no-walk-to-base-root-Enriched-Directed-Tree : (b : base-Enriched-Directed-Tree A B T) → ¬ ( walk-Enriched-Directed-Tree A B T ( root-Enriched-Directed-Tree A B T) ( node-base-Enriched-Directed-Tree A B T b)) no-walk-to-base-root-Enriched-Directed-Tree b = no-walk-to-base-root-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( map-compute-base-Enriched-Directed-Tree A B T b)
There are no edges between base elements
module _ {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) (T : Enriched-Directed-Tree l3 l4 A B) where no-edge-base-Enriched-Directed-Tree : (a b : base-Enriched-Directed-Tree A B T) → ¬ ( edge-Enriched-Directed-Tree A B T ( node-base-Enriched-Directed-Tree A B T a) ( node-base-Enriched-Directed-Tree A B T b)) no-edge-base-Enriched-Directed-Tree a b = no-edge-base-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( map-compute-base-Enriched-Directed-Tree A B T a) ( map-compute-base-Enriched-Directed-Tree A B T b)
For any node x, the coproduct of is-root x and the type of base elements b equipped with a walk from x to b is contractible
module _ {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) (T : Enriched-Directed-Tree l3 l4 A B) where unique-walk-to-base-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B T) → is-contr ( is-root-Enriched-Directed-Tree A B T x + Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T)) unique-walk-to-base-Enriched-Directed-Tree x = is-contr-equiv ( is-root-Enriched-Directed-Tree A B T x + Σ ( direct-predecessor-Enriched-Directed-Tree A B T ( root-Enriched-Directed-Tree A B T)) ( walk-Enriched-Directed-Tree A B T x ∘ pr1)) ( equiv-coprod ( id-equiv) ( equiv-Σ ( walk-Enriched-Directed-Tree A B T x ∘ pr1) ( compute-base-Enriched-Directed-Tree A B T) ( λ b → id-equiv))) ( unique-walk-to-base-Directed-Tree ( directed-tree-Enriched-Directed-Tree A B T) ( x)) is-root-or-walk-to-base-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B T) → is-root-Enriched-Directed-Tree A B T x + Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T) is-root-or-walk-to-base-Enriched-Directed-Tree x = center (unique-walk-to-base-Enriched-Directed-Tree x) is-root-is-root-or-walk-to-base-root-Enriched-Directed-Tree : is-root-or-walk-to-base-Enriched-Directed-Tree ( root-Enriched-Directed-Tree A B T) ＝ inl refl is-root-is-root-or-walk-to-base-root-Enriched-Directed-Tree = eq-is-contr ( unique-walk-to-base-Enriched-Directed-Tree ( root-Enriched-Directed-Tree A B T)) unique-walk-to-base-is-not-root-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B T) → ¬ (is-root-Enriched-Directed-Tree A B T x) → is-contr ( Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T)) unique-walk-to-base-is-not-root-Enriched-Directed-Tree x f = is-contr-equiv' ( is-root-Enriched-Directed-Tree A B T x + Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T)) ( left-unit-law-coprod-is-empty ( is-root-Enriched-Directed-Tree A B T x) ( Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T)) ( f)) ( unique-walk-to-base-Enriched-Directed-Tree x) unique-walk-to-base-direct-successor-Enriched-Directed-Tree : (x : node-Enriched-Directed-Tree A B T) (u : Σ ( node-Enriched-Directed-Tree A B T) ( edge-Enriched-Directed-Tree A B T x)) → is-contr ( Σ ( base-Enriched-Directed-Tree A B T) ( walk-Enriched-Directed-Tree A B T x ∘ node-base-Enriched-Directed-Tree A B T)) unique-walk-to-base-direct-successor-Enriched-Directed-Tree x (y , e) = unique-walk-to-base-is-not-root-Enriched-Directed-Tree x ( is-proper-node-direct-successor-Enriched-Directed-Tree A B T e)