{-# OPTIONS --without-K --exact-split --rewriting #-}

module Pi.FSMG.M where

open import lib.Base
open import lib.NType
open import lib.PathOver
open import lib.PathGroupoid

open import Pi.FSMG.Paths
open import Pi.Common.Extra

module _ {i} where
  postulate
    M : (A : Type i)  Type i

  module _ {A : Type i} where
    infixr 40 _::_
    postulate
      nil : M A
      _::_ : A  M A  M A

      swap : (x y : A) (xs : M A)  x :: y :: xs == y :: x :: xs

       : (x y z : A) (xs : M A)
         swap x y (z :: xs)  ap (y ::_) (swap x z xs)  swap y z (x :: xs)
        == ap (x ::_) (swap y z xs)  swap x z (y :: xs)  ap (z ::_) (swap x y xs)

      swap² : (x y : A) (xs : M A)  swap x y xs  swap y x xs == idp

      instance trunc : has-level 1 (M A)

    module MElim {j} {P : M A  Type j}
      (nil* : P nil)
      (_::*_ : (x : A) {xs : M A}  (xs* : P xs)  P (x :: xs))
      (swap* : (x y : A) {xs : M A} (xs* : P xs)
              (x ::* (y ::* xs*)) == (y ::* (x ::* xs*)) [ P  swap x y xs ])
      (swap²* : (x y z : A) {xs : M A} (xs* : P xs)
               (swap* x y xs* ∙ᵈ swap* y x xs*) == idp [  p  (x ::* (y ::* xs*)) == (x ::* (y ::* xs*)) [ P  p ])  swap² x y xs ])
      (⬡* : (x y z : A) {xs : M A} (xs* : P xs)
           let p1 = swap* x y (z ::* xs*) ∙ᵈ ($ (y ::*_) (swap* x z xs*) ∙ᵈ swap* y z (x ::* xs*)) in
            let p2 = ($ (x ::*_) (swap* y z xs*) ∙ᵈ (swap* x z (y ::* xs*) ∙ᵈ $ (z ::*_) (swap* x y xs*))) in
            p1 == p2 [  p  (x ::* (y ::* (z ::* xs*))) == (z ::* (y ::* (x ::* xs*))) [ P  p ])   x y z xs ])
      (trunc* : {xs : M A}  has-level 1 (P xs))
      where

      postulate
        f : (xs : M A)  P xs
        f-nil-β : f nil  nil*
        {-# REWRITE f-nil-β #-}
        f-::-β : {x : A} {xs : M A}  f (x :: xs)  (x ::* f xs)
        {-# REWRITE f-::-β #-}

      postulate
        f-swap-β : {x y : A} {xs : M A}  apd f (swap x y xs) == swap* x y (f xs)

    module MRec {j} {P : Type j}
      (nil* : P)
      (_::*_ : (x : A)  P  P)
      (swap* : (x y : A) (xs* : P)
              (x ::* (y ::* xs*)) == (y ::* (x ::* xs*)))
      (swap²* : (x y z : A) (xs* : P)
               (swap* x y xs*  swap* y x xs*) == idp)
      (⬡* : (x y z : A) (xs* : P)
           let p1 = swap* x y (z ::* xs*)  (ap (y ::*_) (swap* x z xs*)  swap* y z (x ::* xs*)) in
            let p2 = (ap (x ::*_) (swap* y z xs*)  (swap* x z (y ::* xs*)  ap (z ::*_) (swap* x y xs*))) in
            p1 == p2)
      (trunc* : has-level 1 P)
      where

      f : M A  P
      f = MElim.f {P = λ _  P} nil*  x p  x ::* p)  x y {xs} xs*  ↓-cst-in (swap* x y xs*)) TODO TODO trunc*