The combinator of directed trees
module trees.combinator-directed-trees where
Imports
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.functions open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.isolated-points 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.morphisms-directed-trees
Idea
The combinator operation on directed trees combines a family of directed trees into a single directed tree with a new root.
Definitions
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) where data node-combinator-Directed-Tree : UU (l1 ⊔ l2) where root-combinator-Directed-Tree : node-combinator-Directed-Tree node-inclusion-combinator-Directed-Tree : (i : I) → node-Directed-Tree (T i) → node-combinator-Directed-Tree data edge-combinator-Directed-Tree : ( x y : node-combinator-Directed-Tree) → UU (l1 ⊔ l2 ⊔ l3) where edge-to-root-combinator-Directed-Tree : (i : I) → edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i (root-Directed-Tree (T i))) ( root-combinator-Directed-Tree) edge-inclusion-combinator-Directed-Tree : (i : I) (x y : node-Directed-Tree (T i)) → edge-Directed-Tree (T i) x y → edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) ( node-inclusion-combinator-Directed-Tree i y) graph-combinator-Directed-Tree : Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2 ⊔ l3) pr1 graph-combinator-Directed-Tree = node-combinator-Directed-Tree pr2 graph-combinator-Directed-Tree = edge-combinator-Directed-Tree inclusion-combinator-Directed-Tree : (i : I) → hom-Directed-Graph ( graph-Directed-Tree (T i)) ( graph-combinator-Directed-Tree) pr1 (inclusion-combinator-Directed-Tree i) = node-inclusion-combinator-Directed-Tree i pr2 (inclusion-combinator-Directed-Tree i) = edge-inclusion-combinator-Directed-Tree i walk-combinator-Directed-Tree : ( x y : node-combinator-Directed-Tree) → UU (l1 ⊔ l2 ⊔ l3) walk-combinator-Directed-Tree = walk-Directed-Graph graph-combinator-Directed-Tree walk-inclusion-combinator-Directed-Tree : (i : I) (x y : node-Directed-Tree (T i)) → walk-Directed-Graph (graph-Directed-Tree (T i)) x y → walk-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) ( node-inclusion-combinator-Directed-Tree i y) walk-inclusion-combinator-Directed-Tree a x y = walk-hom-Directed-Graph ( graph-Directed-Tree (T a)) ( graph-combinator-Directed-Tree) ( inclusion-combinator-Directed-Tree a) walk-to-root-combinator-Directed-Tree : ( x : node-combinator-Directed-Tree) → walk-combinator-Directed-Tree x root-combinator-Directed-Tree walk-to-root-combinator-Directed-Tree root-combinator-Directed-Tree = refl-walk-Directed-Graph walk-to-root-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) = snoc-walk-Directed-Graph ( graph-combinator-Directed-Tree) ( walk-inclusion-combinator-Directed-Tree i x ( root-Directed-Tree (T i)) ( walk-to-root-Directed-Tree (T i) x)) ( edge-to-root-combinator-Directed-Tree i) is-root-combinator-Directed-Tree : node-combinator-Directed-Tree → UU (l1 ⊔ l2) is-root-combinator-Directed-Tree x = root-combinator-Directed-Tree ＝ x is-isolated-root-combinator-Directed-Tree : is-isolated root-combinator-Directed-Tree is-isolated-root-combinator-Directed-Tree root-combinator-Directed-Tree = inl refl is-isolated-root-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) = inr (λ ()) cases-center-unique-direct-successor-combinator-Directed-Tree' : (i : I) (x : node-Directed-Tree (T i)) → is-decidable (is-root-Directed-Tree (T i) x) → Σ ( node-combinator-Directed-Tree) ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x)) cases-center-unique-direct-successor-combinator-Directed-Tree' a ._ ( inl refl) = ( root-combinator-Directed-Tree , edge-to-root-combinator-Directed-Tree a) cases-center-unique-direct-successor-combinator-Directed-Tree' i x (inr f) = map-Σ ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x)) ( node-inclusion-combinator-Directed-Tree i) ( edge-inclusion-combinator-Directed-Tree i x) ( direct-successor-is-proper-node-Directed-Tree (T i) x f) center-unique-direct-successor-combinator-Directed-Tree' : ( x : node-combinator-Directed-Tree) → ¬ (is-root-combinator-Directed-Tree x) → Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x) center-unique-direct-successor-combinator-Directed-Tree' root-combinator-Directed-Tree f = ex-falso (f refl) center-unique-direct-successor-combinator-Directed-Tree' ( node-inclusion-combinator-Directed-Tree i x) f = cases-center-unique-direct-successor-combinator-Directed-Tree' i x ( is-isolated-root-Directed-Tree (T i) x) cases-center-unique-direct-successor-combinator-Directed-Tree : (i : I) (x : node-Directed-Tree (T i)) → is-decidable (is-root-Directed-Tree (T i) x) → Σ ( node-combinator-Directed-Tree) ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x)) cases-center-unique-direct-successor-combinator-Directed-Tree i ._ ( inl refl) = root-combinator-Directed-Tree , edge-to-root-combinator-Directed-Tree i cases-center-unique-direct-successor-combinator-Directed-Tree i x (inr f) = map-Σ ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x)) ( node-inclusion-combinator-Directed-Tree i) ( edge-inclusion-combinator-Directed-Tree i x) ( direct-successor-is-proper-node-Directed-Tree (T i) x f) center-unique-direct-successor-combinator-Directed-Tree : (x : node-combinator-Directed-Tree) → is-root-combinator-Directed-Tree x + Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x) center-unique-direct-successor-combinator-Directed-Tree root-combinator-Directed-Tree = inl refl center-unique-direct-successor-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) = inr ( cases-center-unique-direct-successor-combinator-Directed-Tree i x ( is-isolated-root-Directed-Tree (T i) x)) cases-contraction-unique-direct-successor-combinator-Directed-Tree : (i : I) (x : node-Directed-Tree (T i)) → (d : is-decidable (is-root-Directed-Tree (T i) x)) → ( p : Σ ( node-combinator-Directed-Tree) ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x))) → cases-center-unique-direct-successor-combinator-Directed-Tree i x d ＝ p cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._ ( inl r) ( ._ , edge-to-root-combinator-Directed-Tree .i) = ap ( λ u → cases-center-unique-direct-successor-combinator-Directed-Tree i ( root-Directed-Tree (T i)) ( inl u)) ( eq-refl-root-Directed-Tree (T i) r) cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._ ( inr f) ( ._ , edge-to-root-combinator-Directed-Tree .i) = ex-falso (f refl) cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._ ( inl refl) ( ._ , edge-inclusion-combinator-Directed-Tree .i ._ y e) = ex-falso (no-direct-successor-root-Directed-Tree (T i) (y , e)) cases-contraction-unique-direct-successor-combinator-Directed-Tree i x ( inr f) ( ._ , edge-inclusion-combinator-Directed-Tree .i .x y e) = ap ( map-Σ ( edge-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x)) ( node-inclusion-combinator-Directed-Tree i) ( edge-inclusion-combinator-Directed-Tree i x)) ( eq-is-contr ( unique-direct-successor-is-proper-node-Directed-Tree (T i) x f)) contraction-unique-direct-successor-combinator-Directed-Tree : (x : node-combinator-Directed-Tree) → (p : is-root-combinator-Directed-Tree x + Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x)) → center-unique-direct-successor-combinator-Directed-Tree x ＝ p contraction-unique-direct-successor-combinator-Directed-Tree ._ (inl refl) = refl contraction-unique-direct-successor-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) ( inr (y , e)) = ap ( inr) ( cases-contraction-unique-direct-successor-combinator-Directed-Tree i x ( is-isolated-root-Directed-Tree (T i) x) ( y , e)) unique-direct-successor-combinator-Directed-Tree : unique-direct-successor-Directed-Graph ( graph-combinator-Directed-Tree) ( root-combinator-Directed-Tree) pr1 (unique-direct-successor-combinator-Directed-Tree x) = center-unique-direct-successor-combinator-Directed-Tree x pr2 (unique-direct-successor-combinator-Directed-Tree x) = contraction-unique-direct-successor-combinator-Directed-Tree x is-tree-combinator-Directed-Tree : is-tree-Directed-Graph graph-combinator-Directed-Tree is-tree-combinator-Directed-Tree = is-tree-unique-direct-successor-Directed-Graph graph-combinator-Directed-Tree root-combinator-Directed-Tree unique-direct-successor-combinator-Directed-Tree walk-to-root-combinator-Directed-Tree combinator-Directed-Tree : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2 ⊔ l3) pr1 combinator-Directed-Tree = graph-combinator-Directed-Tree pr2 combinator-Directed-Tree = is-tree-combinator-Directed-Tree base-combinator-Directed-Tree : UU (l1 ⊔ l2 ⊔ l3) base-combinator-Directed-Tree = base-Directed-Tree combinator-Directed-Tree is-proper-node-combinator-Directed-Tree : node-combinator-Directed-Tree → UU (l1 ⊔ l2) is-proper-node-combinator-Directed-Tree = is-proper-node-Directed-Tree combinator-Directed-Tree proper-node-combinator-Directed-Tree : UU (l1 ⊔ l2) proper-node-combinator-Directed-Tree = proper-node-Directed-Tree combinator-Directed-Tree is-proper-node-inclusion-combinator-Directed-Tree : {i : I} {x : node-Directed-Tree (T i)} → is-proper-node-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) is-proper-node-inclusion-combinator-Directed-Tree {i} {x} ()
Properties
The type of direct predecessors of x : T i is equivalent to the type of direct predecessors of the inclusion of x in combinator T
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) (i : I) (x : node-Directed-Tree (T i)) where direct-predecessor-combinator-Directed-Tree : UU (l1 ⊔ l2 ⊔ l3) direct-predecessor-combinator-Directed-Tree = Σ ( node-combinator-Directed-Tree T) ( λ y → edge-combinator-Directed-Tree T y ( node-inclusion-combinator-Directed-Tree i x)) map-compute-direct-predecessor-combinator-Directed-Tree : direct-predecessor-Directed-Tree (T i) x → direct-predecessor-combinator-Directed-Tree pr1 (map-compute-direct-predecessor-combinator-Directed-Tree (y , e)) = node-inclusion-combinator-Directed-Tree i y pr2 (map-compute-direct-predecessor-combinator-Directed-Tree (y , e)) = edge-inclusion-combinator-Directed-Tree i y x e map-inv-compute-direct-predecessor-combinator-Directed-Tree : direct-predecessor-combinator-Directed-Tree → direct-predecessor-Directed-Tree (T i) x map-inv-compute-direct-predecessor-combinator-Directed-Tree ( ._ , edge-inclusion-combinator-Directed-Tree .i y .x e) = ( y , e) issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree : ( map-compute-direct-predecessor-combinator-Directed-Tree ∘ map-inv-compute-direct-predecessor-combinator-Directed-Tree) ~ id issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree ( ._ , edge-inclusion-combinator-Directed-Tree .i y .x e) = refl isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree : ( map-inv-compute-direct-predecessor-combinator-Directed-Tree ∘ map-compute-direct-predecessor-combinator-Directed-Tree) ~ id isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree (y , e) = refl is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree : is-equiv map-compute-direct-predecessor-combinator-Directed-Tree is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree = is-equiv-has-inverse map-inv-compute-direct-predecessor-combinator-Directed-Tree issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree compute-direct-predecessor-combinator-Directed-Tree : direct-predecessor-Directed-Tree (T i) x ≃ direct-predecessor-combinator-Directed-Tree pr1 compute-direct-predecessor-combinator-Directed-Tree = map-compute-direct-predecessor-combinator-Directed-Tree pr2 compute-direct-predecessor-combinator-Directed-Tree = is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree
If e is an edge from node-inclusion i x to node-inclusion j y, then i ＝ j
eq-index-edge-combinator-Directed-Tree : {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) {i : I} (x : node-Directed-Tree (T i)) {j : I} (y : node-Directed-Tree (T j)) → edge-combinator-Directed-Tree T ( node-inclusion-combinator-Directed-Tree i x) ( node-inclusion-combinator-Directed-Tree j y) → i ＝ j eq-index-edge-combinator-Directed-Tree T x y ( edge-inclusion-combinator-Directed-Tree _ .x .y e) = refl
The base of the combinator tree of a family T of directed tree indexed by I is equivalent to I
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) where node-base-index-combinator-Directed-Tree : I → node-combinator-Directed-Tree T node-base-index-combinator-Directed-Tree i = node-inclusion-combinator-Directed-Tree i (root-Directed-Tree (T i)) edge-base-index-combinator-Directed-Tree : (i : I) → edge-combinator-Directed-Tree T ( node-base-index-combinator-Directed-Tree i) ( root-combinator-Directed-Tree) edge-base-index-combinator-Directed-Tree i = edge-to-root-combinator-Directed-Tree i base-index-combinator-Directed-Tree : I → base-combinator-Directed-Tree T pr1 (base-index-combinator-Directed-Tree i) = node-base-index-combinator-Directed-Tree i pr2 (base-index-combinator-Directed-Tree i) = edge-base-index-combinator-Directed-Tree i index-base-combinator-Directed-Tree : base-combinator-Directed-Tree T → I index-base-combinator-Directed-Tree ( ._ , edge-to-root-combinator-Directed-Tree i) = i issec-index-base-combinator-Directed-Tree : ( base-index-combinator-Directed-Tree ∘ index-base-combinator-Directed-Tree) ~ id issec-index-base-combinator-Directed-Tree ( ._ , edge-to-root-combinator-Directed-Tree i) = refl isretr-index-base-combinator-Directed-Tree : ( index-base-combinator-Directed-Tree ∘ base-index-combinator-Directed-Tree) ~ id isretr-index-base-combinator-Directed-Tree i = refl is-equiv-base-index-combinator-Directed-Tree : is-equiv base-index-combinator-Directed-Tree is-equiv-base-index-combinator-Directed-Tree = is-equiv-has-inverse index-base-combinator-Directed-Tree issec-index-base-combinator-Directed-Tree isretr-index-base-combinator-Directed-Tree equiv-base-index-combinator-Directed-Tree : I ≃ base-combinator-Directed-Tree T pr1 equiv-base-index-combinator-Directed-Tree = base-index-combinator-Directed-Tree pr2 equiv-base-index-combinator-Directed-Tree = is-equiv-base-index-combinator-Directed-Tree
The type of nodes of the combinator tree of T is equivalent to the dependent sum of the types of nodes of each T i, plus a root
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) where map-compute-node-combinator-Directed-Tree : Maybe (Σ I (node-Directed-Tree ∘ T)) → node-combinator-Directed-Tree T map-compute-node-combinator-Directed-Tree (inl (i , x)) = node-inclusion-combinator-Directed-Tree i x map-compute-node-combinator-Directed-Tree (inr star) = root-combinator-Directed-Tree map-inv-compute-node-combinator-Directed-Tree : node-combinator-Directed-Tree T → Maybe (Σ I (node-Directed-Tree ∘ T)) map-inv-compute-node-combinator-Directed-Tree root-combinator-Directed-Tree = exception-Maybe map-inv-compute-node-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) = unit-Maybe (i , x) issec-map-inv-compute-node-combinator-Directed-Tree : ( map-compute-node-combinator-Directed-Tree ∘ map-inv-compute-node-combinator-Directed-Tree) ~ id issec-map-inv-compute-node-combinator-Directed-Tree root-combinator-Directed-Tree = refl issec-map-inv-compute-node-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x) = refl isretr-map-inv-compute-node-combinator-Directed-Tree : ( map-inv-compute-node-combinator-Directed-Tree ∘ map-compute-node-combinator-Directed-Tree) ~ id isretr-map-inv-compute-node-combinator-Directed-Tree (inl (i , x)) = refl isretr-map-inv-compute-node-combinator-Directed-Tree (inr star) = refl is-equiv-map-compute-node-combinator-Directed-Tree : is-equiv map-compute-node-combinator-Directed-Tree is-equiv-map-compute-node-combinator-Directed-Tree = is-equiv-has-inverse map-inv-compute-node-combinator-Directed-Tree issec-map-inv-compute-node-combinator-Directed-Tree isretr-map-inv-compute-node-combinator-Directed-Tree compute-node-combinator-Directed-Tree : Maybe (Σ I (node-Directed-Tree ∘ T)) ≃ node-combinator-Directed-Tree T pr1 compute-node-combinator-Directed-Tree = map-compute-node-combinator-Directed-Tree pr2 compute-node-combinator-Directed-Tree = is-equiv-map-compute-node-combinator-Directed-Tree
The type of proper nodes of the combinator tree of T is equivalent to the dependent sum of the types of nodes of each T i
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) where map-compute-proper-node-combinator-Directed-Tree : Σ I (node-Directed-Tree ∘ T) → proper-node-combinator-Directed-Tree T map-compute-proper-node-combinator-Directed-Tree (i , x) = ( node-inclusion-combinator-Directed-Tree i x , is-proper-node-inclusion-combinator-Directed-Tree T) map-inv-compute-proper-node-combinator-Directed-Tree : proper-node-combinator-Directed-Tree T → Σ I (node-Directed-Tree ∘ T) map-inv-compute-proper-node-combinator-Directed-Tree ( root-combinator-Directed-Tree , H) = ex-falso (H refl) map-inv-compute-proper-node-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x , H) = (i , x) issec-map-inv-compute-proper-node-combinator-Directed-Tree : ( map-compute-proper-node-combinator-Directed-Tree ∘ map-inv-compute-proper-node-combinator-Directed-Tree) ~ id issec-map-inv-compute-proper-node-combinator-Directed-Tree ( root-combinator-Directed-Tree , H) = ex-falso (H refl) issec-map-inv-compute-proper-node-combinator-Directed-Tree ( node-inclusion-combinator-Directed-Tree i x , H) = eq-pair-Σ ( refl) ( eq-is-prop ( is-prop-is-proper-node-Directed-Tree ( combinator-Directed-Tree T) ( node-inclusion-combinator-Directed-Tree i x))) isretr-map-inv-compute-proper-node-combinator-Directed-Tree : ( map-inv-compute-proper-node-combinator-Directed-Tree ∘ map-compute-proper-node-combinator-Directed-Tree) ~ id isretr-map-inv-compute-proper-node-combinator-Directed-Tree (i , x) = refl is-equiv-map-compute-proper-node-combinator-Directed-Tree : is-equiv map-compute-proper-node-combinator-Directed-Tree is-equiv-map-compute-proper-node-combinator-Directed-Tree = is-equiv-has-inverse map-inv-compute-proper-node-combinator-Directed-Tree issec-map-inv-compute-proper-node-combinator-Directed-Tree isretr-map-inv-compute-proper-node-combinator-Directed-Tree compute-proper-node-combinator-Directed-Tree : Σ I (node-Directed-Tree ∘ T) ≃ proper-node-combinator-Directed-Tree T pr1 compute-proper-node-combinator-Directed-Tree = map-compute-proper-node-combinator-Directed-Tree pr2 compute-proper-node-combinator-Directed-Tree = is-equiv-map-compute-proper-node-combinator-Directed-Tree
The fibers at a base element b of the comibinator of a family T of trees is equivalent to T (index-base b)
module _ {l1 l2 l3 : Level} {I : UU l1} (T : I → Directed-Tree l2 l3) where node-fiber-combinator-Directed-Tree : (i : I) → node-Directed-Tree (T i) → node-fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i) pr1 (node-fiber-combinator-Directed-Tree i x) = node-inclusion-combinator-Directed-Tree i x pr2 (node-fiber-combinator-Directed-Tree i x) = walk-inclusion-combinator-Directed-Tree T i x ( root-Directed-Tree (T i)) ( walk-to-root-Directed-Tree (T i) x) compute-map-Σ-node-fiber-combinator-Directed-Tree : ( map-Σ ( λ b → Σ ( node-combinator-Directed-Tree T) ( λ x → walk-combinator-Directed-Tree T x ( node-base-Directed-Tree (combinator-Directed-Tree T) b))) ( base-index-combinator-Directed-Tree T) ( node-fiber-combinator-Directed-Tree)) ~ map-equiv ( ( compute-proper-node-Directed-Tree (combinator-Directed-Tree T)) ∘e ( compute-proper-node-combinator-Directed-Tree T)) compute-map-Σ-node-fiber-combinator-Directed-Tree (i , x) = inv ( eq-compute-proper-node-Directed-Tree ( combinator-Directed-Tree T) ( is-proper-node-inclusion-combinator-Directed-Tree T) ( base-index-combinator-Directed-Tree T i) ( walk-inclusion-combinator-Directed-Tree T i x ( root-Directed-Tree (T i)) ( walk-to-root-Directed-Tree (T i) x))) is-equiv-map-Σ-node-fiber-combinator-Directed-Tree : is-equiv ( map-Σ ( λ b → Σ ( node-combinator-Directed-Tree T) ( λ x → walk-combinator-Directed-Tree T x ( node-base-Directed-Tree (combinator-Directed-Tree T) b))) ( base-index-combinator-Directed-Tree T) ( node-fiber-combinator-Directed-Tree)) is-equiv-map-Σ-node-fiber-combinator-Directed-Tree = is-equiv-htpy ( map-equiv ( ( compute-proper-node-Directed-Tree (combinator-Directed-Tree T)) ∘e ( compute-proper-node-combinator-Directed-Tree T))) ( compute-map-Σ-node-fiber-combinator-Directed-Tree) ( is-equiv-map-equiv ( ( compute-proper-node-Directed-Tree (combinator-Directed-Tree T)) ∘e ( compute-proper-node-combinator-Directed-Tree T))) is-equiv-node-fiber-combinator-Directed-Tree : (i : I) → is-equiv (node-fiber-combinator-Directed-Tree i) is-equiv-node-fiber-combinator-Directed-Tree = is-fiberwise-equiv-is-equiv-map-Σ ( λ b → Σ ( node-combinator-Directed-Tree T) ( λ x → walk-combinator-Directed-Tree T x ( node-base-Directed-Tree (combinator-Directed-Tree T) b))) ( base-index-combinator-Directed-Tree T) ( node-fiber-combinator-Directed-Tree) ( is-equiv-base-index-combinator-Directed-Tree T) ( is-equiv-map-Σ-node-fiber-combinator-Directed-Tree) edge-fiber-combinator-Directed-Tree : (i : I) (x y : node-Directed-Tree (T i)) → edge-Directed-Tree (T i) x y → edge-fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i) ( node-fiber-combinator-Directed-Tree i x) ( node-fiber-combinator-Directed-Tree i y) pr1 (edge-fiber-combinator-Directed-Tree i x y e) = edge-inclusion-combinator-Directed-Tree i x y e pr2 (edge-fiber-combinator-Directed-Tree i x y e) = ap ( walk-inclusion-combinator-Directed-Tree T i x ( root-Directed-Tree (T i))) ( eq-is-contr (unique-walk-to-root-Directed-Tree (T i) x)) hom-fiber-combinator-Directed-Tree : (i : I) → hom-Directed-Tree ( T i) ( fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i)) pr1 (hom-fiber-combinator-Directed-Tree i) = node-fiber-combinator-Directed-Tree i pr2 (hom-fiber-combinator-Directed-Tree i) = edge-fiber-combinator-Directed-Tree i is-equiv-hom-fiber-combinator-Directed-Tree : (i : I) → is-equiv-hom-Directed-Tree ( T i) ( fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i)) ( hom-fiber-combinator-Directed-Tree i) is-equiv-hom-fiber-combinator-Directed-Tree i = is-equiv-is-equiv-node-hom-Directed-Tree ( T i) ( fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i)) ( hom-fiber-combinator-Directed-Tree i) ( is-equiv-node-fiber-combinator-Directed-Tree i) fiber-combinator-Directed-Tree : (i : I) → equiv-Directed-Tree ( T i) ( fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i)) fiber-combinator-Directed-Tree i = equiv-is-equiv-hom-Directed-Tree ( T i) ( fiber-Directed-Tree ( combinator-Directed-Tree T) ( node-base-index-combinator-Directed-Tree T i)) ( hom-fiber-combinator-Directed-Tree i) ( is-equiv-hom-fiber-combinator-Directed-Tree i)
Any tree is the combinator tree of the fibers at the nodes equipped with edges to the root
module _ {l1 l2 : Level} (T : Directed-Tree l1 l2) where node-combinator-fiber-base-Directed-Tree : node-combinator-Directed-Tree (fiber-base-Directed-Tree T) → node-Directed-Tree T node-combinator-fiber-base-Directed-Tree root-combinator-Directed-Tree = root-Directed-Tree T node-combinator-fiber-base-Directed-Tree ( node-inclusion-combinator-Directed-Tree b (x , w)) = x cases-map-inv-node-combinator-fiber-base-Directed-Tree : (x : node-Directed-Tree T) → is-root-Directed-Tree T x + Σ ( base-Directed-Tree T) ( walk-Directed-Tree T x ∘ node-base-Directed-Tree T) → node-combinator-Directed-Tree (fiber-base-Directed-Tree T) cases-map-inv-node-combinator-fiber-base-Directed-Tree ._ (inl refl) = root-combinator-Directed-Tree cases-map-inv-node-combinator-fiber-base-Directed-Tree x (inr (b , w)) = node-inclusion-combinator-Directed-Tree b (x , w) map-inv-node-combinator-fiber-base-Directed-Tree : node-Directed-Tree T → node-combinator-Directed-Tree (fiber-base-Directed-Tree T) map-inv-node-combinator-fiber-base-Directed-Tree x = cases-map-inv-node-combinator-fiber-base-Directed-Tree x ( is-root-or-walk-to-base-Directed-Tree T x) cases-issec-map-inv-node-combinator-fiber-base-Directed-Tree : (x : node-Directed-Tree T) → (H : is-root-Directed-Tree T x + Σ ( base-Directed-Tree T) ( walk-Directed-Tree T x ∘ node-base-Directed-Tree T)) → node-combinator-fiber-base-Directed-Tree ( cases-map-inv-node-combinator-fiber-base-Directed-Tree x H) ＝ x cases-issec-map-inv-node-combinator-fiber-base-Directed-Tree ._ (inl refl) = refl cases-issec-map-inv-node-combinator-fiber-base-Directed-Tree x (inr (b , w)) = refl issec-map-inv-node-combinator-fiber-base-Directed-Tree : ( node-combinator-fiber-base-Directed-Tree ∘ map-inv-node-combinator-fiber-base-Directed-Tree) ~ id issec-map-inv-node-combinator-fiber-base-Directed-Tree x = cases-issec-map-inv-node-combinator-fiber-base-Directed-Tree x ( is-root-or-walk-to-base-Directed-Tree T x) isretr-map-inv-node-combinator-fiber-base-Directed-Tree : ( map-inv-node-combinator-fiber-base-Directed-Tree ∘ node-combinator-fiber-base-Directed-Tree) ~ id isretr-map-inv-node-combinator-fiber-base-Directed-Tree root-combinator-Directed-Tree = ap ( cases-map-inv-node-combinator-fiber-base-Directed-Tree ( root-Directed-Tree T)) ( eq-is-contr ( unique-walk-to-base-Directed-Tree T (root-Directed-Tree T))) isretr-map-inv-node-combinator-fiber-base-Directed-Tree ( node-inclusion-combinator-Directed-Tree b (x , w)) = ap ( cases-map-inv-node-combinator-fiber-base-Directed-Tree x) ( eq-is-contr ( unique-walk-to-base-Directed-Tree T x)) is-equiv-node-combinator-fiber-base-Directed-Tree : is-equiv node-combinator-fiber-base-Directed-Tree is-equiv-node-combinator-fiber-base-Directed-Tree = is-equiv-has-inverse map-inv-node-combinator-fiber-base-Directed-Tree issec-map-inv-node-combinator-fiber-base-Directed-Tree isretr-map-inv-node-combinator-fiber-base-Directed-Tree equiv-node-combinator-fiber-base-Directed-Tree : node-combinator-Directed-Tree (fiber-base-Directed-Tree T) ≃ node-Directed-Tree T pr1 equiv-node-combinator-fiber-base-Directed-Tree = node-combinator-fiber-base-Directed-Tree pr2 equiv-node-combinator-fiber-base-Directed-Tree = is-equiv-node-combinator-fiber-base-Directed-Tree edge-combinator-fiber-base-Directed-Tree : (x y : node-combinator-Directed-Tree (fiber-base-Directed-Tree T)) → edge-combinator-Directed-Tree (fiber-base-Directed-Tree T) x y → edge-Directed-Tree T ( node-combinator-fiber-base-Directed-Tree x) ( node-combinator-fiber-base-Directed-Tree y) edge-combinator-fiber-base-Directed-Tree ._ ._ ( edge-to-root-combinator-Directed-Tree (b , e)) = e edge-combinator-fiber-base-Directed-Tree ._ ._ ( edge-inclusion-combinator-Directed-Tree i (u , ._) y (e , refl)) = e hom-combinator-fiber-base-Directed-Tree : hom-Directed-Tree ( combinator-Directed-Tree (fiber-base-Directed-Tree T)) ( T) pr1 hom-combinator-fiber-base-Directed-Tree = node-combinator-fiber-base-Directed-Tree pr2 hom-combinator-fiber-base-Directed-Tree = edge-combinator-fiber-base-Directed-Tree is-equiv-combinator-fiber-base-Directed-Tree : is-equiv-hom-Directed-Tree ( combinator-Directed-Tree (fiber-base-Directed-Tree T)) ( T) ( hom-combinator-fiber-base-Directed-Tree) is-equiv-combinator-fiber-base-Directed-Tree = is-equiv-is-equiv-node-hom-Directed-Tree ( combinator-Directed-Tree (fiber-base-Directed-Tree T)) ( T) ( hom-combinator-fiber-base-Directed-Tree) ( is-equiv-node-combinator-fiber-base-Directed-Tree) combinator-fiber-base-Directed-Tree : equiv-Directed-Tree ( combinator-Directed-Tree (fiber-base-Directed-Tree T)) ( T) combinator-fiber-base-Directed-Tree = equiv-is-equiv-hom-Directed-Tree ( combinator-Directed-Tree (fiber-base-Directed-Tree T)) ( T) ( hom-combinator-fiber-base-Directed-Tree) ( is-equiv-combinator-fiber-base-Directed-Tree)