------------------------------------------------------------------------
-- Lists parameterised on things in Set1
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.List1 where

import Data.List as List
open List using (List; []; _∷_)
open import Data.Nat

infixr 5 _∷_ _++_

data List₁ (a : Set1) : Set1 where
  []  : List₁ a
  _∷_ : (x : a) (xs : List₁ a)  List₁ a

_++_ :  {a}  List₁ a  List₁ a  List₁ a
[]       ++ bs = bs
(a  as) ++ bs = a  (as ++ bs)

map₀₁ :  {a b}  (a  b)  List a  List₁ b
map₀₁ f []       = []
map₀₁ f (x  xs) = f x  map₀₁ f xs

map₁₁ :  {a b}  (a  b)  List₁ a  List₁ b
map₁₁ f []       = []
map₁₁ f (x  xs) = f x  map₁₁ f xs

replicate :  {a}  (n : )  a  List₁ a
replicate zero    x = []
replicate (suc n) x = x  replicate n x

foldr₁₀ : {a : Set1} {b : Set}  (a  b  b)  b  List₁ a  b
foldr₁₀ c n []       = n
foldr₁₀ c n (x  xs) = c x (foldr₁₀ c n xs)

foldr₁₁ : {a b : Set1}  (a  b  b)  b  List₁ a  b
foldr₁₁ c n []       = n
foldr₁₁ c n (x  xs) = c x (foldr₁₁ c n xs)

length :  {A}  List₁ A  
length []       = zero
length (x  xs) = suc (length xs)