{-# OPTIONS --rewriting --prop #-}
module Lib where

open import Agda.Primitive

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

postulate
  cheat : ∀ {i} {A : Set i} → A
  cheatP : ∀ {i} {A : Prop i} → A

record Lift {i j} (A : Set i) : Set (i ⊔ j) where
  constructor lift
  field lower : A
open Lift public

record LiftP {i j} (A : Prop i) : Prop (i ⊔ j) where
  constructor lift
  field lower : A
open LiftP public

record LiftPS {i j} (A : Prop i) : Set (i ⊔ j) where
  constructor lift
  field lower : A
open LiftPS public

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

record ⊤p {j} : Prop j 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

-- Propositional truncation to strict Prop
data ∥_∥ {i} (A : Set i) : Prop i where
  ∣_∣ : A → ∥ A ∥

∥-∥-out : ∀ {i} {A : Prop i} → ∥ LiftPS {i} {i} A ∥ → A
∥-∥-out ∣ x ∣ = lower x

∥-∥-ap : ∀ {i j} {A : Set i} {B : Set j} → (A → B) → ∥ A ∥ → ∥ B ∥
∥-∥-ap f ∣ x ∣ = ∣ f x ∣

∥-∥-bind : ∀ {i j} {A : Set i} {B : Set j} → ∥ A ∥ → (A → ∥ B ∥) → ∥ B ∥
∥-∥-bind ∣ x ∣ f = f x

∥-∥-elim : ∀ {i j} {A : Set i} (x : ∥ A ∥) {B : ∥ A ∥ → Prop j} → (∀ a → B ∣ a ∣) → B x
∥-∥-elim ∣ x ∣ f = f x

∥-∥-rec : ∀ {i j} {A : Set i} (x : ∥ A ∥) {B : Prop j} → (A → B) → B
∥-∥-rec ∣ x ∣ f = f x

-- 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 _≡_ #-}
{-# BUILTIN REWRITE _≡_ #-}


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


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
    funext♭  : ∀ {@♭ i} {j} {@♭ A : Set i} {B : @♭ A → Set j} {f g : (@♭ a : A) → B a} → ((@♭ a : A) → f a ≡ g a) → f ≡ g

  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

-- 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)

--

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


-- Natural numbers

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

--

record Iso {i} {j} (A : Set i) (B : Set j) : Set (i ⊔ j) where
  field
    f : A → B
    g : B → A
    fg : ∀ {a} → g (f a) ≡ a
    gf : ∀ {b} → f (g b) ≡ b

Iso-refl : ∀ {i} {A : Set i} → Iso A A
Iso.f Iso-refl x = x
Iso.g Iso-refl x = x
Iso.fg Iso-refl = refl
Iso.gf Iso-refl = refl

Iso-sym : ∀ {i j} {A : Set i} {B : Set j} → Iso A B → Iso B A
Iso.f (Iso-sym f) = f .Iso.g
Iso.g (Iso-sym f) = f .Iso.f
Iso.fg (Iso-sym f) = f .Iso.gf
Iso.gf (Iso-sym f) = f .Iso.fg

Iso-trans : ∀ {ia ib ic} {A : Set ia} {B : Set ib} {C : Set ic} → Iso A B → Iso B C → Iso A C
Iso.f (Iso-trans f g) x = g .Iso.f (f .Iso.f x)
Iso.g (Iso-trans f g) x = f .Iso.g (g .Iso.g x)
Iso.fg (Iso-trans f g) {a} = L.ap (f .Iso.g) (g .Iso.fg) L.∙ f .Iso.fg
Iso.gf (Iso-trans f g) {b} = L.ap (g .Iso.f) (f .Iso.gf) L.∙ g .Iso.gf