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

module set-quotient where

open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels
open import foundation.constant-type-families
       renaming ( tr-constant-type-family  to tr-const
                ; apd-constant-type-family to apd-const)


open import notation
open import rewriting


module _ {i j} {A : UU i} (R : A → A → UU j) where

  postulate set-quotient : UU (i ⊔ j)

module _ {i j} {A : UU i} {R : A → A → UU j} where
  postulate q[_] : A → set-quotient R
  postulate
    quot-rel : {a₁ a₂ : A} → R a₁ a₂ → q[ a₁ ] == q[ a₂ ]
  postulate set-quotient-is-set : is-set (set-quotient R)

module _ {i j} {A : UU i} (R : A → A → UU j) where
  Set-quotient : Set (i ⊔ j)
  Set-quotient = (set-quotient R , set-quotient-is-set)

  module _ {k}
      {P : set-quotient {i} {j} {A} R → UU k}
      (p : ∀ x → is-set (P x)) (q[_]* : (a : A) → P q[ a ])
      (rel* : ∀ {a₁ a₂} (r : R a₁ a₂)
            → tr P
                (quot-rel r)
                q[ a₁ ]*
            == q[ a₂ ]*) where
    postulate set-quotient-elim : ∀ x → P x
    postulate set-quotient-elim-β : ∀ a → set-quotient-elim q[ a ] ↦ q[ a ]*
    {-# REWRITE set-quotient-elim-β #-}
    postulate set-quotient-elim-rel-β : ∀ {a₁ a₂} (r : R a₁ a₂) → apd set-quotient-elim (quot-rel r) == rel* r

  module _ {k} {B : UU k}
       (p : is-set B)
       (f : A → B)
       (rel* : ∀ {a₀ a₁} → (r : R a₀ a₁) → f a₀ == f a₁) where

   set-quotient-rec : set-quotient R → B
   set-quotient-rec
      = set-quotient-elim {P = λ _ → B}
                          (λ _ → p)
                          (f)
                          (λ r → tr-const _ _ ∙ rel* r)

   set-quotient-rec-rel-β : ∀ {a₁ a₂} (r : R a₁ a₂)
                          → ap set-quotient-rec (quot-rel r) == rel* r
   set-quotient-rec-rel-β r
     = is-injective-concat (tr-const _ _)
                           (  inv (apd-const _ _)
                            ∙ (set-quotient-elim-rel-β {P = λ _ → B}
                                                       (λ _ → p)
                                                       (f)
                                                       (λ r → tr-const _ _ ∙ rel* r)
                                                       (r)) )


{- Special case when P is propositional. -}
module _ {i j k} {A : UU i} (R : A → A → UU j)
  {P : set-quotient R → UU k}
  (p : ∀ x → is-prop (P x)) where

  set-quotient-prop-elim : ((a : A) → P q[ a ])
                        → ∀ x → P x
  set-quotient-prop-elim q[_]* =
    set-quotient-elim R
      (λ x → is-set-is-prop (p x))
      q[_]*
      λ {a₁} {a₂} Ra₁a₂ → eq-is-prop (p _)


{- The induced transitive, reflexive, symmetric closure -}

module _ {i j} {A : UU i} (R : A → A → UU j) where
   ∥_∥ : A → A → Prop (i ⊔ j)
   ∥_∥ a b = Id-Prop (Set-quotient R) q[ a ] q[ b ]

   ∥_∥-equivalence-class-representation : (a a' : set-quotient R) → ((b : A) → a == q[ b ] ≃ (a' == q[ b ])) ≃ a == a'
   ∥_∥-equivalence-class-representation a a'
        = equiv-iff (Π-Prop A (λ b → equiv-Prop (Id-Prop (Set-quotient R) a  q[ b ])
                                                (Id-Prop (Set-quotient R) a' q[ b ])))
                    (Id-Prop (Set-quotient R) a a')
                    (set-quotient-prop-elim R
                                           {P = λ a' → ((b : A) → a == q[ b ] ≃ (a' == q[ b ])) → a == a'}
                                           (λ _ → is-prop-function-type (set-quotient-is-set _ _))
                                           (λ a' p → (p a' ⁻¹) 〈 refl 〉) a')
                    (λ{refl b → id-equiv})