module Container.Directed where

open import Prelude
open import Container

record Directed  (π’ž : Container ) : Type where
  S = fst π’ž
  P = snd π’ž
  field
    _↓_ : βˆ€ s β†’ P s β†’ S
    ⊚ : {s : S} β†’ P s
    _βŠ•_ : {s : S} β†’ (p : P s) β†’ P (s ↓ p) β†’ P s

    ↓id : βˆ€ s β†’ s ↓ ⊚ ≑ s
    lassoc : βˆ€ x y z β†’ x ↓ (y βŠ• z) ≑ (x ↓ y) ↓ z
    βŠ•idΚ³ : βˆ€ {s} (x : P s) β†’ x βŠ• ⊚ ≑ x
    βŠ•idΛ‘ : βˆ€ {s} x β†’ ⊚ βŠ• x ≑[ i ≔ P (↓id s (~ i)) ]≑ x
    rassoc :
      βˆ€ {s} (x : P s) (y : P (s ↓ x)) β†’ 
        (Ξ» z β†’ (x βŠ• y) βŠ• z) ≑[ i ≔ (P (lassoc s x y i) β†’ P s) ]≑ (Ξ» z β†’ x βŠ• (y βŠ• z))

open Directed public

DCont : Type₁
DCont = Ξ£ Container Directed

open import Data.Fin

NEList : Container
NEList .fst = β„•
NEList .snd n = Fin (suc n)

mutual
  _β‡Šβ€²_ : βˆ€ s β†’ Fin s β†’ β„•
  suc s β‡Šβ€² x = s β‡Š x

  _β‡Š_ : βˆ€ s β†’ Fin (suc s) β†’ β„•
  s β‡Š f0 = s
  s β‡Š fs x = s β‡Šβ€² x

_βŠ•βŠ•_ : βˆ€ {s} β†’ (p : Fin (suc s)) β†’ Fin (suc (s β‡Š p)) β†’ Fin (suc s)
_βŠ•βŠ•_ {s} f0 y = y
_βŠ•βŠ•_ {suc s} (fs x) y = fs (x βŠ•βŠ• y)

-- NEList⋆ : DCont β„“zero β„“zero
-- NEList⋆ .fst = NEList
-- NEList⋆ .snd ._↓_ = _β‡Š_
-- NEList⋆ .snd .⊚ = f0
-- NEList⋆ .snd ._βŠ•_ = _βŠ•βŠ•_
-- NEList⋆ .snd .↓id _ = refl
-- NEList⋆ .snd .lassoc = {!!}
-- NEList⋆ .snd .βŠ•idΚ³ = {!!}
-- NEList⋆ .snd .βŠ•idΛ‘ _ = refl
-- NEList⋆ .snd .rassoc = {!!}