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

open import Agda.Primitive

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

--------------------------------------------------
--- Fibrant congruence over an internal family ---
--------------------------------------------------
-- The definition is split into two parts (similar to how identity types are
-- split into introduction and elimination structures) :
--   PreCong-Fam C consists of equivalence relations on types and terms of the
--     families, such that the setoid of terms is fibrant over the setoid of
--     types.
--   PreCong-Ap {C} C~ {D} D~ consists of compatibility conditions on
--     congruences C~ and D~ for the types and terms of D dependent over C.
--
--  A congruence over C consists of C~ : PreCong-Fam C and C~-ap : PreCong-Ap C~ C~.

record PreCong-Fam {ic' jc' ic jc} (C : Fam {ic} {jc}) : Set (lsuc (ic ⊔ jc ⊔ ic' ⊔ jc')) where
  module C = Fam C
  -- Equivalence relation on Ty
  field Ty~ : C.Ty → C.Ty → Prop ic'
        Ty~R : ∀ {A} → Ty~ A A
        Ty~S : ∀ {A B} → Ty~ A B → Ty~ B A
        Ty~T : ∀ {A B C} → Ty~ A B → Ty~ B C → Ty~ A C
  -- Dependent equivalence relation on Tm
        Tm~ : ∀ {A B} → Ty~ A B → (a : C.Tm A) → (b : C.Tm B) → Prop jc'
        Tm~R : ∀ {A a} → Tm~ (Ty~R {A}) a a
        Tm~S : ∀ {A B p a b} → Tm~ {A} {B} p a b → Tm~ (Ty~S p) b a
        Tm~T : ∀ {A B C p q a b c} → Tm~ {A} {B} p a b → Tm~ {B} {C} q b c → Tm~ (Ty~T p q) a c
  -- Fibrancy condition
        Tm~fib : ∀ {A B} (p : Ty~ A B) (a : C.Tm A) → ∥ ΣPS (C.Tm B) (λ b → Tm~ p a b) ∥

  EqRel-Ty~ : EqRel Ty~
  EqRel-Ty~ = record { R = Ty~R ; S = Ty~S ; T = Ty~T }

  EqRel-Tm~ : ∀ {A} → EqRel (Tm~ (Ty~R {A}))
  EqRel-Tm~ = record { R = Tm~R ; S = Tm~S ; T = Tm~T }

  Ty⋆~ : ∀ {n} → (LIxTele n C) .Fam.Ty → (LIxTele n C) .Fam.Ty → Prop (ic' ⊔ jc' ⊔ jc)
  Tm⋆~ : ∀ {n A B} → Ty⋆~ {n} A B → (LIxTele n C) .Fam.Tm A → (LIxTele n C) .Fam.Tm B → Prop jc'

  Ty⋆~ {zero}  _       _       = ⊤p
  Ty⋆~ {suc n} (Γ , A) (Δ , B) = ΣP (Ty⋆~ {n} Γ Δ) (λ A~ → ∀ γ δ → Tm⋆~ A~ γ δ → Ty~ (A γ) (B δ))
  Tm⋆~ {zero}  _         _         _         = ⊤p
  Tm⋆~ {suc n} (A~ , B~) (a₁ , b₁) (a₂ , b₂) = ΣP (Tm⋆~ A~ a₁ a₂) (λ a~ → Tm~ (B~ _ _ a~) b₁ b₂)

record PreCong-Ap {ic jc ic' jc'} {C : Fam {ic} {jc}} (C~ : PreCong-Fam {ic'} {jc'} C)
                  (n : ℕ) (Ty⋆~R : ∀ {A} → PreCong-Fam.Ty⋆~ C~ {n} A A)
                  : Set (ic ⊔ jc ⊔ ic' ⊔ jc') where
  coinductive
  private
    module C = Fam C
    module C~ = PreCong-Fam C~

  field ap-Ty : ∀ {A : LIxTele n C .Fam.Ty} (B : (LIxTele n C) .Fam.Tm A → C.Ty)
                  {x y} (p : C~.Tm⋆~ Ty⋆~R x y)
                → C~.Ty~ (B x) (B y)
        ap-Tm : ∀ {A : LIxTele n C .Fam.Ty} (B : (LIxTele n C) .Fam.Tm A → C.Ty) (b : ∀ a → C.Tm (B a))
                  {x y} (p : C~.Tm⋆~ Ty⋆~R x y)
                → C~.Tm~ (ap-Ty B p) (b x) (b y)

  field ap-next : PreCong-Ap C~ (suc n) (Ty⋆~R , (λ γ δ x → ap-Ty _ x))

record Cong-Fam {ic' jc' ic jc} (C : Fam {ic} {jc}) : Set (lsuc (ic ⊔ jc ⊔ ic' ⊔ jc')) where
  field C~ : PreCong-Fam {ic'} {jc'} C
        C~-ap : PreCong-Ap C~ zero _
  open PreCong-Fam C~ public

--------------------------------------------------------------------
--- Compatibility of a congruence with type-theoretic structures ---
--------------------------------------------------------------------

record Cong-Id-Intro {ic' jc' ic jc} {C : Fam {ic} {jc}} (C~ : Cong-Fam {ic'} {jc'} C) ⦃ CId : Id-Intro C ⦄ : Prop (ic ⊔ jc ⊔ ic' ⊔ jc') where
  private
    module C   = Fam C
    module C~  = Cong-Fam C~
    open Id-Intro CId
  field Id~ : ∀ {A₁ A₂ x₁ x₂ y₁ y₂} (A~ : C~.Ty~ A₁ A₂) (x~ : C~.Tm~ A~ x₁ x₂) (y~ : C~.Tm~ A~ y₁ y₂)
            → C~.Ty~ (Id x₁ y₁) (Id x₂ y₂)
        idp~ : ∀ {A₁ A₂ x₁ x₂} (A~ : C~.Ty~ A₁ A₂) (x~ : C~.Tm~ A~ x₁ x₂)
             → C~.Tm~ (Id~ A~ x~ x~) (idp {x = x₁}) (idp {x = x₂})

record Cong-Id-Elim {ic' jc' ic jc} {C : Fam {ic} {jc}} (C~ : Cong-Fam {ic'} {jc'} C) ⦃ CId : Id-Intro C ⦄ (CId~ : Cong-Id-Intro C~) ⦃ CId-Elim-C : Id-Elim C C ⦄ : Prop (ic ⊔ jc ⊔ ic' ⊔ jc') where
  private
    module C  = Fam C
    module C~ = Cong-Fam C~
    open Id-Intro CId
    open Id-Elim CId-Elim-C
    open Cong-Id-Intro CId~
  field J~ : ∀ {A₁ A₂ x₁ x₂ P₁ P₂ d₁ d₂ y₁ y₂ p₁ p₂} (A~ : C~.Ty~ A₁ A₂) (x~ : C~.Tm~ A~ x₁ x₂)
               (P~ : ∀ {y₁ y₂} y~ {p₁ p₂} (p~ : C~.Tm~ (Id~ A~ x~ y~) p₁ p₂) → C~.Ty~ (P₁ (y₁ , p₁)) (P₂ (y₂ , p₂)))
               (d~ : C~.Tm~ (P~ x~ (idp~ A~ x~)) d₁ d₂)
               (y~ : C~.Tm~ A~ y₁ y₂) (p~ : C~.Tm~ (Id~ A~ x~ y~) p₁ p₂)
             → C~.Tm~ (P~ y~ p~) (J {A₁} {x₁} P₁ d₁ (y₁ , p₁)) (J {A₂} {x₂} P₂ d₂ (y₂ , p₂))
        J-β~ : ∀ {A₁ A₂ x₁ x₂ P₁ P₂ d₁ d₂} (A~ : C~.Ty~ A₁ A₂) (x~ : C~.Tm~ A~ x₁ x₂)
                 (P~ : ∀ {y₁ y₂} (y~ : C~.Tm~ A~ y₁ y₂) {p₁ p₂} (p~ : C~.Tm~ (Id~ A~ x~ y~) p₁ p₂) → C~.Ty~ (P₁ (y₁ , p₁)) (P₂ (y₂ , p₂)))
                 (d~ : C~.Tm~ (P~ x~ (idp~ A~ x~)) d₁ d₂)
               → C~.Tm~ (Id~ (P~ x~ (idp~ A~ x~)) (J~ A~ x~ P~ d~ x~ (idp~ A~ x~)) d~) (J-β {A₁} {x₁} {P₁} {d₁}) (J-β {A₂} {x₂} {P₂} {d₂})

record Cong-Pi-Intro {ic' jc' ic jc} {C : Fam {ic} {jc}} (C~ : Cong-Fam {ic'} {jc'} C) ⦃ CPi-Intro : Pi-Intro C C ⦄ : Prop (ic ⊔ jc ⊔ ic' ⊔ jc') where
  private
    module C = Fam C
    module C~ = Cong-Fam C~
    open Pi-Intro CPi-Intro
  field Π~ : ∀ {A₁ A₂ B₁ B₂} (A~ : C~.Ty~ A₁ A₂) (B~ : ∀ {a₁ a₂} → C~.Tm~ A~ a₁ a₂ → C~.Ty~ (B₁ a₁) (B₂ a₂))
            → C~.Ty~ (Π A₁ B₁) (Π A₂ B₂)
        lam~ : ∀ {A₁ A₂ B₁ B₂ b₁ b₂} (A~ : C~.Ty~ A₁ A₂) (B~ : ∀ {a₁ a₂} (a~ : C~.Tm~ A~ a₁ a₂) → C~.Ty~ (B₁ a₁) (B₂ a₂))
                 (b~ : ∀ {a₁ a₂} (a~ : C~.Tm~ A~ a₁ a₂) → C~.Tm~ (B~ a~) (b₁ a₁) (b₂ a₂))
               → C~.Tm~ (Π~ A~ B~) (lam {B = B₁} b₁) (lam {B = B₂} b₂)

record Cong-Pi-App {ic' jc' ic jc} {C : Fam {ic} {jc}} (C~ : Cong-Fam {ic'} {jc'} C) ⦃ CId : Id-Intro C ⦄ (CId~ : Cong-Id-Intro C~)
                   ⦃ CPi-Intro : Pi-Intro C C ⦄ (CPi~ : Cong-Pi-Intro C~) ⦃ CPi-App : Pi-App C C ⦄ : Prop (ic ⊔ jc ⊔ ic' ⊔ jc') where
  private
    module C = Fam C
    module C~ = Cong-Fam C~
    open Pi-Intro CPi-Intro
    open Cong-Pi-Intro CPi~
    open Pi-App CPi-App
    open Cong-Id-Intro CId~
  field app~ : ∀ {A₁ A₂ B₁ B₂ f₁ f₂ a₁ a₂} (A~ : C~.Ty~ A₁ A₂) (B~ : ∀ {a₁ a₂} → C~.Tm~ A~ a₁ a₂ → C~.Ty~ (B₁ a₁) (B₂ a₂))
                 (f~ : C~.Tm~ (Π~ A~ B~) f₁ f₂) (a~ : C~.Tm~ A~ a₁ a₂)
               → C~.Tm~ (B~ a~) (app {A₁} {B₁} f₁ a₁) (app {A₂} {B₂} f₂ a₂)
        app-β~ : ∀ {A₁ A₂ B₁ B₂ b₁ b₂ a₁ a₂} (A~ : C~.Ty~ A₁ A₂) (B~ : ∀ {a₁ a₂} → C~.Tm~ A~ a₁ a₂ → C~.Ty~ (B₁ a₁) (B₂ a₂))
                   (b~ : ∀ {a₁ a₂} (a~ : C~.Tm~ A~ a₁ a₂) → C~.Tm~ (B~ a~) (b₁ a₁) (b₂ a₂)) (a~ : C~.Tm~ A~ a₁ a₂)
                 → C~.Tm~ (Id~ (B~ a~) (app~ A~ B~ (lam~ A~ B~ b~) a~) (b~ a~)) (app-β {A₁} {B₁} {b₁} {a₁}) (app-β {A₂} {B₂} {b₂} {a₂})