{-# OPTIONS --rewriting #-}
module QuotientViaPrimTrustme+Private where

open import Prelude

----------------------------------------------------------------------
-- primTrustMe for Agda v.2.6
----------------------------------------------------------------------
primitive
{- The function primEraseEquality takes a proof of a homogeneous
equality between two values x and y and stays stuck on it until x and
y actually become definitionally equal. Whenever that is the case,
primEraseEquality e reduces to refl. -}
  primEraseEquality :
    {l : Level}
    {A : Set l}
    {x y : A}
    (_ : Id x y)
    → ----------
    Id x y

private
  postulate
    unsafePrimTrustMe :
      {l : Level}
      {A : Set l}
      {x y : A}
      → ---------
      Id x y

primTrustMe :
  {l : Level}
  {A : Set l}
  {x y : A}
  → ---------
  Id x y
primTrustMe = primEraseEquality unsafePrimTrustMe

{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}

----------------------------------------------------------------------
-- Hofmann-style quotient types
----------------------------------------------------------------------
module quot where
  -- implemented via private definitions and primTrustMe
  -- (see https://www.cl.cam.ac.uk/~amp12/agda/quotient.html)
  private
  -- # is used to mark private definitions
    record # {l : Level}(A : Set l) : Set l where
      constructor #in
      field
        #out : A
    open #

  ty :
    {l m : Level}
    {A : Set l}
    (_ : A → A → Set m)
    → -----------------
    Set l
  ty {A = A} _ =  # (𝟙 → # A)

  mk :
    {l m : Level}
    {A : Set l}
    (R : A → A → Set m)
    → -----------------
    A → ty R
  mk _ x = #in (λ _ → #in x)

  eq :
    {l m : Level}
    {A : Set l}
    (R : A → A → Set m)
    {x y : A}
    → ---------------------
    R x y → mk R x ≡ mk R y
  eq _ _ = Id2≡ primTrustMe

  elim :
    {l m : Level}
    {A : Set l}
    (R : A → A → Set 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
  elim _ _ f _ (#in g) = f (#out (g tt))

  comp :
    {l m : Level}
    {A : Set l}
    (R : A → A → Set 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
  comp _ _ _ _ _ = refl

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

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

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

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

  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 _ _ OI = e x

  m : ty 𝕀₂ → (x : A) → B x
  m z x = elim 𝕀₂ (λ _ → B x) (k x) (l x _ _) z

funext :
  {l m : Level}
  {A : Set l}
  {B C : A → Set m}
  {f : (x : A) → B x}
  {g : (x : A) → C x}
  (_ : ∀ x → f x ≡≡ g x)
  → ---------------------
  f ≡≡ g
funext e with homfunext (≡≡typ ∘ e)
funext e | refl = homfunext e

----------------------------------------------------------------------
-- Function extensionality with implicit arguments
----------------------------------------------------------------------
implicit-eval :
  {l m : Level}
  {A : Set l}
  {B : A → Set m}
  → -----------------------------
  ((x : A) → B x) → {x : A} → B x
implicit-eval f {x} = f x

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 {f = f} {g} e =
  ap implicit-eval (funext {f = λ x → f{x}} {g = λ x → g{x}} e)

----------------------------------------------------------------------
-- Functions of two quotiented arguments (uses funext)
----------------------------------------------------------------------
module quot₂ where
  ext :
    {l m : Level}
    {A : Set l}
    {R : A → A → Set m}
    {n : Level}
    {B : A / R → Set n}
    (g h : ∀ t → B t)
    (_ : ∀ x → g([ x ]/ R) ≡ h([ x ]/ R))
    → ------------------------------------
    g ≡ h
  ext {A = A} {R} g h e =
    funext (quot.elim _ _ e
    λ r → uip (ap g (quot.eq R r)))

  lift :
    {l l' m m' : Level}
    {A : Set l}
    {R : A → A → Set m}
    {B : Set l'}
    {S : B → B → Set 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')
    → ------------------------------------------
    A / R → B / S → C
  lift {S = S} f e₁ e₂ =
    quot.lift
      (λ x → quot.lift (f x) e₂)
      (λ {x} {y} r →
        ext {R = S}
          (quot.lift (f x) e₂)
          (quot.lift (f y) e₂)
          (λ _ → e₁ r))

  _ :
    {l l' m m' n : Level}
    {A : Set l}
    {R : A → A → Set m}
    {B : Set l'}
    {S : B → B → Set m'}
    {C : Set n}
    (f : A → B → C)
    (e₁ : ∀ {x x' y } → R x x' → f x y ≡ f x' y )
    (e₂ : ∀ {x y  y'} → S y y' → f x y ≡ f x  y')
    → -------------------------------------------------
    ∀ x y → lift f e₁ e₂ ([ x ]/ R) ([ y ]/ S) ≡ f x y
  _ = λ _ _ _ _ _ → refl