{-# OPTIONS --postfix-projections --prop #-}

module TwoLevel where

open import Agda.Primitive
open import Lib
open import Fam as _
open import Id as _
open import Pi as _

-----------------------------------------------
--- Two-level families / Higher congruences ---
-----------------------------------------------

record TwoLevelFam {i j} : Set (lsuc i ⊔ lsuc j) where
  field Tyᵒ : Set i
        Tmᵒ : Tyᵒ → Set j

  Outer : Fam
  Outer = record { Ty = Tyᵒ ; Tm = Tmᵒ }

  field ty : Tyᵒ
  Ty = Tmᵒ ty

  field tm : Ty → Tyᵒ
  Tm : Ty → Set j
  Tm A = Tmᵒ (tm A)

  Inner : Fam
  Inner = record { Ty = Ty ; Tm = Tm }

  field instance OuterId-Intro : Id-Intro Outer
  field instance OuterId-Elim : Id-Elim Outer ⦃ CId = OuterId-Intro ⦄ Outer ⦃ DId = OuterId-Intro ⦄

  field OuterPi : Pi-StrictBeta Inner Outer ⦃ DId = OuterId-Intro ⦄ ⦃ DId-Elim-D = OuterId-Elim ⦄

--- Given any family C, (C ⁼) is a higher congruence on C whose outer identity
---  types are interpreted by the strict (metatheoretic) equality of C.
module _ {i j} (C : Fam {i} {j}) where
  private
    module C = Fam C

  _⁼ : TwoLevelFam {lsuc (i ⊔ j)} {i ⊔ j}
  _⁼ .TwoLevelFam.Tyᵒ  = Set (i ⊔ j)
  _⁼ .TwoLevelFam.Tmᵒ A = A

  _⁼ .TwoLevelFam.ty   = Lift {i} {i ⊔ j} C.Ty
  _⁼ .TwoLevelFam.tm A = Lift {j} {i ⊔ j} (C.Tm (A .lower))

  _⁼ .TwoLevelFam.OuterId-Intro .Id-Intro.Id {A} x y              = x ≡ y
  _⁼ .TwoLevelFam.OuterId-Intro .Id-Intro.idp {A} {x}             = refl
  _⁼ .TwoLevelFam.OuterId-Elim .Id-Elim.J {A} {.y} P d (y , refl) = d
  _⁼ .TwoLevelFam.OuterId-Elim .Id-Elim.J-β {A} {x} {P} {d}       = refl

  _⁼ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-intro .Pi-Intro.Π A B                            = (a : C.Tm (A .lower)) → B (lift a)
  _⁼ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-intro .Pi-Intro.lam b                            = λ a → b (lift a)
  _⁼ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-app-strict .Pi-App-Strict.app f a                = f (a .lower)
  _⁼ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-app-strict .Pi-App-Strict.app-βₛ {A} {B} {f} {a} = refl
  _⁼ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-funext                                           = cheat -- This can be defined using the metatheoretic funext.

--- Given any family C with Id and Pi type structures, (C ͌) is a higher
---  congruence on C whose outer identity types are interpreted by the internal
---  equality (identity types) of C.
module _ {i j} (C : Fam {i} {j}) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim : Id-Elim C C ⦄ ⦃ CPi : Pi-StrictBeta C C ⦄
         (U : C .Fam.Ty) (El : C .Fam.Tm U → C .Fam.Ty) -- We need this universe because we don't assume that C is a cumulative family
         where
  private
    module C = Fam C
    open Pi-StrictBeta CPi

  _͌ : TwoLevelFam {i} {j}
  _͌ .TwoLevelFam.Tyᵒ = C.Ty
  _͌ .TwoLevelFam.Tmᵒ = C.Tm
  _͌ .TwoLevelFam.ty  = U
  _͌ .TwoLevelFam.tm  = El

  _͌ .TwoLevelFam.OuterId-Intro = CId
  _͌ .TwoLevelFam.OuterId-Elim  = CId-Elim

  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-intro .Pi-Intro.Π                 = λ A B → Π (El A) B
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-intro .Pi-Intro.lam               = lam
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-app-strict .Pi-App-Strict.app     = app
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-app-strict .Pi-App-Strict.app-βₛ  = app-βₛ
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-funext .Pi-Funext.funext          = funext
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-funext .Pi-Funext.funext-β        = funext-β
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-funext .Pi-Funext.happly-funext   = happly-funext
  _͌ .TwoLevelFam.OuterPi .Pi-StrictBeta.Pi-funext .Pi-Funext.happly-funext-β = happly-funext-β