# Flattening of lists

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-08.

module lists.flattening-lists where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.sums-of-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.identity-types
open import foundation.universe-levels

open import lists.concatenation-lists
open import lists.functoriality-lists
open import lists.lists


## Idea

Any list of lists of elements of A can be flattened to form a list of elements of A

## Definition

flatten-list : {l : Level} {A : UU l} → list (list A) → list A
flatten-list = fold-list nil concat-list


## Properties

### Properties of flattening

flatten-unit-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (flatten-list (unit-list x)) x
flatten-unit-list x = right-unit-law-concat-list x

length-flatten-list :
{l1 : Level} {A : UU l1} (x : list (list A)) →
Id
( length-list (flatten-list x))
( sum-list-ℕ (map-list length-list x))
length-flatten-list nil = refl
length-flatten-list (cons a x) =
( length-concat-list a (flatten-list x)) ∙
( ap ((length-list a) +ℕ_) (length-flatten-list x))

flatten-concat-list :
{l1 : Level} {A : UU l1} (x y : list (list A)) →
Id
( flatten-list (concat-list x y))
( concat-list (flatten-list x) (flatten-list y))
flatten-concat-list nil y = refl
flatten-concat-list (cons a x) y =
( ap (concat-list a) (flatten-concat-list x y)) ∙
( inv (associative-concat-list a (flatten-list x) (flatten-list y)))

flatten-flatten-list :
{l1 : Level} {A : UU l1} (x : list (list (list A))) →
Id
( flatten-list (flatten-list x))
( flatten-list (map-list flatten-list x))
flatten-flatten-list nil = refl
flatten-flatten-list (cons a x) =
( flatten-concat-list a (flatten-list x)) ∙
( ap (concat-list (flatten-list a)) (flatten-flatten-list x))

flatten-snoc-list :
{l1 : Level} {A : UU l1} (x : list (list A)) (a : list A) →
flatten-list (snoc x a) ＝ concat-list (flatten-list x) a
flatten-snoc-list nil a = right-unit-law-concat-list a
flatten-snoc-list (cons b x) a =
( ap (concat-list b) (flatten-snoc-list x a)) ∙
( inv (associative-concat-list b (flatten-list x) a))