agda-unimath/src/trees/coproduct-polynomial-endofunctors.lagda.md at 0369f0f9d3b3ff06257ac047ce1590579e4d36c6 · UniMath/agda-unimath · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
# Coproduct polynomial endofunctors

```agda
module trees.coproduct-polynomial-endofunctors where
```

<details><summary>Imports</summary>

```agda
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import trees.polynomial-endofunctors
```

</details>

## Idea

For every pair of [polynomial endofunctors](trees.polynomial-endofunctors.md)
`𝑃` and `𝑄` there is a
{{#concept "coproduct polynomial endofunctor" Disambiguation="on types" Agda=coproduct-polynomial-endofunctor}}
`𝑃 + 𝑄` given on shapes by `(𝑃 + 𝑄)₀ := 𝑃₀ + 𝑄₀` and on positions by
`(𝑃 + 𝑄)₁(inl a) := 𝑃₁(a)` and `(𝑃 + 𝑄)₁(inr c) := 𝑄₁(c)`. This polynomial
endofunctor satisfies the [equivalence](foundation-core.equivalences.md)

```text
  (𝑃 + 𝑄)(X) ≃ 𝑃(X) + 𝑄(X).
```

Note that for this definition to make sense, the positions of `𝑃` and `𝑄` have
to live in the same universe.

## Definition

```agda
module _
  {l1 l2 l3 : Level}
  (P@(A , B) : polynomial-endofunctor l1 l3)
  (Q@(C , D) : polynomial-endofunctor l2 l3)
  where

  shape-coproduct-polynomial-endofunctor : UU (l1 ⊔ l2)
  shape-coproduct-polynomial-endofunctor = A + C

  position-coproduct-polynomial-endofunctor :
    shape-coproduct-polynomial-endofunctor → UU l3
  position-coproduct-polynomial-endofunctor (inl a) = B a
  position-coproduct-polynomial-endofunctor (inr c) = D c

  coproduct-polynomial-endofunctor : polynomial-endofunctor (l1 ⊔ l2) l3
  coproduct-polynomial-endofunctor =
    ( shape-coproduct-polynomial-endofunctor ,
      position-coproduct-polynomial-endofunctor)

  map-compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    type-polynomial-endofunctor coproduct-polynomial-endofunctor X →
    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X
  map-compute-type-coproduct-polynomial-endofunctor (inl a , b) = inl (a , b)
  map-compute-type-coproduct-polynomial-endofunctor (inr c , d) = inr (c , d)

  map-inv-compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X →
    type-polynomial-endofunctor coproduct-polynomial-endofunctor X
  map-inv-compute-type-coproduct-polynomial-endofunctor (inl (a , b)) =
    (inl a , b)
  map-inv-compute-type-coproduct-polynomial-endofunctor (inr (c , d)) =
    (inr c , d)

  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    is-section
      ( map-compute-type-coproduct-polynomial-endofunctor {X = X})
      ( map-inv-compute-type-coproduct-polynomial-endofunctor {X = X})
  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor (inl x) =
    refl
  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor (inr y) =
    refl

  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    is-retraction
      ( map-compute-type-coproduct-polynomial-endofunctor {X = X})
      ( map-inv-compute-type-coproduct-polynomial-endofunctor {X = X})
  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor
    ( inl x , _) =
    refl
  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor
    ( inr y , _) =
    refl

  is-equiv-map-compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    is-equiv (map-compute-type-coproduct-polynomial-endofunctor {X = X})
  is-equiv-map-compute-type-coproduct-polynomial-endofunctor =
    is-equiv-is-invertible
      ( map-inv-compute-type-coproduct-polynomial-endofunctor)
      ( is-section-map-inv-compute-type-coproduct-polynomial-endofunctor)
      ( is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor)

  compute-type-coproduct-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    type-polynomial-endofunctor coproduct-polynomial-endofunctor X ≃
    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X
  compute-type-coproduct-polynomial-endofunctor =
    ( map-compute-type-coproduct-polynomial-endofunctor ,
      is-equiv-map-compute-type-coproduct-polynomial-endofunctor)
```