module Axioms where

open import Prelude public

----------------------------------------------------------------------
-- Propositional extensionality
----------------------------------------------------------------------
postulate
  propext :
    {l : Level}
    {P Q : Prop l}
    → --------------
    (P ↔ Q) → P ≡ Q

----------------------------------------------------------------------
-- Hofmann-style quotient types, using heterogeneous equality
----------------------------------------------------------------------
module quot where
  -- implemented via postulates and rewriting
  postulate
    ty :
      {l m : Level}
      {A : Set l}
      (R : A → A → Prop m)
      → ------------------
      Set l
    mk :
      {l m : Level}
      {A : Set l}
      (R : A → A → Prop m)
      → ------------------
      A → ty R
    eq :
      {l m : Level}
      {A : Set l}
      (R : A → A → Prop m)
      {x y : A}
      → ----------------------
      R x y → mk R x ≡ mk R y
    elim :
      {l m : Level}
      {A : Set l}
      (R : A → A → Prop m)
      {n : Level}
      (B : ty R → Set n)
      (f : ∀ x → B (mk R x))
      (_ : ∀ {x y} → R x y → f x ≣ f y)
      → -------------------------------
      ∀ t → B t
    comp :
      {l m : Level}
      {A : Set l}
      (R : A → A → Prop m)
      {n : Level}
      (B : ty R → Set n)
      (f : ∀ x → B (mk R x))
      (e : ∀ {x y} → R x y → f x ≣ f y)
      → -------------------------------
      ∀ x → elim R B f e (mk R x) ≡ f x
  {-# REWRITE comp #-}

  lift :
    {l m : Level}
    {A : Set l}
    {R : A → A → Prop m}
    {n : Level}
    {B : Set n}
    (f : A → B)
    (_ : ∀ {x y} → R x y → f x ≡ f y)
    → -------------------------------
    ty R → B
  lift = elim _ (λ _ → _)

  liftcomp :
    {l m : Level}
    {A : Set l}
    {R : A → A → Prop m}
    {n : Level}
    {B : Set n}
    (f : A → B)
    (e : ∀ {x y} → R x y → f x ≡ f y)
    → -------------------------------
    ∀ x → lift f e (mk R x) ≡ f x
  liftcomp = λ _ _ _ → refl

  ind :
    {l m : Level}
    {A : Set l}
    (R : A → A → Prop m)
    {n : Level}
    (P : ty R → Prop n)
    (f : ∀ x → P (mk R x))
    → --------------------
    ∀ t → P t
  ind R P f t =
    ↓prop (elim R
      (LiftProp ∘ P)
      (λ x → ↑prop (f x))
      (λ r → ≣irrel (ap P (eq R r)))
      t)

  surjectionmk :
    {l m : Level}
    {A : Set l}
    (R : A → A → Prop m)
    → ------------------
    surjection (mk R)
  surjectionmk {A = A} R =
    ind R (λ z → ∃ x ∶ A , mk R x ≡ z) λ x → (∃i x refl)

  -- Function extensionality from quotients
  funext :
    {l m : Level}
    {A : Set l}
    {B : A → Set m}
    {f g : (x : A) → B x}
    (_ : ∀ x → f x ≡ g x)
    → --------------------
    f ≡ g
  funext {A = A} {B} {f} {g} e = ap m (eq 𝕀₂ {x = O} {I} ⊤i)
    where
      data 𝕀 : Set where
        O : 𝕀
        I : 𝕀
      𝕀₂ : 𝕀 → 𝕀 → Prop
      𝕀₂ _ _ = ⊤

      k : (x : A) → 𝕀 → B x
      k x O = f x
      k x I = g x

      l : (x : A)(i j : 𝕀) → 𝕀₂ i j → k x i ≡ k x j
      l x O O _ = refl
      l x O I _ = e x
      l x I O _ = symm (e x)
      l x I I _ = refl

      m : ty 𝕀₂ → (x : A) → B x
      m z x = elim 𝕀₂ (λ _ → B x) (k x) (λ {i} {j} _ → l x i j ⊤i) z

  -- Functions of two quotiented arguments (uses funext)
  lift₂ :
    {l l' m m' : Level}
    {A : Set l}
    {R : A → A → Prop m}
    {B : Set l'}
    {S : B → B → Prop m'}
    {n : Level}
    {C : Set n}
    (f : A → B → C)
    (_ : ∀ {x x' y } → R x x' → f x y ≡ f x' y )
    (_ : ∀ {x y  y'} → S y y' → f x y ≡ f x  y')
    → ------------------------------------------
    ty R → ty S → C
  lift₂ {S = S} f e₁ e₂ =
    lift
      (λ x → lift (λ y → f x y) e₂)
      (λ {x} {x'} r →
      funext (ind S
        (λ z → lift (λ y → f x y) e₂ z ≡ lift (λ y → f x' y) e₂ z)
        (λ _ → e₁ r)))

  ind₂ :
    {l l' m m' : Level}
    {A : Set l}
    (R : A → A → Prop m)
    {B : Set l'}
    (S : B → B → Prop m')
    {n : Level}
    (P : ty R → ty S → Prop n)
    (f : ∀ x y → P (mk R x) (mk S y))
    → -------------------------------
    ∀ r s → P r s
  ind₂ R S P f =
    ind R (λ r → ∀ s → P r s) (λ x →
    ind S (P (mk R x)) (f x))

-- end module quot ---------------------------------------------------

-- Notation for quotients
infix  _/_ [_]/_
_/_ : {l m : Level}(A : Set l)(R : A → A → Prop m) → Set l
A / R = quot.ty R

[_]/_ : {l m : Level}{A : Set l} → A → (R : A → A → Prop m) → A / R
[ x ]/ R = quot.mk R x

-- Effectiveness of quotients:
-- for all x y : A, if [ x ]/ R ≡ [ y ]/ R, then x and y are related
-- by the equivalence relation generated by R, and hence by any
-- equivalence relation containing R.
quot-eff :
  {l      : Level}
  {A      : Set l}
  (R S    : A → A → Prop l)
  (R⊆S    : ∀{x y} → R x y → S x y)
  (Srefl  : ∀{x y} → x ≡ y → S x y)
  (Ssymm  : ∀{x y} → S x y → S y x)
  (Strans : ∀{x y z} → S y z → S x y → S x z)
  → -----------------------------------------
  ∀{x y} → [ x ]/ R ≡ [ y ]/ R → S x y
quot-eff {l} {A} R S R⊆S Srefl Ssymm Strans p = r p
  where
  f : ∀{x x' y} → R x x' → S x y ≡ S x' y
  f p = propext  -- Propositional Extensionality used here
    (∧i (λ q → Strans q (Ssymm (R⊆S p))) (λ q → Strans q (R⊆S p)))

  g : ∀{x y y'} → R y y' → S x y ≡ S x y'
  g p = propext -- Propositional Extensionality used here
    (∧i (λ q → Strans (R⊆S p) q) (λ q → Strans (Ssymm (R⊆S p)) q))

  S' : A / R  → A / R → Prop l
  S' = quot.lift₂ S f g

  r : {z z' : A / R} → z ≡ z' → S' z z'
  r {z} refl =
    quot.ind R (λ z → S' z z) (λ _ → Srefl refl) z

----------------------------------------------------------------------
-- Function Extensionality, derived from quotients
----------------------------------------------------------------------
funext :
  {l m : Level}
  {A : Set l}
  {B : A → Set m}
  {f g : (x : A) → B x}
  (_ : ∀ x → f x ≡ g x)
  → --------------------
  f ≡ g
funext = quot.funext

funexp :
  {l m : Level}
  {A : Prop l}
  {B : A → Set m}
  {f g : (x : A) → B x}
  (_ : ∀ x → f x ≡ g x)
  → -------------------
  f ≡ g
funexp {A = A} {B} {f} {g} e = ap f=g (eq O=I {x = O} {I} ⊤i)
  where
  open quot
  data 𝕀 : Set where
    O : 𝕀
    I : 𝕀

  O=I : 𝕀 → 𝕀 → Prop
  O=I _ _ = ⊤

  fg : (x : A) → 𝕀 → B x
  fg x O = f x
  fg x I = g x

  h : (x : A)(i j : 𝕀) → O=I i j → fg x i ≡ fg x j
  h x O O _ = refl
  h x O I _ = e x
  h x I O _ = symm (e x)
  h x I I _ = refl

  f=g : ty O=I → (x : A) → B x
  f=g z x =
    elim O=I (λ _ → B x) (fg x) (λ {i} {j} _ → h x i j ⊤i) z

heq-funext :
  {l m : Level}
  {A A' : Set l}
  {B : A → Set m}
  {B' : A' → Set m}
  {f : (x : A) → B x}
  {f' : (x : A') → B' x}
  (_ : A ≡ A')
  (_ : ∀{x x'} → x ≣ x' → f x ≣ f' x')
  → ----------------------------------
  f ≣ f'
heq-funext refl e with funext (λ x → (≣typ (e{x}{x} refl)))
... | refl = funext λ x → e{x}{x} refl

heq-funexp :
  {l m : Level}
  {A : Prop l}
  {B C : Set m}
  {f : A → B}
  {g : A → C}
  (_ : B ≡ C)
  (_ : ∀ x → f x ≣ g x)
  → -------------------
  f ≣ g
heq-funexp refl e' = funexp e'

heq-funexp' :
  {l m : Level}
  {A B : Prop l}
  {C : Set m}
  {f : A → C}
  {g : B → C}
  (_ : A ≡ B)
  (_ : ∀ x y → f x ≣ g y)
  → ---------------------
  f ≣ g
heq-funexp' refl e = funexp λ x → e x x


--  Function extensionality with implicit arguments
implicit-funext :
  {l m : Level}
  {A : Set l}
  {B : A → Set m}
  {f g : {x : A} → B x}
  (_ : ∀ x → f {x} ≡ g {x})
  → -----------------------------
  (λ{x} → f {x}) ≡ (λ{x} → g {x})
implicit-funext {A = A} {B} {f} {g} e =
  ap impl (funext {f = λ x → f{x}} {g = λ x → g{x}} e)
  where
  impl : ((x : A) → B x) → {x : A} → B x
  impl f {x} = f x

--  Function extensionality with implicit arguments
instance-funext :
  {l m : Level}
  {A : Set l}
  {B : A → Set m}
  {f g : {{x : A}} → B x}
  (_ : ∀ x → f {{x}} ≡ g {{x}})
  → -------------------------------------
  (λ{{x}} → f {{x}}) ≡ (λ{{x}} → g {{x}})
instance-funext {A = A} {B} {f} {g} e =
  ap sett (funext {f = λ x → f{{x}}} {g = λ x → g{{x}}} e)
  where
  sett : ((x : A) → B x) → {{x : A}} → B x
  sett f {{x}} = f x

instance-funexp :
  {l m : Level}
  {A : Prop l}
  {B : A → Set m}
  {f g : {{x : A}} → B x}
  (_ : ∀ x → f {{x}} ≡ g {{x}})
  → -------------------------------------
  (λ{{x}} → f {{x}}) ≡ (λ{{x}} → g {{x}})
instance-funexp {A = A} {B} {f} {g} e =
  ap sett (funexp {f = λ x → f{{x}}} {g = λ x → g{{x}}} e)
  where
  sett : ((x : A) → B x) → {{x : A}} → B x
  sett f {{x}} = f x

----------------------------------------------------------------------
-- The Axiom of Unique Choice
----------------------------------------------------------------------
postulate
  A!C : {l : Level}{A : Set l} → (∃ x ∶ A , ∀(x' : A) → x ≡ x') → A

-- Definite description
module _
  {l m : Level}
  (A : Set l)
  (P : A → Prop m)
  where
  private
    AP : Set (l ⊔ m)
    AP = set A P

    ∃!AP : ∃! A P → ∃ z ∶ AP , ∀(z' : AP) → z ≡ z'
    ∃!AP (∃i x (∧i p q)) =
      ∃i (x ∣ p) λ{(x' ∣ p') → setext (q x' p')}

  the : {{∃! A P}} → A
  the {{u}} = el (A!C (∃!AP u))

  the-pf : {{_ : ∃! A P}} → P the
  the-pf {{u}} = pf (A!C (∃!AP u))

  the-uniq : {{_ : ∃! A P}}(x : A) → P x → the ≡ x
  the-uniq {{∃i x' (∧i p' q)}} x p =
    let
      instance
        _ : ∃! A P
        _ = ∃i x' (∧i p' q)
    in
    -- proof
    --   the
    -- =[ symm (q the the-pf) ]
    --   x'
    -- =[ q x p ]
    --   x
    -- qed
    symm (q the the-pf) ； q x p

  syntax the A (λ x → P) = the x ∶ A , P

-- Transport along a propositional equality between types
coe :
  {l : Level}
  {A B : Set l}
  → ------------
  A ≡ B → A → B
coe {A = A} {B} e x = the B (_≣ x) {{coe! e}}
  module _ where
  coe! : A ≡ B → ∃! y ∶ B , y ≣ x
  coe! refl = ∃i x (∧i refl λ _ p → symm p)

coerefl :
  {l : Level}
  {A : Set l}
  (x : A)
  → ------------
  coe refl x ≡ x
coerefl x = the-pf _ (_≣ x) {{coe! refl x refl}}

coe≣ :
  {l : Level}
  {A A' : Set l}
  (e : A ≡ A')
  (x : A)
  → ------------
  coe e x ≣ x
coe≣ refl x = coerefl x

coe⁻¹ :
  {l : Level}
  {A B : Set l}
  → -----------
  A ≡ B → B → A
coe⁻¹ e = coe (symm e)

coe⁻¹coe :
  {l : Level}
  {A B : Set l}
  (e : A ≡ B)
  {x : A}
  → -------------------
  coe⁻¹ e (coe e x) ≡ x
coe⁻¹coe refl {x} =
  proof
    coe refl (coe refl x)
  =[ coerefl _ ]
    coe refl x
  =[ coerefl _ ]
    x
  qed

coecoe⁻¹ :
  {l : Level}
  {A B : Set l}
  (e : A ≡ B)
  {y : B}
  → -------------------
  coe e (coe⁻¹ e y) ≡ y
coecoe⁻¹ refl {y} =
  proof
    coe refl (coe refl y)
  =[ coerefl _ ]
    coe refl y
  =[ coerefl _ ]
    y
  qed

coe=id :
  {l : Level}
  {A A' : Set l}
  (e : A ≡ A')
  → -------------------
  coe e ≣ λ (x : A) → x
coe=id refl = funext coerefl

∘coe :
  {l m : Level}
  {A A' : Set l}
  {B : Set m}
  (e : A ≡ A')
  (f : A' → B)
  → ------------
  f ∘ coe e ≣ f
∘coe refl f = ap (f ∘_) (coe=id refl)

coe∘ :
  {l m : Level}
  {A  : Set l}
  {B B' : Set m}
  (e : B ≡ B')
  (f : A → B)
  → -----------
  coe e ∘ f ≣ f
coe∘ refl f = ap (_∘ f) (coe=id refl)

subst :
  {l m : Level}
  {A : Set l}
  (B : A → Set m)
  {x x' : A}
  (e : x ≡ x')
  → ------------
  B x → B x'
subst B e = coe (ap B e)

subst≣ :
  {l m : Level}
  {A : Set l}
  (B : A → Set m)
  {x x' : A}
  (e : x ≡ x')
  (y : B x)
  → -------------
  subst B e y ≣ y
subst≣ _ refl = coerefl

substrefl :
  {l m : Level}
  {A : Set l}
  (B : A → Set m)
  {x  : A}
  (y : B x)
  → ----------------
  subst B refl y ≡ y
substrefl _ = coerefl