Prelude.agda

module Prelude where
  open import Agda.Primitive using (Level; lzero; lsuc)
    renaming (_⊔_ to lmax) public
  
  -- empty type
  data ⊥ : Set where

  -- from false, derive whatever
  abort : ∀ {C : Set} → ⊥ → C
  abort ()

  -- unit
  data ⊤ : Set where
    <> : ⊤

  -- sums
  infixr 1 _+_
  data _+_ (A B : Set) : Set where
    Inl : A → A + B
    Inr : B → A + B

  -- pairs
  infixr 4 _,_
  record Σ {l1 l2 : Level} (A : Set l1) (B : A → Set l2) : Set (lmax l1 l2) where
    constructor _,_
    field
      π1 : A
      π2 : B π1
  open Σ public

  -- Sigma types, or dependent pairs, with nice notation.
  infix 2 Σ
  syntax Σ A (\ x -> B) = Σ[ x ∈ A ] B

  -- non-dependent pairs
  infixr 2 _×_
  _×_ : {l1 : Level} {l2 : Level} → (Set l1) → (Set l2) → Set (lmax l1 l2)
  A × B = Σ A λ _ → B

  -- currying and uncurrying
  curry : ∀{a b c : Level} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
          ((p : Σ A B) → C p) →
          ((x : A) → (y : B x) → C (x , y))
  curry f x y = f (x , y)

  uncurry : ∀{a b c : Level} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
            ((x : A) → (y : B x) → C (x , y)) →
            ((p : Σ A B) → C p)
  uncurry f (x , y) = f x y
  
  -- equality
  infix 4 _==_
  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    refl : M == M
  {-# BUILTIN EQUALITY _==_ #-}

  -- disequality
  infix 4 _≠_
  _≠_ : {l : Level} {A : Set l} → (a b : A) → Set l
  a ≠ b = (a == b) → ⊥

  -- transitivity of equality
  _·_ : {l : Level} {α : Set l} {x y z : α} → x == y → y == z → x == z
  refl · refl = refl

  -- symmetry of equality
  ! : {l : Level} {α : Set l} {x y : α} → x == y → y == x
  ! refl = refl

  -- ap, in the sense of HoTT, that all functions respect equality in their
  -- arguments. named in a slightly non-standard way to avoid naming
  -- clashes with hazelnut constructors.
  ap1 : {l1 l2 : Level} {α : Set l1} {β : Set l2} {x y : α}
        (F : α → β) →
        x == y →
        F x == F y
  ap1 F refl = refl

  -- transport, in the sense of HoTT, that fibrations respect equality
  tr : {l1 l2 : Level} {α : Set l1} {x y : α}
       (B : α → Set l2) →
       x == y →
       B x →
       B y
  tr B refl x₁ = x₁

  -- options
  data Maybe (A : Set) : Set where
    Some : A → Maybe A
    None : Maybe A
  {-# BUILTIN MAYBE Maybe #-}
  
  -- the some constructor is injective
  some-inj : {A : Set} {x y : A} → Some x == Some y → x == y
  some-inj refl = refl

  -- some is not none
  some-not-none : {A : Set} {x : A} → Some x == None → ⊥
  some-not-none ()

  -- function extensionality.
  -- used to reason about contexts as finite functions
  postulate
     funext : {A : Set} {B : A → Set} {f g : (x : A) → (B x)} →
              ((x : A) → f x == g x) → f == g

  -- non-equality is commutative
  flip : {A : Set} {x y : A} → 
         (x == y → ⊥) →
         (y == x → ⊥)
  flip neq eq = neq (! eq)

  contra : {A : Set} → A → (A → ⊥) → ⊥
  contra a ¬a = ¬a a