TwoVecs.agda

open import Data.Unit.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Vec

{-# TERMINATING #-}  -- Lie.
fix : ∀ {α} {A : Set α} -> (A -> A) -> A
fix f = f (fix f)

{-# NO_POSITIVITY_CHECK #-}
data Fix {α β} {A : Set α} (F : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  Wrap : F (Fix F) x -> Fix F x

VecF : Set -> (ℕ -> Set) -> ℕ -> Set
VecF A R  0      = ⊤
VecF A R (suc n) = A × R n

DataVec : Set -> ℕ -> Set
DataVec A = Fix (VecF A)

CompVec : Set -> ℕ -> Set
CompVec A = fix (VecF A)

compToData : ∀ {n A} -> CompVec A n -> DataVec A n
compToData {0}      tt      = Wrap tt
compToData {suc n} (x , xs) = Wrap (x , compToData xs)

dataToComp : ∀ {n A} -> DataVec A n -> CompVec A n
dataToComp {0}     (Wrap tt)       = tt
dataToComp {suc n} (Wrap (x , xs)) = x , dataToComp xs