Skip to content

Commit 6598e02

Browse files
malarbolmalarbol
authored
Inserting and removing elements in finite sequences (#1929)
This PR introduces the following maps for finite sequences: - `(x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↦ xᵢ`; - `(x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↦ (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ)`; - `xᵢ ↦ (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ) ↦ (x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ)`; and the corresponding equivalences `Aⁿ⁺¹ ≃ A × Aⁿ`: - `(x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↔ (xᵢ , (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ))`. We apply these to the case of **finite sequences of types** `A : Fin n → UU l` and define ```text Πₙ A = (i : Fin n) → A i ≃ A₀ × A₁ × ... × Aᵢ × ... Aₙ₋₁ ``` to prove that ```text Πₙ₊₁ A ≃ Aᵢ × Πₙ Aⁱ ``` where `Aⁱ` denotes the finite sequence of types obtained by removing the `i`th component of `A` so ```text Πₙ Aⁱ = A₀ × ... Aᵢ₋₁ × Aᵢ₊ᵢ × ... × Aₙ. ```
1 parent 68cfbac commit 6598e02

7 files changed

Lines changed: 656 additions & 1 deletion

‎src/lists.lagda.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,14 @@ open import lists.dependent-sequences public
1212
open import lists.equivalence-relations-tuples public
1313
open import lists.equivalence-tuples-finite-sequences public
1414
open import lists.finite-sequences public
15+
open import lists.finite-sequences-of-types public
1516
open import lists.flattening-lists public
17+
open import lists.focus-at-index-finite-sequences public
1618
open import lists.functoriality-finite-sequences public
1719
open import lists.functoriality-lists public
1820
open import lists.functoriality-tuples public
1921
open import lists.functoriality-tuples-finite-sequences public
22+
open import lists.insert-at-index-finite-sequences public
2023
open import lists.lists public
2124
open import lists.lists-discrete-types public
2225
open import lists.pairs-of-successive-elements-finite-sequences public
@@ -25,6 +28,7 @@ open import lists.permutation-lists public
2528
open import lists.permutation-tuples public
2629
open import lists.predicates-on-lists public
2730
open import lists.quicksort-lists public
31+
open import lists.remove-at-index-finite-sequences public
2832
open import lists.repetitions-sequences public
2933
open import lists.reversing-lists public
3034
open import lists.sequences public

‎src/lists/finite-sequences-of-types.lagda.md‎

Lines changed: 286 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,286 @@
1+
# Finite sequences of types
2+
3+
```agda
4+
module lists.finite-sequences-of-types where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import elementary-number-theory.natural-numbers
11+
12+
open import foundation.action-on-identifications-functions
13+
open import foundation.cartesian-product-types
14+
open import foundation.coproduct-types
15+
open import foundation.dependent-pair-types
16+
open import foundation.equality-cartesian-product-types
17+
open import foundation.equivalences
18+
open import foundation.function-extensionality
19+
open import foundation.function-types
20+
open import foundation.homotopies
21+
open import foundation.identity-types
22+
open import foundation.sets
23+
open import foundation.truncated-types
24+
open import foundation.truncation-levels
25+
open import foundation.unit-type
26+
open import foundation.universe-levels
27+
28+
open import lists.finite-sequences
29+
open import lists.focus-at-index-finite-sequences
30+
open import lists.insert-at-index-finite-sequences
31+
open import lists.remove-at-index-finite-sequences
32+
open import lists.sequences
33+
34+
open import univalent-combinatorics.involution-standard-finite-types
35+
open import univalent-combinatorics.standard-finite-types
36+
```
37+
38+
</details>
39+
40+
## Idea
41+
42+
A [finite sequence](lists.finite-sequences.md) of types `A : Fin n → UU l`
43+
induces a type `Πₙ A = (i : Fin n) → A i`, i.e.,
44+
45+
```text
46+
Πₙ A ≃ A₀ × A₁ × ... × Aᵢ × ... Aₙ₋₁
47+
```
48+
49+
For any [natural number](elementary-number-theory.natural-numbers.md) `n`, and
50+
and any [index](univalent-combinatorics.standard-finite-types.md)
51+
`i : Fin (n+1)`,
52+
53+
```text
54+
Πₙ₊₁ A ≃ Aᵢ × Πₙ Aⁱ
55+
```
56+
57+
where `Aⁱ` denotes the finite sequence of types obtained by
58+
[removing](lists.remove-at-index-finite-sequences.md) the `i`th component of `A`
59+
so `Πₙ Aⁱ = A₀ × ... Aᵢ₋₁ × Aᵢ₊ᵢ × ... × Aₙ`.
60+
61+
## Definition
62+
63+
### Elements of a finite product of types
64+
65+
```agda
66+
module _
67+
{l : Level} (n : ℕ) (A : Fin n → UU l)
68+
where
69+
70+
Π-fin-sequence : UU l
71+
Π-fin-sequence = (i : Fin n) → A i
72+
```
73+
74+
## Properties
75+
76+
### Coordinate maps of finite products
77+
78+
```agda
79+
module _
80+
{l : Level} (n : ℕ) (A : Fin n → UU l)
81+
where
82+
83+
elem-at-Π-fin-sequence :
84+
(i : Fin n) → Π-fin-sequence n A → A i
85+
elem-at-Π-fin-sequence i u = u i
86+
```
87+
88+
### Insertion at an index
89+
90+
```agda
91+
insert-at-Π-fin-sequence :
92+
{l : Level} →
93+
(n : ℕ) →
94+
(A : Fin (succ-ℕ n) → UU l) →
95+
(i : Fin (succ-ℕ n)) →
96+
(x : A i) →
97+
Π-fin-sequence n (remove-at-fin-sequence n i A) →
98+
Π-fin-sequence (succ-ℕ n) A
99+
insert-at-Π-fin-sequence zero-ℕ A (inr _) x _ (inr _) = x
100+
insert-at-Π-fin-sequence (succ-ℕ n) A (inl i) x u (inl j) =
101+
insert-at-Π-fin-sequence
102+
( n)
103+
( tail-fin-sequence (succ-ℕ n) A)
104+
( i)
105+
( x)
106+
( u ∘ (inl-Fin n))
107+
( j)
108+
insert-at-Π-fin-sequence (succ-ℕ n) A (inl i) x u (inr j) = u (inr j)
109+
insert-at-Π-fin-sequence (succ-ℕ n) A (inr i) x u (inl j) = u j
110+
insert-at-Π-fin-sequence (succ-ℕ n) A (inr i) x u (inr j) = x
111+
```
112+
113+
### Removing at an index
114+
115+
```agda
116+
remove-at-Π-fin-sequence :
117+
{l : Level} →
118+
(n : ℕ)
119+
(A : Fin (succ-ℕ n) → UU l) →
120+
(i : Fin (succ-ℕ n)) →
121+
Π-fin-sequence (succ-ℕ n) A →
122+
Π-fin-sequence n (remove-at-fin-sequence n i A)
123+
remove-at-Π-fin-sequence zero-ℕ A (inr _) u ()
124+
remove-at-Π-fin-sequence (succ-ℕ n) A (inl i) u (inl j) =
125+
remove-at-Π-fin-sequence
126+
( n)
127+
( tail-fin-sequence (succ-ℕ n) A)
128+
( i)
129+
( u ∘ inl-Fin (succ-ℕ n))
130+
( j)
131+
remove-at-Π-fin-sequence (succ-ℕ n) A (inl i) u (inr _) = u (inr _)
132+
remove-at-Π-fin-sequence (succ-ℕ n) A (inr i) u j = u (inl j)
133+
```
134+
135+
### Focusing at in index
136+
137+
```agda
138+
focus-at-Π-fin-sequence :
139+
{l : Level} →
140+
(n : ℕ)
141+
(A : Fin (succ-ℕ n) → UU l) →
142+
(i : Fin (succ-ℕ n)) →
143+
Π-fin-sequence (succ-ℕ n) A →
144+
(A i × Π-fin-sequence n (remove-at-fin-sequence n i A))
145+
focus-at-Π-fin-sequence n A i u =
146+
( elem-at-Π-fin-sequence (succ-ℕ n) A i u ,
147+
remove-at-Π-fin-sequence n A i u)
148+
149+
unfocus-at-Π-fin-sequence :
150+
{l : Level} →
151+
(n : ℕ)
152+
(A : Fin (succ-ℕ n) → UU l) →
153+
(i : Fin (succ-ℕ n)) →
154+
(A i × Π-fin-sequence n (remove-at-fin-sequence n i A)) →
155+
Π-fin-sequence (succ-ℕ n) A
156+
unfocus-at-Π-fin-sequence n A i (x , u) = insert-at-Π-fin-sequence n A i x u
157+
```
158+
159+
### The coordinate at the index of an inserted element is the inserted element
160+
161+
```agda
162+
compute-elem-at-insert-at-Π-fin-sequence :
163+
{l : Level} →
164+
(n : ℕ) →
165+
(A : Fin (succ-ℕ n) → UU l) →
166+
(i : Fin (succ-ℕ n)) →
167+
(x : A i) →
168+
(u : Π-fin-sequence n (remove-at-fin-sequence n i A)) →
169+
elem-at-Π-fin-sequence (succ-ℕ n) A i (insert-at-Π-fin-sequence n A i x u) ＝
170+
x
171+
compute-elem-at-insert-at-Π-fin-sequence zero-ℕ A (inr _) x u = refl
172+
compute-elem-at-insert-at-Π-fin-sequence (succ-ℕ n) A (inl i) x u =
173+
compute-elem-at-insert-at-Π-fin-sequence
174+
( n)
175+
( tail-fin-sequence (succ-ℕ n) A)
176+
( i)
177+
( x)
178+
( u �� inl-Fin n)
179+
compute-elem-at-insert-at-Π-fin-sequence (succ-ℕ n) A (inr i) x u = refl
180+
```
181+
182+
### Inserting a removed element is the identity
183+
184+
```agda
185+
compute-insert-at-remove-at-Π-fin-sequence :
186+
{l : Level} →
187+
(n : ℕ) →
188+
(A : Fin (succ-ℕ n) → UU l) →
189+
(i : Fin (succ-ℕ n)) →
190+
(u : Π-fin-sequence (succ-ℕ n) A) →
191+
insert-at-Π-fin-sequence
192+
( n)
193+
( A)
194+
( i)
195+
( elem-at-Π-fin-sequence (succ-ℕ n) A i u)
196+
( remove-at-Π-fin-sequence n A i u) ~
197+
u
198+
compute-insert-at-remove-at-Π-fin-sequence zero-ℕ A (inr _) u (inr _) = refl
199+
compute-insert-at-remove-at-Π-fin-sequence (succ-ℕ n) A (inl i) u (inl j) =
200+
compute-insert-at-remove-at-Π-fin-sequence
201+
( n)
202+
( tail-fin-sequence (succ-ℕ n) A)
203+
( i)
204+
( u ∘ inl-Fin (succ-ℕ n))
205+
( j)
206+
compute-insert-at-remove-at-Π-fin-sequence (succ-ℕ n) A (inl i) u (inr j) = refl
207+
compute-insert-at-remove-at-Π-fin-sequence (succ-ℕ n) A (inr i) u (inl j) = refl
208+
compute-insert-at-remove-at-Π-fin-sequence (succ-ℕ n) A (inr i) u (inr j) = refl
209+
```
210+
211+
### Removing an inserted element is the identity
212+
213+
```agda
214+
compute-remove-at-insert-at-Π-fin-sequence :
215+
{l : Level} →
216+
(n : ℕ) →
217+
(A : Fin (succ-ℕ n) → UU l) →
218+
(i : Fin (succ-ℕ n)) →
219+
(x : A i) →
220+
(u : Π-fin-sequence n (remove-at-fin-sequence n i A)) →
221+
remove-at-Π-fin-sequence
222+
( n)
223+
( A)
224+
( i)
225+
( insert-at-Π-fin-sequence n A i x u) ~
226+
u
227+
compute-remove-at-insert-at-Π-fin-sequence zero-ℕ A i x u ()
228+
compute-remove-at-insert-at-Π-fin-sequence (succ-ℕ n) A (inl i) x u (inl j) =
229+
compute-remove-at-insert-at-Π-fin-sequence
230+
( n)
231+
( tail-fin-sequence (succ-ℕ n) A)
232+
( i)
233+
( x)
234+
( u ∘ inl-Fin n)
235+
( j)
236+
compute-remove-at-insert-at-Π-fin-sequence (succ-ℕ n) A (inl i) x u (inr j) =
237+
refl
238+
compute-remove-at-insert-at-Π-fin-sequence (succ-ℕ n) A (inr i) x u j = refl
239+
```
240+
241+
### Focusing a finite sequence at an index is an equivalence
242+
243+
```agda
244+
module _
245+
{l : Level}
246+
(n : ℕ)
247+
(A : Fin (succ-ℕ n) → UU l)
248+
(i : Fin (succ-ℕ n))
249+
where abstract
250+
251+
is-section-focus-at-Π-finite-sequence :
252+
focus-at-Π-fin-sequence n A i ∘ unfocus-at-Π-fin-sequence n A i ~ id
253+
is-section-focus-at-Π-finite-sequence (x , u) =
254+
eq-pair
255+
( compute-elem-at-insert-at-Π-fin-sequence n A i x u)
256+
( eq-htpy (compute-remove-at-insert-at-Π-fin-sequence n A i x u))
257+
258+
is-retraction-focus-at-Π-finite-sequence :
259+
unfocus-at-Π-fin-sequence n A i ∘ focus-at-Π-fin-sequence n A i ~ id
260+
is-retraction-focus-at-Π-finite-sequence =
261+
eq-htpy ∘ compute-insert-at-remove-at-Π-fin-sequence n A i
262+
263+
is-equiv-focus-at-Π-finite-sequence :
264+
is-equiv (focus-at-Π-fin-sequence n A i)
265+
is-equiv-focus-at-Π-finite-sequence =
266+
is-equiv-is-invertible
267+
( unfocus-at-Π-fin-sequence n A i)
268+
( is-section-focus-at-Π-finite-sequence)
269+
( is-retraction-focus-at-Π-finite-sequence)
270+
271+
module _
272+
{l : Level}
273+
(n : ℕ)
274+
(A : Fin (succ-ℕ n) → UU l)
275+
where
276+
277+
Π-equiv-focus-at-Π-fin-sequence :
278+
Π-fin-sequence
279+
( succ-ℕ n)
280+
( λ i →
281+
Π-fin-sequence (succ-ℕ n) A ≃
282+
A i × Π-fin-sequence n (remove-at-fin-sequence n i A))
283+
Π-equiv-focus-at-Π-fin-sequence i =
284+
( focus-at-Π-fin-sequence n A i ,
285+
is-equiv-focus-at-Π-finite-sequence n A i)
286+
```

‎src/lists/finite-sequences.lagda.md‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,17 @@ module _
9999

100100
## Properties
101101

102+
### The coordinates maps
103+
104+
```agda
105+
module _
106+
{l : Level} {A : UU l} (n : ℕ)
107+
where
108+
109+
elem-at-fin-sequence : (i : Fin n) → fin-sequence A n → A
110+
elem-at-fin-sequence i v = v i
111+
```
112+
102113
### The type of finite sequences of elements in a truncated type is truncated
103114

104115
```agda

0 commit comments

Comments
 (0)