module A201802.WIP.CoquandList where

open import A201801.Prelude
open import A201801.Category

open import A201802.WIP.Bool
open import A201802.WIP.Name


--------------------------------------------------------------------------------


infix 6 _,_⦂_
mutual
  data List (𝔄 : Set) : Set
    where
      βˆ™ : List 𝔄

      _,_⦂_ : (Ξ : List 𝔄) (x : Name) β†’ 𝔄 β†’ {{_ : T (fresh x Ξ)}}
                                      β†’ List 𝔄

  fresh : βˆ€ {𝔄} β†’ Name β†’ List 𝔄 β†’ Bool
  fresh x βˆ™           = true
  fresh x (Ξ , y ⦂ A) = and (x β‰  y) (fresh x Ξ)


--------------------------------------------------------------------------------


infix 4 _βˆ‹_⦂_
data _βˆ‹_⦂_ {𝔄} : List 𝔄 β†’ Name β†’ 𝔄 β†’ Set
  where
    zero : βˆ€ {Ξ A x} β†’ {{_ : T (fresh x Ξ)}}
                     β†’ Ξ , x ⦂ A βˆ‹ x ⦂ A

    suc : βˆ€ {Ξ A B x y} β†’ {{_ : T (fresh y Ξ)}}
                        β†’ Ξ βˆ‹ x ⦂ A
                        β†’ Ξ , y ⦂ B βˆ‹ x ⦂ A


notβˆ‹ : βˆ€ {𝔄 A x} β†’ {Ξ : List 𝔄} {{_ : T (fresh x Ξ)}}
                 β†’ Β¬ (Ξ βˆ‹ x ⦂ A)
notβˆ‹ {x = x} {{Ο†}}  zero             with x β‰Ÿ x
notβˆ‹ {x = x} {{()}} zero             | yes refl
notβˆ‹ {x = x} {{Ο†}}  zero             | no xβ‰’x   = refl β†― xβ‰’x
notβˆ‹ {x = x} {{Ο†}}  (suc {y = y}  i) with x β‰Ÿ y
notβˆ‹ {x = x} {{()}} (suc {y = .x} i) | yes refl
notβˆ‹ {x = x} {{Ο†}}  (suc {y = y}  i) | no xβ‰’y   = i β†― notβˆ‹


uniqβˆ‹ : βˆ€ {𝔄 A x} β†’ {Ξ : List 𝔄} (i j : Ξ βˆ‹ x ⦂ A)
                  β†’ i ≑ j
uniqβˆ‹ zero    zero    = refl
uniqβˆ‹ zero    (suc j) = j β†― notβˆ‹
uniqβˆ‹ (suc i) zero    = i β†― notβˆ‹
uniqβˆ‹ (suc i) (suc j) = suc & uniqβˆ‹ i j


--------------------------------------------------------------------------------


infix 4 _βŠ‡_
data _βŠ‡_ {𝔄} : List 𝔄 β†’ List 𝔄 β†’ Set
  where
    done : βˆ€ {Ξ} β†’ Ξ βŠ‡ βˆ™

    step : βˆ€ {Ξ Ξžβ€² A x} β†’ {{_ : T (fresh x Ξ)}}
                        β†’ Ξžβ€² βŠ‡ Ξ β†’ Ξžβ€² βˆ‹ x ⦂ A
                        β†’ Ξžβ€² βŠ‡ Ξ , x ⦂ A


putβŠ‡ : βˆ€ {𝔄} β†’ {Ξ Ξžβ€² : List 𝔄}
             β†’ (βˆ€ {A x} β†’ Ξ βˆ‹ x ⦂ A β†’ Ξžβ€² βˆ‹ x ⦂ A)
             β†’ Ξžβ€² βŠ‡ Ξ
putβŠ‡ {Ξ = βˆ™}         f = done
putβŠ‡ {Ξ = Ξ , x ⦂ A} f = step (putβŠ‡ (f ∘ suc)) (f zero)


getβŠ‡ : βˆ€ {𝔄 A x} β†’ {Ξ Ξžβ€² : List 𝔄}
                 β†’ Ξžβ€² βŠ‡ Ξ β†’ Ξ βˆ‹ x ⦂ A
                 β†’ Ξžβ€² βˆ‹ x ⦂ A
getβŠ‡ (step Ξ· i) zero    = i
getβŠ‡ (step Ξ· i) (suc j) = getβŠ‡ Ξ· j


uniqβŠ‡ : βˆ€ {𝔄} β†’ {Ξ Ξžβ€² : List 𝔄}
              β†’ (η₁ Ξ·β‚‚ : Ξžβ€² βŠ‡ Ξ)
              β†’ η₁ ≑ Ξ·β‚‚
uniqβŠ‡ done       done        = refl
uniqβŠ‡ (step c i) (step cβ€² j) = step & uniqβŠ‡ c cβ€² βŠ— uniqβˆ‹ i j


dropβŠ‡ : βˆ€ {𝔄 A x} β†’ {Ξ Ξžβ€² : List 𝔄} {{_ : T (fresh x Ξžβ€²)}}
                  β†’ Ξžβ€² βŠ‡ Ξ
                  β†’ Ξžβ€² , x ⦂ A βŠ‡ Ξ
dropβŠ‡ done       = done
dropβŠ‡ (step Ξ· i) = step (dropβŠ‡ Ξ·) (suc i)


keepβŠ‡ : βˆ€ {𝔄 A x} β†’ {Ξ Ξžβ€² : List 𝔄} {{_ : T (fresh x Ξžβ€²)}} {{_ : T (fresh x Ξ)}}
                  β†’ Ξžβ€² βŠ‡ Ξ
                  β†’ Ξžβ€² , x ⦂ A βŠ‡ Ξ , x ⦂ A
keepβŠ‡ Ξ· = step (dropβŠ‡ Ξ·) zero


idβŠ‡ : βˆ€ {𝔄} β†’ {Ξ : List 𝔄}
            β†’ Ξ βŠ‡ Ξ
idβŠ‡ = putβŠ‡ id


_βˆ˜βŠ‡_ : βˆ€ {𝔄} β†’ {Ξ Ξžβ€² Ξžβ€³ : List 𝔄}
             β†’ Ξžβ€² βŠ‡ Ξ β†’ Ξžβ€³ βŠ‡ Ξžβ€²
             β†’ Ξžβ€³ βŠ‡ Ξ
η₁ βˆ˜βŠ‡ Ξ·β‚‚ = putβŠ‡ (getβŠ‡ Ξ·β‚‚ ∘ getβŠ‡ η₁)


--------------------------------------------------------------------------------


lidβˆ˜βŠ‡ : βˆ€ {X} β†’ {Ξ Ξžβ€² : List X}
              β†’ (Ξ· : Ξžβ€² βŠ‡ Ξ)
              β†’ idβŠ‡ βˆ˜βŠ‡ Ξ· ≑ Ξ·
lidβˆ˜βŠ‡ Ξ· = uniqβŠ‡ (idβŠ‡ βˆ˜βŠ‡ Ξ·) Ξ·


ridβˆ˜βŠ‡ : βˆ€ {X} β†’ {Ξ Ξžβ€² : List X}
              β†’ (Ξ· : Ξžβ€² βŠ‡ Ξ)
              β†’ Ξ· βˆ˜βŠ‡ idβŠ‡ ≑ Ξ·
ridβˆ˜βŠ‡ Ξ· = uniqβŠ‡ (Ξ· βˆ˜βŠ‡ idβŠ‡) Ξ·

assocβˆ˜βŠ‡ : βˆ€ {X} β†’ {Ξ Ξžβ€² Ξžβ€³ Ξžβ€΄ : List X}
                β†’ (η₁ : Ξžβ€² βŠ‡ Ξ) (Ξ·β‚‚ : Ξžβ€³ βŠ‡ Ξžβ€²) (η₃ : Ξžβ€΄ βŠ‡ Ξžβ€³)
                β†’ (η₁ βˆ˜βŠ‡ Ξ·β‚‚) βˆ˜βŠ‡ η₃ ≑ η₁ βˆ˜βŠ‡ (Ξ·β‚‚ βˆ˜βŠ‡ η₃)
assocβˆ˜βŠ‡ η₁ Ξ·β‚‚ η₃ = uniqβŠ‡ ((η₁ βˆ˜βŠ‡ Ξ·β‚‚) βˆ˜βŠ‡ η₃) (η₁ βˆ˜βŠ‡ (Ξ·β‚‚ βˆ˜βŠ‡ η₃))


instance
  π‘πžπ§ : βˆ€ {𝔄} β†’ Category (List 𝔄) _βŠ‡_
  π‘πžπ§ = record
          { id     = idβŠ‡
          ; _∘_    = _βˆ˜βŠ‡_
          ; lid∘   = lidβˆ˜βŠ‡
          ; rid∘   = ridβˆ˜βŠ‡
          ; assoc∘ = assocβˆ˜βŠ‡
          }


--------------------------------------------------------------------------------


data All {𝔄} (𝔓 : 𝔄 β†’ Set) : List 𝔄 β†’ Set
  where
    βˆ™ : All 𝔓 βˆ™

    _,_ : βˆ€ {Ξ A x} β†’ All 𝔓 Ξ β†’ 𝔓 A β†’ {{_ : T (fresh x Ξ)}}
                    β†’ All 𝔓 (Ξ , x ⦂ A)


get : βˆ€ {𝔄 𝔓 A x} β†’ {Ξ : List 𝔄}
                  β†’ All 𝔓 Ξ β†’ Ξ βˆ‹ x ⦂ A
                  β†’ 𝔓 A
get (ΞΎ , a) zero    = a
get (ΞΎ , b) (suc i) = get ΞΎ i


maps : βˆ€ {𝔄 𝔓 𝔔} β†’ {Ξ : List 𝔄}
                 β†’ (βˆ€ {A} β†’ 𝔓 A β†’ 𝔔 A) β†’ All 𝔓 Ξ
                 β†’ All 𝔔 Ξ
maps 𝔣 βˆ™       = βˆ™
maps 𝔣 (ΞΎ , a) = maps 𝔣 ΞΎ , 𝔣 a


--------------------------------------------------------------------------------