{-# 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  _⇔_
_⇔_ = 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  _×_
_×_ : Set a → Set b → Set (a ℓ⊔ b)
A × B = Σ A (const B)

infixr  _∷_
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  _∘_
_∘_ : ∀ {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  _∙_
  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