------------------------------------------------------------------------
-- Quotients (set-quotients), defined using a higher inductive type
------------------------------------------------------------------------

-- Note that this module is experimental: it uses rewrite rules and
-- postulates to encode a higher inductive type.

{-# OPTIONS --without-K --rewriting #-}

-- Partly following the HoTT book.

module Quotient.HIT where

open import Equality.Propositional as EP hiding (elim)
open import Interval using (ext; ⟨ext⟩)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (_∘_; id)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional as Trunc hiding (rec; elim)
open import Preimage equality-with-J using (_⁻¹_)
import Quotient equality-with-J as Quotient
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

------------------------------------------------------------------------
-- Quotients

-- I have tried to follow the rules for HITs specified in the
-- HoTT-Agda library
-- (https://github.com/HoTT/HoTT-Agda/blob/master/lib/types/HIT_README.txt).

-- The quotient type constructor.

infix 5 _/_

postulate
  _/_ :  {a r} (A : Set a)  (A  A  Proposition r)  Set (a  r)

module _ {a r} {A : Set a} {R : A  A  Proposition r} where

  postulate

    -- Constructors.

    [_]                  : A  A / R
    []-respects-relation :  {x y}  proj₁ (R x y)  [ x ]  [ y ]
    /-is-set             : Is-set (A / R)

    -- Eliminator.

    elim :
       {p} (P : A / R  Set p) 
      (p-[] :  x  P [ x ]) 
      (∀ {x y} (r : proj₁ (R x y)) 
       subst P ([]-respects-relation r) (p-[] x)  p-[] y) 
      (∀ x  Is-set (P x)) 
       x  P x

-- Computation rules.
--
-- NOTE: There is no computation rule corresponding to /-is-set, and
-- rewriting has not been activated for the "computation" rule
-- corresponding to []-respects-relation.

module _ {a r p}
         {A : Set a} {R : A  A  Proposition r} {P : A / R  Set p}
         {p-[] :  x  P [ x ]}
         {p-[]-respects-relation :
             {x y} (r : proj₁ (R x y)) 
            subst P ([]-respects-relation r) (p-[] x)  p-[] y}
         {is-set :  x  Is-set (P x)}
         where

  -- Computation rule for [_].

  postulate
    elim-[] :
       x  elim P p-[] p-[]-respects-relation is-set [ x ]  p-[] x

  {-# REWRITE elim-[] #-}

  -- "Computation" rule for []-respects-relation.

  postulate
    elim-[]-respects-relation :
       {x y} (r : proj₁ (R x y)) 
      dependent-cong (elim P p-[] p-[]-respects-relation is-set)
                     ([]-respects-relation r) 
      p-[]-respects-relation r

-- A non-dependent eliminator.

rec :
   {a r p} {A : Set a} {R : A  A  Proposition r} {P : Set p}
  (f : A  P) 
  (∀ {x y}  proj₁ (R x y)  f x  f y) 
  Is-set P 
  A / R  P
rec {P = P} f resp P-set = elim
  _
  f
   {x y} r 
     subst (const P) ([]-respects-relation r) (f x)  ≡⟨ subst-const ([]-respects-relation r) 
     f x                                             ≡⟨ resp r ⟩∎
     f y                                             )
   _  P-set)

-- A variant of elim that can be used if the motive composed with [_]
-- is a family of propositions.
--
-- I took the idea for this eliminator from Nicolai Kraus.

elim-Prop :
   {a r} {A : Set a} {R : A  A  Proposition r} {p}
  (P : A / R  Set p) 
  (p-[] :  x  P [ x ]) 
  (∀ x  Is-proposition (P [ x ])) 
   x  P x
elim-Prop P p-[] P-prop = elim
  P p-[]
   _  _⇔_.to propositional⇔irrelevant (P-prop _) _ _)
  (elim
     _
     (mono₁ 1  P-prop)
      _  _⇔_.to propositional⇔irrelevant
              (H-level-propositional ext 2) _ _)
      _  mono₁ 1 (H-level-propositional ext 2)))

-- A variant of rec that can be used if the motive is a proposition.

rec-Prop :
   {a r} {A : Set a} {R : A  A  Proposition r} {p} {P : Set p} 
  (A  P) 
  Is-proposition P 
  A / R  P
rec-Prop p-[] P-prop = elim-Prop (const _) p-[] (const P-prop)

------------------------------------------------------------------------
-- Equivalence relations

-- The definition of an equivalence relation.

Is-equivalence-relation :
   {a r} {A : Set a} (R : A  A  Proposition r)  Set (a  r)
Is-equivalence-relation R =
  Quotient.Is-equivalence-relation  x y  proj₁ (R x y))

open Quotient public using (module Is-equivalence-relation)

-- A trivial, propositional binary relation.

Trivial :  {a r} {A : Set a}  A  A  Proposition r
Trivial _ _ =  _  , ↑-closure 1 (mono₁ 0 ⊤-contractible)

-- This relation is an equivalence relation.

Trivial-is-equivalence-relation :
   {a r} {A : Set a} 
  Is-equivalence-relation (Trivial {r = r} {A = A})
Trivial-is-equivalence-relation = _

------------------------------------------------------------------------
-- Pointwise liftings of binary relations

-- The superscript P used in the names of the definitions in this
-- section stands for "pointwise".

-- Lifts binary, propositional relations from B to A → B.

infix 0 _→ᴾ_

_→ᴾ_ :
   {a b r} (A : Set a) {B : Set b} 
  (B  B  Proposition r) 
  ((A  B)  (A  B)  Proposition (a  r))
(_ →ᴾ R) f g =
    (∀ x  proj₁ (R (f x) (g x)))
  , Π-closure ext 1 λ _ 
    proj₂ (R _ _)

-- _→ᴾ_ preserves equivalence relations.

→ᴾ-preserves-Is-equivalence-relation :
   {a b r} {A : Set a} {B : Set b} {R : B  B  Proposition r} 
  Is-equivalence-relation R 
  Is-equivalence-relation (A →ᴾ R)
→ᴾ-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = λ _  reflexive
  ; symmetric  = λ f∼g x  symmetric (f∼g x)
  ; transitive = λ f∼g g∼h x  transitive (f∼g x) (g∼h x)
  }
  where
  open Is-equivalence-relation R-equiv

-- Lifts binary, propositional relations from A and B to A ⊎ B.

infixr 1 _⊎ᴾ_

_⊎ᴾ_ :
   {a b r} {A : Set a} {B : Set b} 
  (A  A  Proposition r) 
  (B  B  Proposition r) 
  (A  B  A  B  Proposition r)
(P ⊎ᴾ Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎ᴾ Q) (inj₂ x) (inj₂ y) = Q x y
(P ⊎ᴾ Q) _        _        =  , ⊥-propositional

-- _⊎ᴾ_ preserves Is-equivalence-relation.

⊎ᴾ-preserves-Is-equivalence-relation :
   {a b r} {A : Set a} {B : Set b}
    {P : A  A  Proposition r} {Q : B  B  Proposition r} 
  Is-equivalence-relation P 
  Is-equivalence-relation Q 
  Is-equivalence-relation (P ⊎ᴾ Q)
⊎ᴾ-preserves-Is-equivalence-relation P-equiv Q-equiv = record
  { reflexive  = λ { {x = inj₁ _}  reflexive P-equiv
                   ; {x = inj₂ _}  reflexive Q-equiv
                   }
    ; symmetric  = λ { {x = inj₁ _} {y = inj₁ _}  symmetric P-equiv
                     ; {x = inj₂ _} {y = inj₂ _}  symmetric Q-equiv
                     ; {x = inj₁ _} {y = inj₂ _} ()
                     ; {x = inj₂ _} {y = inj₁ _} ()
                     }
  ; transitive = λ
     { {x = inj₁ _} {y = inj₁ _} {z = inj₁ _}  transitive P-equiv
     ; {x = inj₂ _} {y = inj₂ _} {z = inj₂ _}  transitive Q-equiv

     ; {x = inj₁ _} {y = inj₂ _} ()
     ; {x = inj₂ _} {y = inj₁ _} ()
     ; {y = inj₁ _} {z = inj₂ _} _ ()
     ; {y = inj₂ _} {z = inj₁ _} _ ()
     }
  }
  where
  open Is-equivalence-relation

-- Lifts a binary, propositional relation from A to Maybe A.

Maybeᴾ :
   {a r} {A : Set a} 
  (A  A  Proposition r) 
  (Maybe A  Maybe A  Proposition r)
Maybeᴾ R = Trivial ⊎ᴾ R

-- Maybeᴾ preserves Is-equivalence-relation.

Maybeᴾ-preserves-Is-equivalence-relation :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  Is-equivalence-relation R 
  Is-equivalence-relation (Maybeᴾ R)
Maybeᴾ-preserves-Is-equivalence-relation =
  ⊎ᴾ-preserves-Is-equivalence-relation Trivial-is-equivalence-relation

------------------------------------------------------------------------
-- Some properties

module _ {a r} {A : Set a} {R : A  A  Proposition r} where

  -- [_] is surjective.

  []-surjective : Surjective ([_] {R = R})
  []-surjective = elim-Prop
    _
     x   x , refl )
     _  truncation-is-proposition)

  -- If the relation is an equivalence relation, then it is equivalent
  -- to equality under [_].
  --
  -- The basic structure of this proof is that of Proposition 2 in
  -- "Quotienting the Delay Monad by Weak Bisimilarity" by Chapman,
  -- Uustalu and Veltri.

  related≃[equal] :
    Propositional-extensionality r 
    Is-equivalence-relation R 
     {x y}  proj₁ (R x y)  _≡_ {A = A / R} [ x ] [ y ]
  related≃[equal] prop-ext R-equiv {x} {y} =
    _↠_.from (Eq.≃↠⇔ (proj₂ (R x y)) (/-is-set _ _))
      (record
        { to   = []-respects-relation
        ; from = λ [x]≡[y] 
                                $⟨ reflexive 
            proj₁ (R′ x [ x ])  ↝⟨ ≡⇒→ (cong (proj₁  R′ x) [x]≡[y]) 
            proj₁ (R′ x [ y ])  ↝⟨ id ⟩□
            proj₁ (R x y)       
        })
    where
    open Is-equivalence-relation R-equiv

    lemma :  {x y z}  proj₁ (R y z)  R x y  R x z
    lemma {x} {y} {z} r =            $⟨ record
                                          { to   = flip transitive r
                                          ; from = flip transitive (symmetric r)
                                          } 
      proj₁ (R x y)  proj₁ (R x z)  ↝⟨ ⇔↔≡″ ext prop-ext 
      R x y  R x z                  

    R′ : A  A / R  Proposition r
    R′ x = rec
       y  R x y)
      lemma
      (Is-set-∃-Is-proposition ext prop-ext)

-- Quotienting with equality (for a set) amounts to the same thing as
-- not quotienting at all.

/≡↔ :
   {a} {A : Set a} 
  (A-set : Is-set A) 
  (A / λ x y  (x  y) , A-set x y)  A
/≡↔ A-set = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec id id A-set
      ; from = [_]
      }
    ; right-inverse-of = λ _  refl
    }
  ; left-inverse-of = elim-Prop _  _  refl)  _  /-is-set _ _)
  }

-- Quotienting with a trivial relation amounts to the same thing as
-- using the propositional truncation.

/trivial↔∥∥ :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  (∀ x y  proj₁ (R x y)) 
  A / R   A 
/trivial↔∥∥ {A = A} {R} trivial = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec-Prop ∣_∣ truncation-is-proposition
      ; from = Trunc.rec /-prop [_]
      }
    ; right-inverse-of = Trunc.elim
        _
         _  mono₁ 0 (truncation-is-proposition _ _))
         _  refl)
    }
  ; left-inverse-of = elim-Prop _  _  refl)  _  /-is-set _ _)
  }
  where
  /-prop : Is-proposition (A / R)
  /-prop = _⇔_.from propositional⇔irrelevant $
    elim-Prop _
       x  elim-Prop _
          y  []-respects-relation (trivial x y))
          _  /-is-set _ _))
       _  Π-closure ext 1 λ _ 
             /-is-set _ _)

-- If the relation is a propositional equivalence relation of a
-- certain size, then there is a split surjection from the definition
-- of quotients given in Quotient to the one given here (assuming
-- extensionality and univalence).
--
-- I don't know if this result can be strengthened to an isomorphism:
-- I encountered size issues when trying to prove this.

/↠/ :  {a} {A : Set a} {R : A  A  Set a} 
      Univalence a 
      Univalence (# 0) 
      Quotient.Is-equivalence-relation R 
      (R-prop :  x y  Is-proposition (R x y)) 
      A Quotient./ R  A /  x y  R x y , R-prop x y)
/↠/ {a} {A} {R} univ univ₀ R-equiv R-prop = record
  { logical-equivalence = record
    { to   = to
    ; from = from
    }
  ; right-inverse-of = to∘from
  }
  where
  R′ : A  A  Proposition a
  R′ x y = R x y , R-prop x y

  R-is-strong-equivalence : Quotient.Strong-equivalence R
  R-is-strong-equivalence =
    Quotient.propositional-equivalence⇒strong-equivalence
      ext univ R-equiv R-prop

  []-respects-R :  {x y}  R x y  Quotient.[ x ]  Quotient.[ y ]
  []-respects-R =
    _↔_.to (Quotient.related↔[equal] ext R-is-strong-equivalence)

  to : A Quotient./ R  A / R′
  to = Quotient.rec
    ext
    (Is-equivalence-relation.reflexive R-equiv)
    _
    /-is-set
    [_]
    []-respects-relation

  from : A / R′  A Quotient./ R
  from = rec
    Quotient.[_]
    []-respects-R
    (Quotient.quotient's-h-level-is-1-+-relation's-h-level
       ext univ univ₀ 1 R-prop)

  to∘from :  x  to (from x)  x
  to∘from = elim-Prop
    _
     _  refl)
     _  /-is-set _ _)

-- Two applications of _/_ are isomorphic if the underlying types are
-- isomorphic and the relations are pointwise logically equivalent.

infix 5 _/-cong_

_/-cong_ :
   {k a₁ a₂ r₁ r₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {R₁ : A₁  A₁  Proposition r₁}
    {R₂ : A₂  A₂  Proposition r₂} 
  (A₁↔A₂ : A₁ ↔[ k ] A₂) 
  (∀ x y 
     proj₁ (R₁ x y) 
     proj₁ (R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y))) 
  A₁ / R₁ ↔[ k ] A₂ / R₂
_/-cong_ {k} {R₁ = R₁} {R₂} A₁↔A₂ R₁⇔R₂ = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = rec
                 ([_]  to)
                 ([]-respects-relation  _⇔_.to (R₁⇔R₂′ _ _))
                 /-is-set
      ; from = rec
                 ([_]  from)
                  {x y} 
                    proj₁ (R₂ x y)                          ↝⟨ ≡⇒↝ _ (sym $ cong₂  x y  proj₁ (R₂ x y))
                                                                                  (right-inverse-of x)
                                                                                  (right-inverse-of y)) 
                    proj₁ (R₂ (to (from x)) (to (from y)))  ↝⟨ _⇔_.from (R₁⇔R₂′ _ _) 
                    proj₁ (R₁ (from x) (from y))            ↝⟨ []-respects-relation ⟩□
                    [ from x ]  [ from y ]                 )
                 /-is-set
      }
    ; right-inverse-of = elim-Prop
        _
         x 
          [ to (from x) ]  ≡⟨ cong [_] $ right-inverse-of x ⟩∎
          [ x ]            )
         _  /-is-set _ _)
    }
  ; left-inverse-of = elim-Prop
      _
       x 
        [ from (to x) ]  ≡⟨ cong [_] $ left-inverse-of x ⟩∎
        [ x ]            )
       _  /-is-set _ _)
  })
  where
  open _↔_ (from-isomorphism A₁↔A₂)

  R₁⇔R₂′ = λ x y 
    proj₁ (R₁ x y)                                                ↝⟨ R₁⇔R₂ x y 
    proj₁ (R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y))  ↝⟨ ≡⇒↝ _ $ cong₂  f g  proj₁ (R₂ (f x) (g y)))
                                                                                   (to-implication∘from-isomorphism k bijection)
                                                                                   (to-implication∘from-isomorphism k bijection) ⟩□
    proj₁ (R₂ (to x) (to y))                                      

------------------------------------------------------------------------
-- Various type formers commute with quotients

-- _⊎_ commutes with quotients.

⊎/-comm :
   {a b r} {A : Set a} {B : Set b}
    {P : A  A  Proposition r} {Q : B  B  Proposition r} 
  (A  B) / (P ⊎ᴾ Q)  A / P  B / Q
⊎/-comm = record
  { surjection = record
    { logical-equivalence = record
      { to = rec
          (⊎-map [_] [_])
           { {x = inj₁ _} {y = inj₁ _}  cong inj₁ 
                                           []-respects-relation
             ; {x = inj₂ _} {y = inj₂ _}  cong inj₂ 
                                           []-respects-relation
             ; {x = inj₁ _} {y = inj₂ _} ()
             ; {x = inj₂ _} {y = inj₁ _} ()
             })
          (⊎-closure 0 /-is-set /-is-set)
      ; from = Prelude.[ rec ([_]  inj₁) []-respects-relation /-is-set
                       , rec ([_]  inj₂) []-respects-relation /-is-set
                       ]
      }
    ; right-inverse-of =
        Prelude.[ elim-Prop
                    _
                     _  refl)
                     _  ⊎-closure 0 /-is-set /-is-set _ _)
                , elim-Prop
                    _
                     _  refl)
                     _  ⊎-closure 0 /-is-set /-is-set _ _)
                ]
    }
  ; left-inverse-of = elim-Prop
      _
      Prelude.[  _  refl) ,  _  refl) ]
       _  /-is-set _ _)
  }

-- Maybe commutes with quotients.
--
-- Chapman, Uustalu and Veltri mention a similar result in
-- "Quotienting the Delay Monad by Weak Bisimilarity".

Maybe/-comm :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  Maybe A / Maybeᴾ R  Maybe (A / R)
Maybe/-comm {A = A} {R} =
  Maybe A / Maybeᴾ R   ↝⟨ ⊎/-comm 
   / Trivial  A / R  ↝⟨ /trivial↔∥∥ _ ⊎-cong F.id 
      A / R        ↝⟨ ∥∥↔ (mono₁ 0 ⊤-contractible) ⊎-cong F.id ⟩□
  Maybe (A / R)        

-- A simplification lemma for Maybe/-comm.

Maybe/-comm-[] :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  _↔_.to Maybe/-comm  [_]  ⊎-map id ([_] {R = R})
Maybe/-comm-[] =
  _↔_.to Maybe/-comm  [_]                             ≡⟨⟩

  ⊎-map _ id 
  ⊎-map (rec-Prop ∣_∣ truncation-is-proposition) id 
  ⊎-map [_] [_]                                        ≡⟨ cong (_∘ ⊎-map [_] [_]) ⊎-map-∘ 

  ⊎-map _ id  ⊎-map [_] [_]                           ≡⟨ ⊎-map-∘ ⟩∎

  ⊎-map id [_]                                         
  where
  ⊎-map-∘ :  {a₁ b₁ c₁} {A₁ : Set a₁} {B₁ : Set b₁} {C₁ : Set c₁}
              {a₂ b₂ c₂} {A₂ : Set a₂} {B₂ : Set b₂} {C₂ : Set c₂}
              {f₁ : B₁  C₁} {g₁ : A₁  B₁}
              {f₂ : B₂  C₂} {g₂ : A₂  B₂} 
            ⊎-map f₁ f₂  ⊎-map g₁ g₂  ⊎-map (f₁  g₁) (f₂  g₂)
  ⊎-map-∘ = ⟨ext⟩ Prelude.[  _  refl) ,  _  refl) ]

-- The sigma type former commutes (kind of) with quotients, assuming
-- that the second projections come from propositional types.

Σ/-comm :
   {a r p}
    {A : Set a} {R : A  A  Proposition r} {P : A / R  Set p} 
  (∀ x  Is-proposition (P x)) 
  Σ (A / R) P  Σ A (P  [_]) / (R on proj₁)
Σ/-comm {A = A} {R} {P} P-prop = record
  { surjection = record
    { logical-equivalence = record
      { to = uncurry $ elim
           x  P x  Σ A (P  [_]) / (R on proj₁))
          (curry [_])
           {x y} r  ⟨ext⟩ λ P[y] 
             subst  x  P x  Σ A (P  [_]) / (R on proj₁))
                   ([]-respects-relation r)
                   (curry [_] x) P[y]                               ≡⟨ cong (_$ P[y]) $ subst-→-domain _ ([]-respects-relation r) 

             [ (x , subst P (sym $ []-respects-relation r) P[y]) ]  ≡⟨ []-respects-relation r ⟩∎

             [ (y , P[y]) ]                                         )
           _  Π-closure ext 2 λ _ 
                 /-is-set)
      ; from = rec
          (Σ-map [_] id)
           { {x = (x₁ , x₂)} {y = (y₁ , y₂)} 
               proj₁ (R x₁ y₁)                ↝⟨ []-respects-relation 
               [ x₁ ]  [ y₁ ]                ↔⟨ ignore-propositional-component (P-prop _) 
               ([ x₁ ] , x₂)  ([ y₁ ] , y₂)  
             })
          (Σ-closure 2 /-is-set (mono₁ 1  P-prop))
      }
    ; right-inverse-of = elim-Prop
        _
         _  refl)
         _  /-is-set _ _)
    }
  ; left-inverse-of = uncurry $ elim-Prop
      _
       _ _  refl)
       _  Π-closure ext 1 λ _ 
             (Σ-closure 2 /-is-set (mono₁ 1  P-prop)) _ _)
  }

-- The type former λ X → ℕ → X commutes with quotients, assuming that
-- the quotient relation is an equivalence relation, and also assuming
-- propositional extensionality and countable choice.
--
-- This result is very similar to Proposition 5 in "Quotienting the
-- Delay Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

-- The forward component of the isomorphism. This component can be
-- defined without any extra assumptions.

ℕ→/-comm-to :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  (  A) / ( →ᴾ R)  (  A / R)
ℕ→/-comm-to = rec
   f n  [ f n ])
   r  ⟨ext⟩ ([]-respects-relation  r))
  (Π-closure ext 2 λ _ 
   /-is-set)

-- The isomorphism.

ℕ→/-comm :
   {a r} {A : Set a} {R : A  A  Proposition r} 
  Propositional-extensionality r 
  Axiom-of-countable-choice (a  r) 
  Is-equivalence-relation R 
  (  A) / ( →ᴾ R)  (  A / R)
ℕ→/-comm {A = A} {R} prop-ext cc R-equiv = record
  { surjection = record
    { logical-equivalence = record
      { to   = ℕ→/-comm-to
      ; from = from unit
      }
    ; right-inverse-of = to∘from unit
    }
  ; left-inverse-of = from∘to unit
  }
  where
  [_]→ : (  A)  (  A / R)
  [ f ]→ n = [ f n ]

  -- A module that is introduced to ensure that []→-surjective is not
  -- in the same abstract block as the abstract definitions below.

  module Dummy where

    abstract

      []→-surjective : Surjective [_]→
      []→-surjective f =                    $⟨ []-surjective 
        Surjective [_]                      ↝⟨  surj  surj  f) 
        (∀ n   ( λ x  [ x ]  f n) )   ↔⟨ countable-choice-bijection cc 
         (∀ n   λ x  [ x ]  f n)      ↔⟨ ∥∥-cong ΠΣ-comm 
         ( λ g   n  [ g n ]  f n)    ↔⟨ Bijection.id 
         ( λ g   n  [ g ]→ n  f n)   ↔⟨ ∥∥-cong (∃-cong λ _  Eq.extensionality-isomorphism ext) ⟩□
         ( λ g  [ g ]→  f)             

  open Dummy

  from₁ :  f  [_]→ ⁻¹ f  ℕ→/-comm-to ⁻¹ f
  from₁ f (g , [g]→≡f) =
      [ g ]
    , (ℕ→/-comm-to [ g ]  ≡⟨⟩
       [ g ]→             ≡⟨ [g]→≡f ⟩∎
       f                  )

  from₁-constant :  f  Constant (from₁ f)
  from₁-constant f (g₁ , [g₁]→≡f) (g₂ , [g₂]→≡f) =
                                             $⟨  n  cong (_$ n) (
        [ g₁ ]→                                    ≡⟨ [g₁]→≡f 
        f                                          ≡⟨ sym [g₂]→≡f ⟩∎
        [ g₂ ]→                                    )) 

    (∀ n  [ g₁ ]→ n  [ g₂ ]→ n)            ↔⟨ Bijection.id 

    (∀ n  [ g₁ n ]  [ g₂ n ])              ↔⟨ ∀-cong ext  _  inverse $ related≃[equal] {R = R} prop-ext R-equiv) 

    (∀ n  proj₁ (R (g₁ n) (g₂ n)))          ↔⟨ Bijection.id 

    proj₁ (( →ᴾ R) g₁ g₂)                   ↝⟨ []-respects-relation 

    [ g₁ ]  [ g₂ ]                          ↔⟨ ignore-propositional-component
                                                  ((Π-closure ext 2 λ _ 
                                                    /-is-set) _ _) ⟩□
    ([ g₁ ] , [g₁]→≡f)  ([ g₂ ] , [g₂]→≡f)  

  from₂ : Unit   f   [_]→ ⁻¹ f   ℕ→/-comm-to ⁻¹ f
  from₂ unit f =
    _≃_.to (constant-function≃∥inhabited∥⇒inhabited
              (Σ-closure 2 /-is-set λ _ 
               mono₁ 1 (Π-closure ext 2  _  /-is-set) _ _)))
           (from₁ f , from₁-constant f)

  unblock-from₂ :  x f p  from₂ x f  p   from₁ f p
  unblock-from₂ unit _ _ = refl

  abstract

    from₃ : Unit   f  ℕ→/-comm-to ⁻¹ f
    from₃ x f = from₂ x f ([]→-surjective f)

    from : Unit  (  A / R)  (  A) / ( →ᴾ R)
    from x f = proj₁ (from₃ x f)

    to∘from :  x f  ℕ→/-comm-to (from x f)  f
    to∘from x f = proj₂ (from₃ x f)

    from∘to :  x f  from x (ℕ→/-comm-to f)  f
    from∘to x = elim-Prop
       f  from x (ℕ→/-comm-to f)  f)
       f 
         from x (ℕ→/-comm-to [ f ])                      ≡⟨⟩

         proj₁ (from₂ x [ f ]→ ([]→-surjective [ f ]→))  ≡⟨ cong (proj₁  from₂ x [ f ]→) $
                                                              _⇔_.to propositional⇔irrelevant truncation-is-proposition _ _ 
         proj₁ (from₂ x [ f ]→  f , refl )             ≡⟨ cong proj₁ $ unblock-from₂ x _ (f , refl) 

         proj₁ (from₁ [ f ]→ (f , refl))                 ≡⟨⟩

         [ f ]                                           )
       _  /-is-set _ _)

------------------------------------------------------------------------
-- Quotient-like eliminators

-- If there is a split surjection from a quotient type to some other
-- type, then one can construct a quotient-like eliminator for the
-- other type.
--
-- This kind of construction is used in "Quotienting the Delay Monad
-- by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

↠-eliminator :
   {a b r} {A : Set a} {R : A  A  Proposition r} {B : Set b}
  (surj : A / R  B) 
   {p} (P : B  Set p) 
  (p-[] :  x  P (_↠_.to surj [ x ])) 
  (∀ {x y} (r : proj₁ (R x y)) 
   subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) 
   p-[] y) 
  (∀ x  Is-set (P x)) 
   x  P x
↠-eliminator surj P p-[] ok P-set x =
  subst P (_↠_.right-inverse-of surj x) p
  where
  p : P (_↠_.to surj (_↠_.from surj x))
  p = elim
    (P  _↠_.to surj)
    p-[]
     {x y} r 
       subst (P  _↠_.to surj) ([]-respects-relation r) (p-[] x)       ≡⟨ subst-∘ P (_↠_.to surj) ([]-respects-relation r) 
       subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x)  ≡⟨ ok r 
       p-[] y                                                          )
     _  P-set _)
    (_↠_.from surj x)

-- The eliminator "computes" in the "right" way for elements that
-- satisfy a certain property.

↠-eliminator-[] :
   {a b r} {A : Set a} {R : A  A  Proposition r} {B : Set b}
  (surj : A / R  B) 
   {p} (P : B  Set p)
  (p-[] :  x  P (_↠_.to surj [ x ]))
  (ok :  {x y} (r : proj₁ (R x y)) 
        subst P (cong (_↠_.to surj) ([]-respects-relation r)) (p-[] x) 
        p-[] y)
  (P-set :  x  Is-set (P x)) x 
  _↠_.from surj (_↠_.to surj [ x ])  [ x ] 
  ↠-eliminator surj P p-[] ok P-set (_↠_.to surj [ x ])  p-[] x
↠-eliminator-[] {R = R} surj P p-[] ok P-set x hyp =
  subst P (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
    (elim (P  _↠_.to surj) p-[] ok′  _  P-set _)
          (_↠_.from surj (_↠_.to surj [ x ])))               ≡⟨ cong  p  subst P p (elim (P  _↠_.to surj) _ _ _ _)) $
                                                                  _⇔_.to set⇔UIP (H-level.respects-surjection surj 2 /-is-set)
                                                                    (_↠_.right-inverse-of surj (_↠_.to surj [ x ]))
                                                                    (cong (_↠_.to surj) hyp) 
  subst P (cong (_↠_.to surj) hyp)
    (elim (P  _↠_.to surj) p-[] ok′  _  P-set _)
          (_↠_.from surj (_↠_.to surj [ x ])))               ≡⟨ EP.elim
                                                                   {x y} p  subst P (cong (_↠_.to surj) p)
                                                                                 (elim (P  _↠_.to surj) p-[] ok′  _  P-set _) x) 
                                                                               elim (P  _↠_.to surj) p-[] ok′  _  P-set _) y)
                                                                   _  refl)
                                                                  hyp 
  elim (P  _↠_.to surj) p-[] ok′  _  P-set _) [ x ]      ≡⟨⟩

  p-[] x                                                     
  where
  ok′ :  {x y} (r : proj₁ (R x y))  _
  ok′ = λ r 
    trans (subst-∘ P (_↠_.to surj) ([]-respects-relation r)) (ok r)

-- If there is a bijection from a quotient type to some other type,
-- then one can also construct a quotient-like eliminator for the
-- other type.

↔-eliminator :
   {a b r} {A : Set a} {R : A  A  Proposition r} {B : Set b}
  (bij : A / R  B) 
   {p} (P : B  Set p) 
  (p-[] :  x  P (_↔_.to bij [ x ])) 
  (∀ {x y} (r : proj₁ (R x y)) 
   subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) 
   p-[] y) 
  (∀ x  Is-set (P x)) 
   x  P x
↔-eliminator bij = ↠-eliminator (_↔_.surjection bij)

-- This latter eliminator always "computes" in the "right" way.

↔-eliminator-[] :
   {a b r} {A : Set a} {R : A  A  Proposition r} {B : Set b}
  (bij : A / R  B) 
   {p} (P : B  Set p)
  (p-[] :  x  P (_↔_.to bij [ x ]))
  (ok :  {x y} (r : proj₁ (R x y)) 
        subst P (cong (_↔_.to bij) ([]-respects-relation r)) (p-[] x) 
        p-[] y)
  (P-set :  x  Is-set (P x)) x 
  ↔-eliminator bij P p-[] ok P-set (_↔_.to bij [ x ])  p-[] x
↔-eliminator-[] bij P p-[] ok P-set x =
  ↠-eliminator-[] (_↔_.surjection bij) P p-[] ok P-set x
    (_↔_.left-inverse-of bij [ x ])

-- A quotient-like eliminator for functions of type ℕ → A / R, where R
-- is an equivalence relation. Defined using propositional
-- extensionality and countable choice.
--
-- This eliminator is taken from Corollary 1 in "Quotienting the Delay
-- Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

ℕ→/-elim :
   {a p r} {A : Set a} {R : A  A  Proposition r} 
  Propositional-extensionality r 
  Axiom-of-countable-choice (a  r) 
  Is-equivalence-relation R 
  (P : (  A / R)  Set p)
  (p-[] :  f  P  n  [ f n ])) 
  (∀ {f g} (r : proj₁ (( →ᴾ R) f g)) 
   subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) 
   p-[] g) 
  (∀ f  Is-set (P f)) 
   f  P f
ℕ→/-elim prop-ext cc R-equiv = ↔-eliminator (ℕ→/-comm prop-ext cc R-equiv)

-- The eliminator "computes" in the "right" way.

ℕ→/-elim-[] :
   {a p r} {A : Set a} {R : A  A  Proposition r}
  (prop-ext : Propositional-extensionality r)
  (cc : Axiom-of-countable-choice (a  r))
  (R-equiv : Is-equivalence-relation R)
  (P : (  A / R)  Set p)
  (p-[] :  f  P  n  [ f n ]))
  (ok :  {f g} (r : proj₁ (( →ᴾ R) f g)) 
        subst P (cong ℕ→/-comm-to ([]-respects-relation r)) (p-[] f) 
        p-[] g)
  (P-set :  f  Is-set (P f)) f 
  ℕ→/-elim prop-ext cc R-equiv P p-[] ok P-set  n  [ f n ])  p-[] f
ℕ→/-elim-[] prop-ext cc R-equiv =
  ↔-eliminator-[] (ℕ→/-comm prop-ext cc R-equiv)