{-# OPTIONS --type-in-type #-}

open import Cubical.Foundations.Prelude hiding (empty)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence

open import Cubical.Data.List
open import Cubical.Data.Sigma hiding (empty)


module Queue.Base
  (ABS : Type) (ABS-isProp : isProp ABS)
  (E : Type) (e₀ : E) (ESet : isSet E) where

open import Modality.Abstract ABS ABS-isProp


record PreQueue : Type₁ where
  field
    X : Type
    empty : X
    enqueue : E → X → X
    dequeue : X → E × X
open PreQueue public

prequeue-path
  : ∀ {P Q : PreQueue} (P≃Q : P .X ≃ Q .X)
  → (equivFun P≃Q (P .empty) ≡ Q .empty)
  → (∀ e p → equivFun P≃Q (P .enqueue e p) ≡ Q .enqueue e (equivFun P≃Q p))
  → (∀ p → fst (P .dequeue p) ≡ fst (Q .dequeue (equivFun P≃Q p)))
  → (∀ p → equivFun P≃Q (snd (P .dequeue p)) ≡ snd (Q .dequeue (equivFun P≃Q p)))
  → P ≡ Q
prequeue-path P≃Q _ _ _ _ i .X = ua P≃Q i
prequeue-path P≃Q h-empty _ _ _ i .empty = ua-gluePath P≃Q h-empty i
prequeue-path {P} {Q} P≃Q _ h-enqueue _ _ i .enqueue e = ua→ {e = P≃Q} {f₁ = Q .enqueue e} (ua-gluePath P≃Q ∘ h-enqueue e) i
prequeue-path {P} {Q} P≃Q _ _ h-fst-dequeue _ i .dequeue p .fst = ua→ {e = P≃Q} {f₁ = fst ∘ Q .dequeue} h-fst-dequeue i p
prequeue-path {P} {Q} P≃Q _ _ _ h-snd-dequeue i .dequeue p .snd = ua→ {e = P≃Q} {f₁ = snd ∘ Q .dequeue} (ua-gluePath P≃Q ∘ h-snd-dequeue) i p

listPreQueue : PreQueue
listPreQueue .X = List E
listPreQueue .empty = []
listPreQueue .enqueue e l = l ++ [ e ]
listPreQueue .dequeue [] = e₀ , []
listPreQueue .dequeue (e ∷ l) = e , l

Queue : Type
Queue = spec listPreQueue

queue-isConcrete : isConcrete Queue
queue-isConcrete = isConcreteSpec listPreQueue

listQueue : Queue
listQueue .fst = listPreQueue
listQueue .snd = η∘ refl