{-# OPTIONS --cubical --safe #-}

module Prelude where

open import Agda.Primitive using (Level; lsuc; lzero) renaming (_⊔_ to _ℓ⊔_) public
open import Cubical.Foundations.Prelude as Cubical hiding (I) renaming (_∙_ to _;_) public
open import Agda.Builtin.Nat renaming (Nat to ) public
open import Cubical.Foundations.Isomorphism public
open import Cubical.Foundations.Everything using (fiber) public

infix 4 _⇔_
_⇔_ = Iso
open Iso public

variable
  a b c : Level
  A : Set a
  B : Set b
  C : Set c
  n m : 

const : A  B  A
const x _ = x

open import Agda.Builtin.Sigma public

infixr 4 _×_
_×_ : Set a  Set b  Set (a ℓ⊔ b)
A × B = Σ A (const B)

infixr 5 _∷_
data List (A : Set a) : Set a where
  [] : List A
  _∷_ : A  List A  List A

foldr : (A  B  B)  B  List A  B
foldr f b [] = b
foldr f b (x  xs) = f x (foldr f b xs)

infixr 9 _∘_
_∘_ :  {A : Type a} {B : A  Type b} {C : {x : A}  B x  Type c} 
        (∀ {x} (y : B x)  C y)  (g : (x : A)  B x) 
        ((x : A)  C (g x))
f  g = λ x  f (g x)

record Monoid  : Set (lsuc ) where
  infixl 7 _∙_
  field
    𝑆 : Set 
    _∙_ : 𝑆  𝑆  𝑆
    ε : 𝑆
    ε∙ :  x  ε  x  x
    ∙ε :  x  x  ε  x
    assoc :  x y z  (x  y)  z  x  (y  z)

data Bool : Set where
  false : Bool
  true : Bool

bool : A  A  Bool  A
bool f t false = f
bool f t true  = t