Martin Escardo, January 2021.

It is possible to work with lists *defined* from the ingredients of
our Spartan MLTT (see the module Fin.lagda). For the moment we are
Athenian in this respect.

\begin{code}

{-# OPTIONS --safe --without-K --no-exact-split #-}

module MLTT.List where

open import MLTT.Spartan
open import MLTT.Bool
open import Naturals.Properties
open import Naturals.Order hiding (minus)
open import Notation.Order
open import UF.Base
open import UF.Subsingletons

data List {𝓀} (X : 𝓀 Μ‡ ) : 𝓀 Μ‡ where
 [] : List X
 _∷_ : X β†’ List X β†’ List X

infixr 3 _∷_

{-# BUILTIN LIST List #-}

length : {X : 𝓀 Μ‡ } β†’ List X β†’ β„•
length []       = 0
length (x ∷ xs) = succ (length xs)

course-of-values-induction-on-length
 : {X : 𝓀 Μ‡ }
 β†’ (P : List X β†’ π“₯ Μ‡ )
 β†’ ((xs : List X) β†’ ((ys : List X) β†’ length ys < length xs β†’ P ys) β†’ P xs)
 β†’ (xs : List X) β†’ P xs
course-of-values-induction-on-length {𝓀} {π“₯} {X} =
 course-of-values-induction-on-value-of-function length

Vector' : 𝓀 Μ‡ β†’ β„• β†’ 𝓀 Μ‡
Vector' X n = (Ξ£ xs κž‰ List X , length xs ＝ n)

_∷'_ : {X : 𝓀 Μ‡ } {n : β„•} β†’ X β†’ Vector' X n β†’ Vector' X (succ n)
x ∷' (xs , p) = (x ∷ xs) , ap succ p

equal-heads : {X : 𝓀 Μ‡ } {x y : X} {s t : List X}
            β†’ x ∷ s ＝ y ∷ t
            β†’ x ＝ y
equal-heads refl = refl

equal-tails : {X : 𝓀 Μ‡ } {x y : X} {s t : List X}
            β†’ x ∷ s ＝ y ∷ t
            β†’ s ＝ t
equal-tails refl = refl

equal-head-tail : {X : 𝓀 Μ‡ } {x : X} {s t : List X}
                β†’ x ∷ s ＝ t
                β†’ Ξ£ y κž‰ X , Ξ£ t' κž‰ List X , (t ＝ y ∷ t')
equal-head-tail {𝓀} {X} {x} {s} {t} refl = x , s , refl

[_] : {X : 𝓀 Μ‡ } β†’ X β†’ List X
[ x ] = x ∷ []

[]-is-not-cons : {X : 𝓀 Μ‡ } (x : X) (xs : List X)
               β†’ [] β‰  x ∷ xs
[]-is-not-cons x []        ()
[]-is-not-cons x (xβ‚€ ∷ xs) ()

_++_ : {X : 𝓀 Μ‡ } β†’ List X β†’ List X β†’ List X
[]      ++ t = t
(x ∷ s) ++ t = x ∷ (s ++ t)

infixr 2 _++_

[]-right-neutral : {X : 𝓀 Μ‡ } (s : List X) β†’ s ＝ s ++ []
[]-right-neutral []      = refl
[]-right-neutral (x ∷ s) = ap (x ∷_) ([]-right-neutral s)

++-assoc : {X : 𝓀 Μ‡ } β†’ associative (_++_ {𝓀} {X})
++-assoc []      t u = refl
++-assoc (x ∷ s) t u = ap (x ∷_) (++-assoc s t u)

foldr : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y β†’ Y) β†’ Y β†’ List X β†’ Y
foldr _Β·_ Ξ΅ []       = Ξ΅
foldr _·_ Ρ (x ∷ xs) = x · foldr _·_ Ρ xs

map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ List X β†’ List Y
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

_<$>_ = map

is-non-empty : {X : 𝓀 Μ‡ } β†’ List X β†’ 𝓀 Μ‡
is-non-empty []       = 𝟘
is-non-empty (x ∷ xs) = πŸ™

-- cons-is-non-empty : {X : 𝓀 Μ‡ } {x : X} {xs : List X} β†’ is-non-empty (x ∷ xs)
pattern cons-is-non-empty = ⋆

list-non-emptiness-is-decidable : {X : 𝓀 Μ‡ }
                                  (xs : List X)
                                β†’ is-decidable (is-non-empty xs)
list-non-emptiness-is-decidable [] = inr 𝟘-elim
list-non-emptiness-is-decidable (x ∷ xs) = inl cons-is-non-empty

map-is-non-empty : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (xs : List X)
                 β†’ is-non-empty xs
                 β†’ is-non-empty (map f xs)
map-is-non-empty f (x ∷ xs) cons-is-non-empty = cons-is-non-empty


[]-is-empty : {X : 𝓀 Μ‡ } β†’ Β¬ is-non-empty ([] {𝓀} {X})
[]-is-empty = 𝟘-elim

is-non-empty-++ : {X : 𝓀 Μ‡ } (xs ys : List X)
                β†’ is-non-empty xs
                β†’ is-non-empty (xs ++ ys)
is-non-empty-++ (x ∷ xs) ys ⋆ = ⋆

empty : {X : 𝓀 Μ‡ } β†’ List X β†’ Bool
empty []       = true
empty (x ∷ xs) = false

data member {X : 𝓀 Μ‡ } : X β†’ List X β†’ 𝓀 Μ‡ where
 in-head : {x : X}   {xs : List X} β†’ member x (x ∷ xs)
 in-tail : {x y : X} {xs : List X} β†’ member x xs β†’ member x (y ∷ xs)

empty-list-has-no-members : {X : 𝓀 Μ‡ }
                            (x : X)
                          β†’ Β¬ member x []
empty-list-has-no-members x ()

lists-with-members-are-non-empty : {X : 𝓀 Μ‡ }
                                   {y : X}
                                   {xs : List X}
                                 β†’ member y xs
                                 β†’ is-non-empty xs
lists-with-members-are-non-empty in-head     = cons-is-non-empty
lists-with-members-are-non-empty (in-tail m) = cons-is-non-empty

member-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (x : X) (xs : List X)
           β†’ member x xs
           β†’ member (f x) (map f xs)
member-map f x' (_ ∷ _)  in-head     = in-head
member-map f x' (_ ∷ xs) (in-tail m) = in-tail (member-map f x' xs m)

private
 filter-helper : {X : 𝓀 Μ‡ } (p : X β†’ π“₯ Μ‡ )
               β†’ (x : X)
               β†’ p x + Β¬ p x
               β†’ List X
               β†’ List X
 filter-helper p x (inl _) xs = x ∷ xs
 filter-helper p x (inr _) xs = xs

filter : {X : 𝓀 Μ‡ } (p : X β†’ π“₯ Μ‡ ) β†’ ((x : X) β†’ p x + Β¬ p x) β†’ List X β†’ List X
filter p Ξ΄ []       = []
filter p δ (x ∷ xs) = filter-helper p x (δ x) (filter p δ xs)

open import MLTT.Plus-Properties

filter-memberβ†’ : {X : 𝓀 Μ‡ }
                 (p : X β†’ π“₯ Μ‡ )
                 (Ξ΄ : (x : X) β†’ p x + Β¬ p x)
                 (y : X)
                 (xs : List X)
               β†’ member y (filter p Ξ΄ xs)
               β†’ p y
filter-memberβ†’ {𝓀} {π“₯} {X} p Ξ΄ y (x ∷ xs) = h x xs (Ξ΄ x)
 where
  h : (x : X)
      (xs : List X)
    β†’ (d : p x + Β¬ p x)
    β†’ member y (filter-helper p x d (filter p Ξ΄ xs))
    β†’ p y
  h x xs        (inl l) in-head     = l
  h x xs        (inl _) (in-tail m) = filter-member→ p δ y xs m
  h x (x' ∷ xs) (inr _) m           = h x' xs (δ x') m

filter-member← : {X : 𝓀 Μ‡ }
                 (p : X β†’ π“₯ Μ‡ )
                 (Ξ΄ : (x : X) β†’ p x + Β¬ p x)
                 (y : X)
                 (xs : List X)
               β†’ p y
               β†’ member y xs
               β†’ member y (filter p Ξ΄ xs)
filter-member← {𝓀} {π“₯} {X} p Ξ΄ y (x ∷ xs) = h x xs (Ξ΄ x)
 where
  h : (x : X)
      (xs : List X)
    β†’ (d : p x + Β¬ p x)
    β†’ p y
    β†’ member y (x ∷ xs)
    β†’ member y (filter-helper p x d (filter p Ξ΄ xs))
  h x xs (inl _) py in-head = in-head
  h x (x' ∷ xs) (inl _) py (in-tail m) = in-tail (h x' xs (δ x') py m)
  h x xs (inr r) py in-head = 𝟘-elim (r py)
  h x xs (inr _) py (in-tail m) = filter-member← p Ξ΄ y xs py m

member' : {X : 𝓀 Μ‡ } β†’ X β†’ List X β†’ 𝓀 Μ‡
member' y []       = 𝟘
member' y (x ∷ xs) = (x ＝ y) + member' y xs

member'-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (x : X) (xs : List X)
            β†’ member' x xs
            β†’ member' (f x) (map f xs)
member'-map f x' (x ∷ xs) (inl p) = inl (ap f p)
member'-map f x' (x ∷ xs) (inr m) = inr (member'-map f x' xs m)

listed : 𝓀 Μ‡ β†’ 𝓀 Μ‡
listed X = Ξ£ xs κž‰ List X , ((x : X) β†’ member x xs)

the-list : {X : 𝓀 Μ‡ } β†’ listed X β†’ List X
the-list (xs , m) = xs

member-of-the-list : {X : 𝓀 Μ‡ } (X-is-listed : listed X)
                   β†’ (x : X) β†’ member x (the-list X-is-listed)
member-of-the-list (xs , m) = m

πŸ™-is-listed : listed (πŸ™ {𝓀})
πŸ™-is-listed = (⋆ ∷ []) , (Ξ» x β†’ in-head)

listed⁺ : 𝓀 Μ‡ β†’ 𝓀 Μ‡
listed⁺ X = X Γ— listed X

distinguished-element : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ X
distinguished-element (x , X-listed) = x

listed⁺-types-are-listed : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ listed X
listed⁺-types-are-listed (x , X-is-listed) = X-is-listed

πŸ™-is-listed⁺ : listed⁺ (πŸ™ {𝓀})
πŸ™-is-listed⁺ = ⋆ , πŸ™-is-listed

type-from-list : {X : 𝓀 Μ‡ } β†’ List X β†’ 𝓀 Μ‡
type-from-list {𝓀} {X} xs = Ξ£ x κž‰ X , member x xs

type-from-list-is-listed : {X : 𝓀 Μ‡ } (xs : List X)
                         β†’ listed (type-from-list xs)
type-from-list-is-listed {𝓀} {X} [] = [] , g
 where
  g : (Οƒ : type-from-list []) β†’ member Οƒ []
  g (x , ())
type-from-list-is-listed {𝓀} {X} (x ∷ xs) = g
 where
  h : (x : X) β†’ type-from-list (x ∷ xs)
  h x = x , in-head

  t : type-from-list xs β†’ type-from-list (x ∷ xs)
  t (x , m) = x , in-tail m

  Ξ± : List (type-from-list xs) β†’ List (type-from-list (x ∷ xs))
  Ξ± Οƒs = h x ∷ map t Οƒs

  Ξ² : ((Οƒs , ΞΌ) : listed (type-from-list xs))
    β†’ (Ο„ : type-from-list (x ∷ xs)) β†’ member Ο„ (Ξ± Οƒs)
  Ξ² (Οƒs , ΞΌ) (y , in-head)   = in-head
  Ξ² (Οƒs , ΞΌ) (y , in-tail m) = in-tail (member-map t (y , m) Οƒs (ΞΌ (y , m)))

  f : listed (type-from-list xs) β†’ listed (type-from-list (x ∷ xs))
  f (Οƒs , ΞΌ) = Ξ± Οƒs , Ξ² (Οƒs , ΞΌ)

  g : listed (type-from-list (x ∷ xs))
  g = f (type-from-list-is-listed xs)

module _ {X : 𝓀 Μ‡ } where

 delete : {n : β„•}
          {y : X}
          ((xs , _) : Vector' X (succ n))
        β†’ member y xs
        β†’ Vector' X n
 delete {0}      _              in-head     = [] , refl
 delete {0}      _              (in-tail _) = [] , refl
 delete {succ _} ((_ ∷ xs) , p) in-head     = xs , succ-lc p
 delete {succ n} ((x ∷ xs) , p) (in-tail m) = x ∷' delete {n} (xs , succ-lc p) m

module list-util
        {𝓀 : Universe}
        {X : 𝓀 Μ‡ }
        {{_ : Eq X}}
       where

 _is-in_ : X β†’ List X β†’ Bool
 x is-in []       = false
 x is-in (y ∷ ys) = (x == y) || (x is-in ys)

 insert : X β†’ List X β†’ List X
 insert x xs = x ∷ xs

 _contained-in_ : List X β†’ List X β†’ Bool
 []       contained-in ys = true
 (x ∷ xs) contained-in ys = (x is-in ys) && (xs contained-in ys)

 contained-lemmaβ‚€ : (x z : X) (xs ys : List X)
                  β†’ ys contained-in (x ∷ xs) ＝ true
                  β†’ ys contained-in (x ∷ z ∷ xs) ＝ true
 contained-lemmaβ‚€ x z xs []       e = e
 contained-lemmaβ‚€ x z xs (y ∷ ys) e = Ξ³
  where
   IH : ys contained-in (x ∷ xs) ＝ true β†’ ys contained-in (x ∷ z ∷ xs) ＝ true
   IH = contained-lemmaβ‚€ x z xs ys

   e₁ : (y == x) || (y is-in xs) ＝ true
   e₁ = pr₁ (&&-gives-Γ— e)

   eβ‚‚ : ys contained-in (x ∷ xs) ＝ true
   eβ‚‚ = prβ‚‚ (&&-gives-Γ— e)

   a : (y == x) || ((y == z) || (y is-in xs)) ＝ true
   a = Cases (||-gives-+ e₁)
        (Ξ» (e : (y == x) ＝ true)   β†’ ||-left-intro ((y == z) || (y is-in xs)) e)
        (Ξ» (e : y is-in xs ＝ true) β†’ ||-right-intro {y == x} ((y == z) || (y is-in xs)) (||-right-intro (y is-in xs) e))

   b : ys contained-in (x ∷ z ∷ xs) ＝ true
   b = IH eβ‚‚

   γ : ((y == x) || ((y == z) || (y is-in xs))) && (ys contained-in (x ∷ z ∷ xs)) ＝ true
   Ξ³ = &&-intro a b

 contained-lemma₁ : (x : X) (ys : List X)
                  β†’ ys contained-in (x ∷ ys) ＝ true
 contained-lemma₁ x []       = refl
 contained-lemma₁ x (y ∷ ys) = Ξ³
  where
   IH : ys contained-in (x ∷ ys) ＝ true
   IH = contained-lemma₁ x ys

   a : y == x || (y == y || (y is-in ys)) ＝ true
   a = ||-right-intro {y == x} ((y == y) || (y is-in ys)) (||-left-intro (y is-in ys) (==-refl y))

   b : ys contained-in (x ∷ y ∷ ys) ＝ true
   b = contained-lemmaβ‚€ x y ys ys IH

   γ : (y == x || (y == y || (y is-in ys))) && (ys contained-in (x ∷ y ∷ ys)) ＝ true
   Ξ³ = &&-intro a b

 some-contained : List (List X) β†’ List X β†’ Bool
 some-contained []         ys = false
 some-contained (xs ∷ xss) ys = xs contained-in ys || some-contained xss ys

 remove-first : X β†’ List X β†’ List X
 remove-first x []       = []
 remove-first x (y ∷ ys) = if x == y then ys else (y ∷ remove-first x ys)

 remove-all : X β†’ List X β†’ List X
 remove-all x []       = []
 remove-all x (y ∷ ys) = if x == y then remove-all x ys else (y ∷ remove-all x ys)

 _minus_ : List X β†’ List X β†’ List X
 xs minus []       = xs
 xs minus (y ∷ ys) = (remove-all y xs) minus ys

\end{code}

Remove first occurrence:

\begin{code}

 remove : X β†’ List X β†’ List X
 remove x []       = []
 remove x (y ∷ ys) = if x == y then ys else (y ∷ remove x ys)

 remove-head : (x y : X) (ys : List X)
             β†’ (x == y) ＝ true
             β†’ remove x (y ∷ ys) ＝ ys
 remove-head x y ys q =
  remove x (y ∷ ys)                          ＝⟨ refl ⟩
  (if x == y then ys else (y ∷ remove x ys)) ＝⟨ I ⟩
  (if true then ys else (y ∷ remove x ys))   ＝⟨ refl ⟩
  ys                                         ∎
   where
    I = ap (Ξ» - β†’ if - then ys else (y ∷ remove x ys)) q

 remove-tail : (x y : X) (ys : List X)
             β†’ (x == y) ＝ false
             β†’ remove x (y ∷ ys) ＝ y ∷ remove x ys
 remove-tail x y ys q =
  remove x (y ∷ ys)                        ＝⟨ refl ⟩
  if x == y then ys else (y ∷ remove x ys) ＝⟨ I ⟩
  if false then ys else (y ∷ remove x ys)  ＝⟨ refl ⟩
  y ∷ remove x ys                          ∎
   where
    I  = ap (Ξ» - β†’ if - then ys else (y ∷ remove x ys)) q

 remove-length : (x : X) (ys : List X)
               β†’ member x ys
               β†’ (n : β„•)
               β†’ length ys ＝ succ n
               β†’ length (remove x ys) ＝ n
 remove-length x ys@(z ∷ zs) m n p = h m n p (x == z) refl
  where
   h : member x ys
     β†’ (n : β„•)
     β†’ length ys ＝ succ n
     β†’ (b : Bool) β†’ (x == z) ＝ b β†’ length (remove x ys) ＝ n
   h _ n p true q =
    length (remove x (z ∷ zs)) ＝⟨ ap length (remove-head x z zs q) ⟩
    length zs                  ＝⟨ succ-lc p ⟩
    n                          ∎

   h in-head n p false q =
    𝟘-elim (true-is-not-false
             (true    ＝⟨ (==-refl x)⁻¹ ⟩
             (x == x) ＝⟨ q ⟩
             false    ∎))
   h (in-tail in-head)     0        () false q
   h (in-tail (in-tail m)) 0        () false q
   h (in-tail m)           (succ n) p  false q =
    length (remove x (z ∷ zs))  ＝⟨ I ⟩
    length (z ∷ remove x zs)    ＝⟨ refl ⟩
    succ (length (remove x zs)) ＝⟨ II ⟩
    succ n                      ∎
     where
      I  = ap length (remove-tail x z zs q)
      II = ap succ (remove-length x zs m n (succ-lc p))

 delete' : {n : β„•}
           (x : X)
           ((xs , _) : Vector' X (succ n))
         β†’ member x xs
         β†’ Vector' X n
 delete' {n} x (xs , p) m = remove x xs , remove-length x xs m n p

\end{code}

Added by Ayberk Tosun on 2023-10-16.

\begin{code}

right-concatenation-preserves-membership : {X : 𝓀 Μ‡ } (x : X) (xs ys : List X)
                                         β†’ member x xs
                                         β†’ member x (xs ++ ys)
right-concatenation-preserves-membership x xs@(xβ€² ∷ _)   ys in-head = in-head
right-concatenation-preserves-membership x xs@(xβ€² ∷ xsβ€²) ys (in-tail p) =
 in-tail (right-concatenation-preserves-membership x xsβ€² ys p)

left-concatenation-preserves-membership : {X : 𝓀 Μ‡ } (x : X) (xs ys : List X)
                                      β†’ member x xs
                                      β†’ member x (ys ++ xs)
left-concatenation-preserves-membership x xs []       p = p
left-concatenation-preserves-membership x xs (y ∷ ys) p = †
 where
  † : member x (y ∷ (ys ++ xs))
  † = in-tail (left-concatenation-preserves-membership x xs ys p)

split-++-membership : {X : 𝓀 Μ‡ } (x : X) (xs ys : List X)
                    β†’ member x (xs ++ ys)
                    β†’ member x xs + member x ys
split-++-membership x []       zs p           = inr p
split-++-membership x (x ∷ ys) zs in-head     = inl in-head
split-++-membership x (y ∷ ys) zs (in-tail p) =
 cases † ‑ (split-++-membership x ys zs p)
 where
  † : member x ys β†’ member x (y ∷ ys) + member x zs
  † p = inl (in-tail p)

  ‑ : member x zs β†’ member x (y ∷ ys) + member x zs
  ‑ = inr

\end{code}

Added 2nd April 2024 by Martin Escardo and Paulo Oliva. Ingredients
for the list monad.

\begin{code}

map-++ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
         (f : X β†’ Y)
         (xs ys : List X)
       β†’ map f (xs ++ ys) ＝ map f xs ++ map f ys
map-++ f [] ys       = refl
map-++ f (x ∷ xs) ys = ap (f x ∷_) (map-++ f xs ys)

map-id : {X : 𝓀 Μ‡ }
         (xs : List X)
       β†’ map id xs ＝ xs
map-id [] = refl
map-id (x ∷ xs) = ap (x ∷_) (map-id xs)

map-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
        (f : X β†’ Y) (g : Y β†’ Z)
      β†’ map (g ∘ f) ∼ map g ∘ map f
map-∘ f g []       = refl
map-∘ f g (x ∷ xs) = ap (g (f x) ∷_) (map-∘ f g xs)

concat : {X : 𝓀 Μ‡ } β†’ List (List X) β†’ List X
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

concat-singletons' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     (g : X β†’ Y)
                     (xs : List X)
                   β†’ concat (map (Ξ» x β†’ [ g x ]) xs) ＝ map g xs
concat-singletons' g []       = refl
concat-singletons' g (x ∷ xs) = ap (g x ∷_) (concat-singletons' g xs)

concat-singletons : {X : 𝓀 Μ‡ }
                    (xs : List X) β†’ concat (map [_] xs) ＝ xs
concat-singletons xs = concat-singletons' id xs βˆ™ map-id xs

concat-++ : {X : 𝓀 Μ‡ }
            (xss yss : List (List X))
          β†’ concat (xss ++ yss) ＝ concat xss ++ concat yss
concat-++ [] yss = refl
concat-++ (xs ∷ xss) yss =
 concat (xs ∷ xss ++ yss)         ＝⟨ refl ⟩
 xs ++ concat (xss ++ yss)        ＝⟨ I ⟩
 xs ++ (concat xss ++ concat yss) ＝⟨ II ⟩
 (xs ++ concat xss) ++ concat yss ＝⟨ refl ⟩
 concat (xs ∷ xss) ++ concat yss  ∎
  where
   I  = ap (xs ++_) (concat-++ xss yss)
   II = (++-assoc xs (concat xss) (concat yss))⁻¹

\end{code}

The following are the Kleisli extension operations for the list monad
and its associativity law.

\begin{code}

List-ext : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
         β†’ (X β†’ List Y) β†’ (List X β†’ List Y)
List-ext f xs = concat (map f xs)

List-ext-unit : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                (f : X β†’ List Y) (x : X)
              β†’ f x ++ [] ＝ f x
List-ext-unit f x = ([]-right-neutral (f x))⁻¹

List-ext-assoc
 : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
   (g : Y β†’ List Z) (f : X β†’ List Y)
   (xs : List X)
 β†’ List-ext (Ξ» x β†’ List-ext g (f x)) xs ＝ List-ext g (List-ext f xs)
List-ext-assoc g f []       = refl
List-ext-assoc g f (x ∷ xs) =
 List-ext (Ξ» - β†’ List-ext g (f -)) (x ∷ xs)               ＝⟨ refl ⟩
 List-ext g (f x) ++ List-ext (Ξ» - β†’ List-ext g (f -)) xs ＝⟨ I ⟩
 List-ext g (f x) ++ List-ext g (List-ext f xs)           ＝⟨ II ⟩
 concat (map g (f x) ++ map g (List-ext f xs))            ＝⟨ III ⟩
 List-ext g (f x ++ List-ext f xs)                        ＝⟨ refl ⟩
 List-ext g (List-ext f (x ∷ xs))                         ∎
  where
   I   = ap (List-ext g (f x) ++_) (List-ext-assoc g f xs)
   II  = (concat-++ (map g (f x)) (map g (List-ext f xs)))⁻¹
   III = (ap concat (map-++ g (f x) (List-ext f xs)))⁻¹

map' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ List X β†’ List Y
map' f = List-ext (Ξ» x β†’ [ f x ])

map-agrees-with-map' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                       (f : X β†’ Y)
                     β†’ map f ∼ map' f
map-agrees-with-map' f [] = refl
map-agrees-with-map' f (x ∷ xs) = ap (f x ∷_) (map-agrees-with-map' f xs)

\end{code}

Added by Martin Escardo and Paulo Oliva 12th March 2025.

\begin{code}

member-of-concat← : {X : 𝓀 Μ‡ } (x : X) (yss : List (List X))
                  β†’ member x (concat yss)
                  β†’ Ξ£ ys κž‰ List X , member ys yss Γ— member x ys
member-of-concat← {𝓀} {X} x (ys ∷ yss) m = II I
 where
  I : member x ys + member x (concat yss)
  I = split-++-membership x ys (concat yss) m

  II : type-of I β†’ Ξ£ ys' κž‰ List X , member ys' (ys ∷ yss) Γ— member x ys'
  II (inl l) = ys , in-head , l
  II (inr r) = III IH
   where
    IH : Ξ£ ys' κž‰ List X , member ys' yss Γ— member x ys'
    IH = member-of-concat← x yss r

    III : type-of IH β†’ Ξ£ ys' κž‰ List X , member ys' (ys ∷ yss) Γ— member x ys'
    III (ys' , r₁ , rβ‚‚) = ys' , in-tail r₁ , rβ‚‚

member-of-map← : {X Y : 𝓀 Μ‡ } (f : X β†’ Y) (y : Y) (xs : List X)
              β†’ member y (map f xs)
              β†’ Ξ£ x κž‰ X , member x xs Γ— (f x ＝ y)
member-of-map← f y (x ∷ xs) in-head = x , in-head , refl
member-of-map← {𝓀} {X} f y (x ∷ xs) (in-tail m) = I IH
 where
  IH : Ξ£ x κž‰ X , member x xs Γ— (f x ＝ y)
  IH = member-of-map← f y xs m

  I : type-of IH β†’ Ξ£ x' κž‰ X , member x' (x ∷ xs) Γ— (f x' ＝ y)
  I (x , m , e) = x , in-tail m , e

\end{code}

Added 10 April 2025 by Fredrik Nordvall Forsberg.

\begin{code}

data All {X : 𝓀 Μ‡ } (P : X β†’ π“₯ Μ‡ ) : List X β†’ 𝓀 βŠ” π“₯ Μ‡  where
  [] : All P []
  _∷_ : {x : X} {xs : List X} β†’ P x β†’ All P xs β†’ All P (x ∷ xs)

All-is-prop : {X : 𝓀 Μ‡ } (P : X β†’ π“₯ Μ‡ )
            β†’ is-prop-valued-family P
            β†’ is-prop-valued-family (All P)
All-is-prop P p [] [] [] = refl
All-is-prop P p (x ∷ l) (a ∷ as) (a' ∷ as') =
 apβ‚‚ _∷_ (p x a a') (All-is-prop P p l as as')

\end{code}

Added by Martin Escardo and Paulo Oliva 14th May 2025.

\begin{code}

member-of-concatβ†’ : {X : 𝓀 Μ‡ } (x : X) (yss : List (List X))
                    (zs : List X)
                  β†’ member zs yss
                  β†’ member x zs
                  β†’ member x (concat yss)
member-of-concatβ†’ x (ys ∷ yss) .ys in-head mβ‚‚ =
 right-concatenation-preserves-membership x ys (concat yss) mβ‚‚
member-of-concatβ†’ x (ys ∷ yss) zs (in-tail m₁) mβ‚‚ =
 left-concatenation-preserves-membership x (concat yss) ys IH
 where
  IH : member x (concat yss)
  IH = member-of-concatβ†’ x yss zs m₁ mβ‚‚

member-of-mapβ†’ : {X Y : 𝓀 Μ‡ } (f : X β†’ Y) (xs : List X)
                 (x : X)
               β†’ member x xs
               β†’ member (f x) (map f xs)
member-of-map→ f xs x in-head = in-head
member-of-mapβ†’ f (_ ∷ xs) x (in-tail m) = in-tail (member-of-mapβ†’ f xs x m)

\end{code}

Added 8-22 October by Martin Escardo and Paulo Oliva.

\begin{code}

conditionally-prepend : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                      β†’ (x : X)
                      β†’ A x + Β¬ A x
                      β†’ List (Ξ£ x κž‰ X , A x)
                      β†’ List (Ξ£ x κž‰ X , A x)
conditionally-prepend A x (inl a) ys = (x , a) ∷ ys
conditionally-prepend A x (inr _) ys = ys

filter' : {X : 𝓀 Μ‡ }
          (A : X β†’ π“₯ Μ‡ )
        β†’ ((x : X) β†’ A x + Β¬ A x)
        β†’ List X
        β†’ List (Ξ£ x κž‰ X , A x)
filter' A Ξ΄ []       = []
filter' A δ (x ∷ xs) = conditionally-prepend A x (δ x) (filter' A δ xs)

filter'-member← : {X : 𝓀 Μ‡ }
                  (A : X β†’ π“₯ Μ‡ )
                  (Ξ΄ : (x : X) β†’ A x + Β¬ A x)
                  (A-is-prop-valued : (x : X) β†’ is-prop (A x))
                  (y : X)
                  (xs : List X)
                  (a : A y)
                β†’ member y xs
                β†’ member (y , a) (filter' A Ξ΄ xs)
filter'-member← {𝓀} {π“₯} {X} A Ξ΄ A-is-prop-valued y (x ∷ xs) = h x xs (Ξ΄ x)
 where
  h : (x : X)
      (xs : List X)
    β†’ (d : A x + Β¬ A x)
      (a : A y)
    β†’ member y (x ∷ xs)
    β†’ member (y , a) (conditionally-prepend A x d (filter' A Ξ΄ xs))
  h x xs (inl b) a in-head = II
   where
    I : member (y , a) ((y , a) ∷ filter' A δ xs)
    I = in-head

    II : member (y , a) ((y , b) ∷ filter' A δ xs)
    II = transport
          (Ξ» - β†’ member (y , a) ((y , -) ∷ filter' A Ξ΄ xs))
          (A-is-prop-valued y a b)
          I
  h x (x' ∷ xs) (inl b) a (in-tail m) = in-tail (h x' xs (δ x') a m)
  h x xs (inr r) a in-head = 𝟘-elim (r a)
  h x xs (inr x₁) a (in-tail m) = filter'-member← A Ξ΄ A-is-prop-valued y xs a m

detachable-subtype-of-listed-type-is-listed
 : {X : Type}
 β†’ (A : X β†’ Type)
 β†’ ((x : X) β†’ is-decidable (A x))
 β†’ ((x : X) β†’ is-prop (A x))
 β†’ listed X
 β†’ listed (Ξ£ x κž‰ X , A x)
detachable-subtype-of-listed-type-is-listed {X} A Ξ΄ A-is-prop-valued (xs , m)
 = filter' A Ξ΄ xs , Ξ³
 where
  Ξ³ : (Οƒ : Ξ£ x κž‰ X , A x) β†’ member Οƒ (filter' A Ξ΄ xs)
  Ξ³ (x , a) = filter'-member← A Ξ΄ A-is-prop-valued x xs a (m x)

\end{code}

Added by Martin Escardo and Paulo Oliva 29th October 2025.

Dependent version of `map`.

\begin{code}

dmap : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } β†’ ((x : X) β†’ Y x) β†’ List X β†’ List (Ξ£ x κž‰ X , Y x)
dmap f []       = []
dmap f (x ∷ xs) = (x , f x) ∷ dmap f xs

\end{code}

We now discuss the non-dependent special case of the above.

\begin{code}

module _ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) where

 pr₁-of-dmap : (xs : List X)
             β†’ xs ＝ map pr₁ (dmap f xs)
 pr₁-of-dmap [] = refl
 pr₁-of-dmap (x ∷ xs) = ap (x ∷_) (pr₁-of-dmap xs)

 map-from-dmap : (xs : List X)
               β†’ map f xs ＝ map prβ‚‚ (dmap f xs)
 map-from-dmap [] = refl
 map-from-dmap (x ∷ xs) = ap (f x ∷_) (map-from-dmap xs)

\end{code}

In the non-dependent case, we can define dmap from map.

\begin{code}

 dmap-from-map : (xs : List X)
               β†’ dmap f xs ＝ map (Ξ» x β†’ x , f x) xs
 dmap-from-map [] = refl
 dmap-from-map (x ∷ xs) = ap ((x , f x) ∷_) (dmap-from-map xs)

\end{code}