module Lib where

open import Agda.Primitive

infixr  _,_
infixr  _×_
infixr  _⊎_

-- Unit type
record ⊤ : Set where
  constructor tt
open ⊤ public

record ⊤p : Prop where
  constructor tt
open ⊤p public

-- Σ-types
record Σ {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
  constructor _,_
  field fst : A
        snd : B fst
open Σ public

_×_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A × B = Σ A λ _ → B

record ΣP {i j} (A : Prop i) (B : A → Prop j) : Prop (i ⊔ j) where
  constructor _,_
  field fst : A
        snd : B fst
open ΣP public

record ΣPS {i j} (A : Set i) (B : A → Prop j) : Set (i ⊔ j) where
  constructor _,_
  field fst : A
        snd : B fst
open ΣPS public

-- Coproducts
data _⊎_ {i j} (A : Set i) (B : Set j) : Set (i ⊔ j) where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- Identity types, with UIP and funext
data _≡_ {i} {A : Set i} (x : A) : (y : A) → Set i where
  refl : x ≡ x
infix  _≡_

{-# BUILTIN EQUALITY _≡_ #-}

module L where
  happly : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a} → f ≡ g → (a : A) → f a ≡ g a
  happly refl a = refl

  postulate
    funext : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a} → ((a : A) → f a ≡ g a) → f ≡ g
    funext-β : ∀ {i j} {A : Set i} {B : A → Set j} {f} → funext {i} {j} {A} {B} {f = f} {g = f} (λ a → refl) ≡ refl

  uip : ∀ {i} {A : Set i} {x : A} {y : A} {p q : x ≡ y} → p ≡ q
  uip {p = refl} {refl} = refl

  ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
  ap f refl = refl

  transp : ∀ {i j} {A : Set i} (B : A → Set j) {x y : A} → x ≡ y → B x → B y
  transp B refl x = x

  ! : ∀ {i} {A : Set i} {x : A} {y : A} → x ≡ y → y ≡ x
  ! refl = refl

  _∙_ : ∀ {i} {A : Set i} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  refl ∙ refl = refl
  infixl  _∙_

  _≡[_]≡_ : ∀ {i} {A B : Set i} → A → A ≡ B → B → Set i
  x ≡[ refl ]≡ y = x ≡ y
  infix  _≡[_]≡_

  uip-≡ : ∀ {i} {A B : Set i} {x : A} {y : B} {p q : A ≡ B} → x ≡[ p ]≡ y → x ≡[ q ]≡ y
  uip-≡ {i} {A} {B} {x} {y} {p} {q} e rewrite uip {p = p} {q = q} = e

postulate
  propext : ∀ {i} {P Q : Prop i} → (P → Q) → (Q → P) → P ≡ Q

-- Function composition

_∘_ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k}
      → (f : ∀ {a} → (b : B a) → C a b)
      → (g : (a : A) → B a)
      → (a : A) → C a (g a)
(f ∘ g) x = f (g x)

-- Misc

fiber : ∀ {i j} {A : Set i} {B : Set j} → (A → B) → B → Set (i ⊔ j)
fiber f b = Σ _ λ a → f a ≡ b

is-contr : ∀ {i} (A : Set i) → Set i
is-contr A = Σ A λ x → ∀ y → y ≡ x

is-prop : ∀ {i} (A : Set i) → Set i
is-prop A = ∀ (x y : A) → x ≡ y

record is-iso {i j} {A : Set i} {B : Set j} (f : A → B) : Set (i ⊔ j) where
  field
    is-iso-inv : B → A
    is-iso-β : ∀ a → is-iso-inv (f a) ≡ a
    is-iso-η : ∀ b → f (is-iso-inv b) ≡ b
open is-iso public

-- Natural numbers

data ℕ : Set₀ where
  zero : ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}