module quotient where
{---------------------------------------------------------------------
Alan Jeffrey, Dan Licata, Andy Pitts
13 May 2015. 
This is an Agda file Tested with Agda 2.4.2.2

An implementation of quotients up to propositional identity, using an
enhanced version of Dan Licata's trick with Agda's "private" and
"postulate" declarations to define an interval type

http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

The enhancements are two-fold:

1. Use primTrustMe rather than postulates for improved
computational behaviour, inspired by Alan Jeffrey

https://groups.google.com/forum/#!topic/homotopytypetheory/hTAVT6CGbrs

2. Careful combination of thunking and private declarations to ensure
(we hope!)  that the function sending an element to its equivalence
class cannot be proved to be an injection outside the scope of the
private declarations. This Yoga to avoid logical inconsistency is
adapted from Guillaume Brunerie and Dan Licata's hott-agda development

https://github.com/dlicata335/hott-agda/blob/master/lib/spaces/hithacks.agda 

----------------------------------------------------------------------
Usage:

Given
 - a type A : Set
 - a relation R : A → A → Set
you get
 - a type A / R 
   (of equivalence classes for the equivalence relation generated by R)
 - a function _mod R : A → A / R 
   (mapping elements of R to propositional equalities and universal 
   amongst such function out of A)
 - an eliminator for A / R, yielding a function 
   elim B f e : (z : A / R) → B z 
   from B : A / R → Set, f : (x : A) → B(x mod R) and a proof e that 
   f maps elements of R to propositional equalities. 
   elim B f e (x mod R) reduces to f x, because of the use of 
   primTrustMe rather than a postulate, and elim B f e is unique with 
   this property up to propositional equality.
---------------------------------------------------------------------}

open import Agda.Primitive

----------------------------------------------------------------------
module prelude where
  
  -- Propositional equality
  data _≡_ {ℓ : Level}{A : Set ℓ}(x : A) : (x' : A) → Set ℓ where
    refl : x ≡ x

  {-# BUILTIN EQUALITY _≡_ #-}
  {-# BUILTIN REFL refl #-}

  {- 
  We only define quotients for h-sets, so we make all types h-sets by
  allowing pattern-matching-with-K and make use of uniqueness of
  identity proofs
  -} 
  uip :
    {ℓ : Level}
    {A : Set ℓ}
    {x y : A}
    (p q : x ≡ y)
    → -----------------------
    (p ≡ q)
  uip refl refl = refl
  
  _∙_ :
    {ℓ ℓ' : Level}
    {A : Set ℓ}
    {B : Set ℓ'}
    (f : A → B)
    {x y : A}
    (p : x ≡ y)
    → -----------
    f x ≡ f y
  f ∙ refl = refl
  
  transport :
    {ℓ ℓ' : Level}
    {A : Set ℓ}
    (B : A → Set ℓ') 
    {x y : A}
    (p : x ≡ y)
    → -----------
    B x → B y
  transport B refl = λ b → b
  
  
  -- Heterogeneous equality over a given type equality
  _≡_over_ :
    {ℓ : Level}
    {A B : Set ℓ}
    (x : A)
    (y : B)
    (p : A ≡ B)
    → -----------
    Set ℓ
  x ≡ y over refl = x ≡ y
  
  _over_ :
    {ℓ : Level}
    {A : Set ℓ}
    {x y : A}
    (p : x ≡ y)
    (q : A ≡ A)
    → ---------
    (x ≡ y over q)
  p over refl = p
  
  singleton-over : 
    {ℓ : Level}
    {A B : Set ℓ}
    (s : (x y : A) → (x ≡ y))
    (p : A ≡ B)
    (x : A)
    (y : B)
    → -----------------
    (x ≡ y over p)
  singleton-over s refl = s
  
  -- One-element type
  record Unit : Set where
    constructor unit

  -- Booleans
  data 𝔹 : Set where
    true : 𝔹
    false : 𝔹
    
  -- Composition of dependent functions
  infix 1 _∘_ 
  _∘_ :
    {ℓ ℓ' ℓ'' : Level}
    {A : Set ℓ}
    {B : A → Set ℓ'}
    {C : {x : A} → B x → Set ℓ''}
    (g : {x : A}(y : B x) → C y)
    (f : (x : A)  → B x)
    → ---------------------------
    (x : A) → C (f x) 
  g ∘ f = λ x → g (f x) 

-- end of prelude-----------------------------------------------------

open prelude

----------------------------------------------------------------------
--- primTrustMe
----------------------------------------------------------------------
primitive
  primTrustMe :
    {ℓ : Level}
    {A : Set ℓ}
    {x y : A}
    → ---------
    x ≡ y

----------------------------------------------------------------------
-- Quotients up to propositional identity, via primTrustMe
----------------------------------------------------------------------
module quot {A : Set}(R : A → A → Set) where
  private -- # is used to mark private definitions 
    record # (X : Set) : Set where
      constructor #in
      field
        #out : X
    open #

    -- an instance of function extensionality
    #unit-fun-ext :
      {X : Set}
      (f : Unit → X)
      → ----------------
      (λ _ → f unit) ≡ f
    #unit-fun-ext f = primTrustMe --!!!!
    {- This is a safe use of primTrustMe, since function extensionality 
       is known to be consistent. In fact quotient sets can be used to 
       prove functional extensionality -- see funext below -- but we need 
       this instance of it as part of the definition. -} 
  set : Set
  set = # (Unit → # A)

  quo : A → set
  quo x = #in (λ _ → #in x)

  equ :
    {x y : A}
    (r : R x y)
    → -----------
    quo x ≡ quo y
  equ r = primTrustMe --!!!!
  {- This is a potentially unsafe use of primTrustMe. We have to ensure 
     that outside this module it is not possible to prove that quot.fun
     is an injection. -}
     
  elim :
    (B : set → Set)
    (f : (x : A) → B (quo x))
    (_ : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
    (y : set)
    → -----------------------------------------------------
    B y
  elim B f _ (#in g) =
    transport B (#in ∙ #unit-fun-ext g) (f (#out (g unit))) 
--end of module quot

----------------------------------------------------------------------
-- Notation for quotients
----------------------------------------------------------------------
--quotient set
_/_ :
  (A : Set)
  (R : A → A → Set)
  → ---------------
  Set
A / R = quot.set {A} R

-- equivalence classes
quo :
  {A : Set}
  {R : A → A → Set}
  → ---------------
  A → A / R
quo {R = R} = quot.quo R
syntax quo {R = R} x = x mod R

-- generating equalities
equ : 
  {A : Set}
  {R : A → A → Set}
  {x y : A}
  (r : R x y)
  → -------------------
  (x mod R) ≡ (y mod R)
equ {R = R} = quot.equ R

-- equivalence class eliminators
elim :
  {A : Set}
  {R : A → A → Set}
  (B : (A / R) → Set)
  (f : (x : A) → B (x mod R))
  (e : {x y : A} (r : R x y) → f x ≡ f y over (B ∙ equ r))
  (y : A / R)
  → ------------------------------------------------------
  B y
elim {R = R} = quot.elim R

elim-simple :
  {A : Set}
  {R : A → A → Set}
  (B : Set)
  (f : A → B)
  (e : {x y : A}(r : R x y) → f x ≡ f y)
  → ------------------------------------
  A / R → B
elim-simple B f e =
  elim (λ _ → B) f (λ r → e r over ((λ _ → B) ∙ equ r))

-- computation rule
comp :
  {A : Set}
  {R : A → A → Set}
  (B : A / R → Set)
  (f : (x : A) → B (x mod R))
  (e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
  (x : A)
  → -----------------------------------------------------
  elim B f e (x mod R) ≡ f x
comp B f e x = refl

-- uniqueness rule
uniq :
  {A : Set}
  {R : A → A → Set}
  (B : A / R → Set)
  (f : (x : A) → B (x mod R))
  (e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
  (g : (y : A / R) → B y)
  (p : (x : A) → g (x mod R) ≡ f x) 
  → -----------------------------------------------------
  (y : A / R) → g y ≡ elim B f e y
uniq B f e g p =
  let
    B' z        = g z ≡ elim B f e z
    e'{x} {y} r = singleton-over uip (B' ∙ equ r) (p x) (p y)
  in elim B' p e'

----------------------------------------------------------------------
-- Example: A/≡ is isomorphic to A
----------------------------------------------------------------------
i :
  {A : Set}
  (z : A / _≡_)
  → -----------
  A
i {A} = elim-simple A (λ x → x) (λ p → p)

j :
  {A : Set}
  (x : A)
  → -------
  A / _≡_
j x = x mod _≡_

i∘j≡id :
  {A : Set}
  (x : A)
  → ---------
  i (j x) ≡ x
i∘j≡id x = refl

j∘i≡id :
  {A : Set}
  (z : A / _≡_)
  → -----------
  j (i z) ≡ z
j∘i≡id {A} =
  let B = λ z → j (i z) ≡ z in elim B (λ _ → refl) e where
  e : {x y : A} (r : x ≡ y) →
    refl ≡ refl over ((λ z → j (i z) ≡ z) ∙ equ r)
  e refl = refl

----------------------------------------------------------------------
-- Interval type as a quotient 
----------------------------------------------------------------------
data Irel : (x y : 𝔹) → Set where
  rel : Irel false true

I = 𝔹 / Irel

s : I
s = false mod Irel

t : I
t = true mod Irel

path : s ≡ t
path = equ {R = Irel} rel

Ielim :
   {A : Set}
   (x y : A)
   (p : x ≡ y)
   → ---------
   I → A
Ielim {A} x y p = elim-simple A f e where
  f : 𝔹 → A
  f true = y
  f false = x

  e : {b b' : 𝔹} (r : Irel b b') → f b ≡ f b'
  e rel = p

----------------------------------------------------------------------
-- Function extensionality is provable, using the interval type
----------------------------------------------------------------------
funext :
   {A : Set}
   {B : A → Set}
   (f g : (x : A) → B x)
   (e : (x : A) → f x ≡ g x)
   → -----------------------
   f ≡ g
funext f g e = (λ i x → Ielim (f x) (g x) (e x) i) ∙ path

----------------------------------------------------------------------
-- Universal property of quotients
----------------------------------------------------------------------
quot-comp :
  {A : Set}
  {R : A → A → Set}
  (B : A / R → Set)
  (f : (x : A) → B (x mod R))
  (e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
  → -----------------------------------------------------
  (elim B f e ∘ quo) ≡ f
quot-comp B f e = funext (elim B f e ∘ quo) f (λ _ → refl) 

quot-uniq :
  {A : Set}
  {R : A → A → Set}
  (B : A / R → Set)
  (f : (x : A) → B (x mod R))
  (e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
  (g : (y : A / R) → B y)
  (p : (x : A) → g (x mod R) ≡ f x)
  → -----------------------------------------------------
  g ≡ elim B f e
quot-uniq B f e g p =
  let
    B' = λ z → g z ≡ elim B f e z
    p' = elim B' p (λ {x} {y} r →
           singleton-over uip (B' ∙ equ r) (p x) (p y))
  in funext g (elim B f e) p'

----------------------------------------------------------------------
-- SANITY CHECK
----------------------------------------------------------------------
{- The use of primTrustMe in the module quot implies that quo : A → A/R
   cannot always be an injection.  So there should be no way to define 
   the following function... 
quo-inj :
  {A : Set}
  {R : A → A → Set}
  (x y : A)
  (p : (x mod R) ≡ (y mod R))
  → -------------------------
  x ≡ y
quo-inj x y p = {!p!}

  ...since otherwise the use of primTrustMe has led to logical
  inconsistency: 
bad : false ≡ true
bad = quo-inj false true path 
-}