{-# OPTIONS --postfix-projections --prop --rewriting #-}
module Cong-Quotient where

open import Agda.Primitive

open import Lib
open import Quotient
open import Fam as _
open import Id
open import Pi
open import Cong

module _ {ic' jc' ic jc} (C : Fam {ic} {jc}) (C~ : Cong-Fam {ic'} {jc'} C) where
  private
    module C  = Fam C
    module C~ = Cong-Fam C~

  Tyq : Set ic
  Tyq = C.Ty // C~.Ty~

  quot-Ty : C.Ty → Tyq
  quot-Ty = //-in _ _

  quot-Ty-≡-out : ∀ {A B} → quot-Ty A ≡ quot-Ty B → C~.Ty~ A B
  quot-Ty-≡-out = //-≡-out _ _ C~.EqRel-Ty~

  Tmq0 : Tyq → Set (ic ⊔ jc)
  Tmq0 A = Σ C.Ty λ B → (quot-Ty B ≡ A) × C.Tm B

  Tmq1 : ∀ {A} → Tmq0 A → Tmq0 A → Prop jc'
  Tmq1 (B₁ , p₁ , x₁) (B₂ , p₂ , x₂) = C~.Tm~ (quot-Ty-≡-out (p₁ L.∙ L.! p₂)) x₁ x₂

  Tmq : Tyq → Set (ic ⊔ jc)
  Tmq A = Tmq0 A // Tmq1

  Quot-Fam : Fam {_} {_}
  Quot-Fam .Fam.Ty = Tyq
  Quot-Fam .Fam.Tm = Tmq

  quot-Tm : ∀ {A} → C.Tm A → Quot-Fam .Fam.Tm (quot-Ty A)
  quot-Tm x = //-in _ _ (_ , refl , x)