{-# OPTIONS --cubical --postfix-projections #-}

open import Prelude
open import Algebra
open import Container

module Control.Monad.ListT
  (𝔽 : Container)
  (is-mon : Monad  ⟦ 𝔽 ⟧)
  where

open Monad {β„“β‚‚ = β„“zero} is-mon

postulate
  cmap-return : (f : A β†’ B) (x : ⟦ 𝔽 ⟧ A) β†’
                (cmap f x ≑ (x >>= return ∘ f))


infixr 5 _∷_
mutual
  List : Type β†’ Type
  List A = ⟦ 𝔽 ⟧ (Cons A)

  data Cons (A : Type) : Type where
    []  : Cons A
    _∷_ : (x : A) β†’ (xs : List A) β†’ Cons A

data ℭ𝔬𝔫𝔰 (A : Type) (P : List A β†’ Type) : Type where
  [] : ℭ𝔬𝔫𝔰 A P
  _∷_⟨_⟩ : (x : A) β†’ (xs : List A) β†’ (P⟨xs⟩ : P xs) β†’ ℭ𝔬𝔫𝔰 A P

module _ {A : Type} (P : List A β†’ Type) where
  wrapc : ℭ𝔬𝔫𝔰 A P β†’ Cons A
  wrapc [] = []
  wrapc (x ∷ xs ⟨ P⟨xs⟩ ⟩) = x ∷ xs

  wrap : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P) β†’ List A
  wrap = cmap wrapc
  {-# INLINE wrap #-}

  -- module _ (ψ : (x : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) β†’ P (wrap x)) where
  --   elim : (x : List A) β†’ P x
  --   elim (n , k) = {!!}

    -- elimc : Cons A β†’ ℭ𝔬𝔫𝔰 A P

    -- wrapc-elimc : (c : Cons A) β†’ wrapc (elimc c) ≑ c

    -- wrapc-elimc []       i = []
    -- wrapc-elimc (x ∷ xs) i = x ∷ xs

    -- elimc [] = []
    -- elimc (x ∷ xs) = x ∷ xs ⟨ elim xs ⟩

    -- elim xs =
    --   subst
    --     P
    --     (cong (xs .fst ,_) (funExt (Ξ» x β†’ wrapc-elimc (xs .snd x))))
    --     (ψ (cmap elimc xs))

-- module _  (Ο• : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const B)) β†’ B) where
--   para : List A β†’ B
--   parac : Cons A β†’ ℭ𝔬𝔫𝔰 A (const B)


--   para xs = Ο• (cmap parac xs)

--   parac [] = []
--   parac (x ∷ xs) = x ∷ xs ⟨ para xs ⟩

-- ++-Ο• : List A β†’ ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const (List A))) β†’ List A
-- ++-Ο• ys xs = xs >>= Ξ» { [] β†’ ys ; (x ∷ _ ⟨ xs ⟩) β†’ return (x ∷ xs) }

-- infixr 5 _++_
-- _++_ : List A β†’ List A β†’ List A
-- xs ++ ys = para (++-Ο• ys) xs

-- cmap-comp : (f : B β†’ C) (g : A β†’ B) (x : ⟦ 𝔽 ⟧ A) β†’ cmap f (cmap g x) ≑ cmap (f ∘ g) x
-- cmap-comp f g x = refl

-- cmap-id : (x : ⟦ 𝔽 ⟧ A) β†’ cmap id x ≑ x
-- cmap-id x = refl

-- open import Path.Reasoning

-- ++-id : (xs : List A) β†’ xs ++ return [] ≑ xs
-- ++-id {A = A} = elim P ψ
--   where
--   P : List A β†’ Type
--   P xs = xs ++ return [] ≑ xs

--   Ο• : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const (List A))) β†’ List A
--   Ο• = ++-Ο• (return [])

--   Ο•β€² : ℭ𝔬𝔫𝔰 A (const (List A)) β†’ Cons A
--   Ο•β€² [] = []
--   Ο•β€² (x ∷ xs ⟨ P⟨xs⟩ ⟩) = x ∷ P⟨xs⟩

--   ϕ≑ : βˆ€ xs β†’ Ο• xs ≑ (xs >>= return βˆ˜β€² Ο•β€²)
--   ϕ≑ xs = cong (xs >>=_) (funExt (Ξ» { [] β†’ refl ; (x ∷ xs ⟨ P⟨xs⟩ ⟩) β†’ refl }))

--   lemma : (xs : ℭ𝔬𝔫𝔰 A P) β†’ Ο•β€² (parac Ο• (wrapc P xs)) ≑ wrapc P xs
--   lemma [] = refl
--   lemma (x ∷ xs ⟨ P⟨xs⟩ ⟩) = cong (x ∷_) P⟨xs⟩

--   ψ : (xs : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) β†’ P (wrap P xs)
--   ψ xs =
--     wrap P xs ++ return [] β‰‘βŸ¨βŸ©
--     para Ο• (wrap P xs) β‰‘βŸ¨βŸ©
--     Ο• (cmap (parac Ο•) (wrap P xs)) β‰‘βŸ¨ ϕ≑ _ ⟩
--     (cmap (parac Ο•) (wrap P xs) >>= return βˆ˜β€² Ο•β€²) β‰‘Λ˜βŸ¨ cmap-return Ο•β€² _ ⟩
--     cmap Ο•β€² (cmap (parac Ο•) (wrap P xs)) β‰‘βŸ¨βŸ©
--     cmap (Ο•β€² ∘ parac Ο•) (wrap P xs) β‰‘βŸ¨βŸ©
--     cmap (Ο•β€² ∘ parac Ο•) (cmap (wrapc P) xs) β‰‘βŸ¨βŸ©
--     cmap (Ο•β€² ∘ parac Ο• ∘ wrapc P) xs β‰‘βŸ¨ cong (flip cmap xs) (funExt lemma) ⟩
--     wrap P xs ∎


-- -- open import Cubical.Data.Sigma.Properties

-- -- ++-assoc : (xs ys zs : List A) β†’ (xs ++ ys) ++ zs ≑ xs ++ (ys ++ zs)
-- -- ++-assoc {A = A} xs ys zs = elim P ψ xs
-- --   where
-- --   P : List A β†’ Type
-- --   P xsβ€² = (xsβ€² ++ ys) ++ zs ≑ xsβ€² ++ (ys ++ zs)
-- --   {-# INLINE P #-}

-- --   ψ : (x : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) β†’ P (wrap P x)
-- --   ψ xs = Ξ£PathTransportβ†’PathΞ£ _ _ ({!refl!} , {!!})

-- -- _>>=β€²_ : List A β†’ (A β†’ List B) β†’ List B
-- -- _>>=β€²_ {A = A} {B = B} xs k = para Ο• xs
-- --   where
-- --   Ο• : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (List B)) β†’ List B
-- --   Ο• xs = xs >>= Ξ» { [] β†’ return [] ; (x ∷ xs) β†’ k x ++ xs }