------------------------------------------------------------------------
-- The Agda standard library
--
-- Quotients for Heterogeneous equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.HeterogeneousEquality.Quotients where

open import Function.Base using (_$_; const; _∘_)
open import Level hiding (lift)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.HeterogeneousEquality
open ≅-Reasoning

record Quotient {c ℓ} (S : Setoid c ℓ) : Set (suc (c ⊔ ℓ)) where
  open Setoid S renaming (Carrier to A)
  field
    Q   : Set c
    abs : A → Q

  compat : (B : Q → Set c) (f : ∀ a → B (abs a)) → Set (c ⊔ ℓ)
  compat _ f = {a a′ : A} → a ≈ a′ → f a ≅ f a′

  field
    compat-abs : compat _ abs
    lift       : (B : Q → Set c) (f : ∀ a → B (abs a)) → compat B f → ∀ q → B q
    lift-conv  : {B : Q → Set c} (f : ∀ a → B (abs a)) (p : compat B f) →
                 ∀ a → lift B f p (abs a) ≅ f a

Quotients : ∀ c ℓ → Set (suc (c ⊔ ℓ))
Quotients c ℓ = (S : Setoid c ℓ) → Quotient S

module Properties {c ℓ} {S : Setoid c ℓ} (Qu : Quotient S) where

  open Setoid S renaming (Carrier to A) hiding (refl; sym; trans)
  open Quotient Qu

  module _ {B B′ : Q → Set c} {f : ∀ a → B (abs a)} {p : compat B f} where

   lift-unique : {g : ∀ q → B′ q} → (∀ a → g (abs a) ≅ f a) →
                 ∀ x → lift B f p x ≅ g x
   lift-unique {g} ext = lift _ liftf≅g liftf≅g-ext where

     liftf≅g : ∀ a → lift B f p (abs a) ≅ g (abs a)
     liftf≅g x = begin
       lift _ f p (abs x) ≅⟨ lift-conv f p x ⟩
       f x                ≅⟨ sym (ext x) ⟩
       g (abs x)          ∎

     liftf≅g-ext : ∀ {a a′} → a ≈ a′ → liftf≅g a ≅ liftf≅g a′
     liftf≅g-ext eq = ≅-heterogeneous-irrelevantˡ _ _
                    $ cong (lift B f p) (compat-abs eq)

   lift-ext : {g : ∀ a → B′ (abs a)} {p′ : compat B′ g} → (∀ x → f x ≅ g x) →
              ∀ x → lift B f p x ≅ lift B′ g p′ x
   lift-ext {g} {p′} h = lift-unique $ λ a → begin
       lift B′ g p′ (abs a) ≅⟨ lift-conv g p′ a ⟩
       g a                  ≅⟨ sym (h a) ⟩
       f a                  ∎

  lift-conv-abs : ∀ a → lift (const Q) abs compat-abs a ≅ a
  lift-conv-abs = lift-unique (λ _ → refl)

  lift-fold : {B : Q → Set c} (f : ∀ q → B q) →
              ∀ a → lift B (f ∘ abs) (cong f ∘ compat-abs) a ≅ f a
  lift-fold f = lift-unique (λ _ → refl)

  abs-epimorphism : {B : Q → Set c} {f g : ∀ q → B q} →
                    (∀ x → f (abs x) ≅ g (abs x)) → ∀ q → f q ≅ g q
  abs-epimorphism {B} {f} {g} p q = begin
    f q                                      ≅⟨ sym (lift-fold f q) ⟩
    lift B (f ∘ abs) (cong f ∘ compat-abs) q ≅⟨ lift-ext p q ⟩
    lift B (g ∘ abs) (cong g ∘ compat-abs) q ≅⟨ lift-fold g q ⟩
    g q                                      ∎

------------------------------------------------------------------------
-- Properties provable with extensionality

module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
                {f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where

  module Properties₂
         {c ℓ} {S₁ S₂ : Setoid c ℓ} (Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂)
         where

    module S₁  = Setoid S₁
    module S₂  = Setoid S₂
    module Qu₁ = Quotient Qu₁
    module Qu₂ = Quotient Qu₂

    module _  {B : _ → _ → Set c} (f : ∀ s₁ s₂ → B (Qu₁.abs s₁) (Qu₂.abs s₂)) where

     compat₂ : Set _
     compat₂ = ∀ {a b a′ b′} → a S₁.≈ a′ → b S₂.≈ b′ → f a b ≅ f a′ b′

     lift₂ : compat₂ → ∀ q q′ → B q q′
     lift₂ p = Qu₁.lift _ g (ext ∘ g-ext) module Lift₂ where

       g : ∀ a q → B (Qu₁.abs a) q
       g a = Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl)

       g-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ q → g a q ≅ g a′ q
       g-ext a≈a′ = Properties.lift-ext Qu₂ (λ _ → p a≈a′ S₂.refl)

     lift₂-conv : (p : compat₂) → ∀ a a′ → lift₂ p (Qu₁.abs a) (Qu₂.abs a′) ≅ f a a′
     lift₂-conv p a a′ = begin
       lift₂ p (Qu₁.abs a) (Qu₂.abs a′)
          ≅⟨ cong (_$ (Qu₂.abs a′)) (Qu₁.lift-conv (Lift₂.g p) (ext ∘ Lift₂.g-ext p) a) ⟩
       Lift₂.g p a (Qu₂.abs a′)
          ≡⟨⟩
       Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl) (Qu₂.abs a′)
          ≅⟨ Qu₂.lift-conv (f a) (p S₁.refl) a′ ⟩
       f a a′
          ∎

  module Properties₃ {c ℓ} {S₁ S₂ S₃ : Setoid c ℓ}
         (Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂) (Qu₃ : Quotient S₃)
         where

    module S₁  = Setoid S₁
    module S₂  = Setoid S₂
    module S₃  = Setoid S₃
    module Qu₁ = Quotient Qu₁
    module Qu₂ = Quotient Qu₂
    module Qu₃ = Quotient Qu₃

    module _ {B : _ → _ → _ → Set c}
             (f : ∀ s₁ s₂ s₃ → B (Qu₁.abs s₁) (Qu₂.abs s₂) (Qu₃.abs s₃)) where

     compat₃ : Set _
     compat₃ = ∀ {a b c a′ b′ c′} → a S₁.≈ a′ → b S₂.≈ b′ → c S₃.≈ c′ →
               f a b c ≅ f a′ b′ c′

     lift₃ : compat₃ → ∀ q₁ q₂ q₃ → B q₁ q₂ q₃
     lift₃ p = Qu₁.lift _ h (ext ∘ h-ext) module Lift₃ where

       g : ∀ a b q → B (Qu₁.abs a) (Qu₂.abs b) q
       g a b = Qu₃.lift (B (Qu₁.abs a) (Qu₂.abs b)) (f a b) (p S₁.refl S₂.refl)

       g-ext : ∀ {a a′ b b′} → a S₁.≈ a′ → b S₂.≈ b′ → ∀ c → g a b c ≅ g a′ b′ c
       g-ext a≈a′ b≈b′ = Properties.lift-ext Qu₃ (λ _ → p a≈a′ b≈b′ S₃.refl)

       h : ∀ a q₂ q₃ → B (Qu₁.abs a) q₂ q₃
       h a = Qu₂.lift (λ b → ∀ q → B (Qu₁.abs a) b q) (g a) (ext ∘ g-ext S₁.refl)

       h-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ b → h a b ≅ h a′ b
       h-ext a≈a′ = Properties.lift-ext Qu₂ $ λ _ → ext (g-ext a≈a′ S₂.refl)