{-# OPTIONS --prop --rewriting #-}

module depModel where

open import lib
open import model
open import morphism

-- Dependent CwF over C
-- Equivalent to the data of a CwF D and a CwF morphism D → C

record DepCwF {i}{i'}{j}{j'}{k}{k'}{l}{l'} (C : CwF {i}{j}{k}{l}) : Set (i ⊔ j ⊔ k ⊔ l ⊔ lsuc i' ⊔ lsuc j' ⊔ lsuc k' ⊔ lsuc l') where
  infixl  _∘∙_
  infixl  _,[_][_]∙_
  infixl  _[_]T∙ _[_]t∙
  infixl  _▹∙_
  module Ci = CwF C
  field
    Con∙      : Ci.Con → Set i'
    Sub∙      : ∀{Δ} → Con∙ Δ → ∀{Γ} → Con∙ Γ → Ci.Sub Δ Γ → Set j'
    _∘∙_      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ} → Sub∙ Δ∙ Γ∙ γ → ∀{Θ}{Θ∙ : Con∙ Θ}{δ}
                → Sub∙ Θ∙ Δ∙ δ → Sub∙ Θ∙ Γ∙ (Ci._∘_ {Γ = Γ}{Δ = Δ} γ {Θ = Θ} δ)
    ass∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{Θ}{Θ∙ : Con∙ Θ}{δ}{δ∙ : Sub∙ Θ∙ Δ∙ δ}
                {Ξ}{Ξ∙ : Con∙ Ξ}{θ}{θ∙ : Sub∙ Ξ∙ Θ∙ θ} → ((γ∙ ∘∙ δ∙) ∘∙ θ∙) ~ (γ∙ ∘∙ (δ∙ ∘∙ θ∙))
    id∙       : ∀{Γ}{Γ∙ : Con∙ Γ} → Sub∙ Γ∙ Γ∙ (Ci.id {Γ})
    idl∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ} → (id∙ ∘∙ γ∙) ~ γ∙
    idr∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ} → (γ∙ ∘∙ id∙) ~ γ∙
    ◇∙        : Con∙ Ci.◇
    ε∙        : ∀{Γ}{Γ∙ : Con∙ Γ} → Sub∙ Γ∙ ◇∙ (Ci.ε {Γ})
    ◇η∙       : ∀{Γ}{Γ∙ : Con∙ Γ}{σ}{σ∙ : Sub∙ Γ∙ ◇∙ σ} → σ∙ ~ ε∙ {Γ∙ = Γ∙}
    Ty∙       : ∀{Γ} → Con∙ Γ → Ci.Ty Γ → Set k'
    _[_]T∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A} → Ty∙ Γ∙ A → ∀{Δ}{Δ∙ : Con∙ Δ}{γ} → Sub∙ Δ∙ Γ∙ γ → Ty∙ Δ∙ (Ci._[_]T {Γ = Γ} A {Δ = Δ} γ)
    [∘]T∙     : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{Θ}{Θ∙ : Con∙ Θ}{δ}{δ∙ : Sub∙ Θ∙ Δ∙ δ}
                → A∙ [ γ∙ ∘∙ δ∙ ]T∙ ~ A∙ [ γ∙ ]T∙ [ δ∙ ]T∙
    [id]T∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A} → A∙ [ id∙ ]T∙ ~ A∙
    Tm∙       : ∀{Γ}(Γ∙ : Con∙ Γ){A} → Ty∙ Γ∙ A → Ci.Tm Γ A → Set l'
    _[_]t∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a} → Tm∙ Γ∙ A∙ a → ∀{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ)
                → Tm∙ Δ∙ (A∙ [ γ∙ ]T∙) (Ci._[_]t {Γ = Γ}{A = A} a {Δ = Δ} γ)
    [∘]t∙     : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a}{a∙ : Tm∙ Γ∙ A∙ a}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{Θ}{Θ∙ : Con∙ Θ}
                {δ}{δ∙ : Sub∙ Θ∙ Δ∙ δ} → a∙ [ γ∙ ∘∙ δ∙ ]t∙ ~ a∙ [ γ∙ ]t∙ [ δ∙ ]t∙
    [id]t∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a}{a∙ : Tm∙ Γ∙ A∙ a} → a∙ [ id∙ ]t∙ ~ a∙
    _▹∙_      : ∀{Γ}(Γ∙ : Con∙ Γ){A} → Ty∙ Γ∙ A → Con∙ (Γ Ci.▹ A)
    _,[_][_]∙_ : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ){A}{A∙ : Ty∙ Γ∙ A}{A'}{A'∙ : Ty∙ Δ∙ A'}(e : A Ci.[ γ ]T ~ A')
                 → A∙ [ γ∙ ]T∙ ~ A'∙ → ∀{a} → Tm∙ Δ∙ A'∙ a → Sub∙ Δ∙ (Γ∙ ▹∙ A∙) (Ci._,[_]_ {Γ}{Δ} γ {A} e a)
    p∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A} → Sub∙ (Γ∙ ▹∙ A∙) Γ∙ (Ci.p {Γ}{A})
    q∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A} → Tm∙ (Γ∙ ▹∙ A∙) (A∙ [ p∙ ]T∙) (Ci.q {Γ}{A})
    ▹β₁∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{A}{A∙ : Ty∙ Γ∙ A}{a}{a∙ : Tm∙ Δ∙ (A∙ [ γ∙ ]T∙) a}
                → p∙ ∘∙ (γ∙ ,[ ~refl ][ ~refl ]∙ a∙) ~ γ∙
    ▹β₂∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{A}{A∙ : Ty∙ Γ∙ A}{a}{a∙ : Tm∙ Δ∙ (A∙ [ γ∙ ]T∙) a}
                → q∙ [ γ∙ ,[ ~refl ][ ~refl ]∙ a∙ ]t∙ ~ a∙
    ▹η∙       : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{A}{A∙ : Ty∙ Γ∙ A}{γa}{γa∙ : Sub∙ Δ∙ (Γ∙ ▹∙ A∙) γa}
                → ((p∙ ∘∙ γa∙) ,[ Ci.[∘]T ][ [∘]T∙ ]∙ (q∙ [ γa∙ ]t∙)) ~ γa∙

-- mostly a parametricity translation of CwF-tools, with a few extras
module DepCwF-tools {i i' j j' k k' l l' : Level} (Ci : CwF {i}{j}{k}{l}) (C : DepCwF {i}{i'}{j}{j'}{k}{k'}{l}{l'} Ci) where
  open CwF Ci
  open CwF-tools Ci
  open DepCwF C

  coeTm∙ : ∀ {Γ}(Γ∙ : Con∙ Γ){A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ Γ∙ B}(e : A ~ B)(e∙ : A∙ ~ B∙){t} → Tm∙ Γ∙ A∙ t → Tm∙ Γ∙ B∙ (coe (cong (Tm Γ) e) t)
  coeTm∙ {Γ} Γ∙ e e∙ {t} t∙ = coe (cong₃ (λ A → Tm∙ Γ∙ {A = A}) e e∙ (coe-eq (cong (Tm Γ) e) t)) t∙

  coeTm∙-eq : ∀ {Γ}(Γ∙ : Con∙ Γ){A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ Γ∙ B}(e : A ~ B)(e∙ : A∙ ~ B∙){t}(t∙ : Tm∙ Γ∙ A∙ t)
            → t∙ ~ coeTm∙ Γ∙ e e∙ t∙
  coeTm∙-eq {Γ} Γ∙ e e∙ {t} t∙ = coe-eq (cong₃ (λ A → Tm∙ Γ∙ {A = A}) e e∙ (coe-eq (cong (Tm Γ) e) t)) t∙

  -- proving two extended substitutions equal
  cong-subExt∙ : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{γ'}{γ'∙ : Sub∙ Δ∙ Γ∙ γ'}(γe : γ ~ γ')(γe∙ : γ∙ ~ γ'∙)
                 {A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ Δ∙ B}{B'}{B'∙ : Ty∙ Δ∙ B'}(Be : B ~ B')(Be∙ : B∙ ~ B'∙)
                 (e : A [ γ ]T ~ B)(e∙ : A∙ [ γ∙ ]T∙ ~ B∙)(e' : A [ γ' ]T ~ B')(e'∙ : A∙ [ γ'∙ ]T∙ ~ B'∙)
                 {a}{a∙ : Tm∙ Δ∙ B∙ a}{a'}{a'∙ : Tm∙ Δ∙ B'∙ a'}(ae : a ~ a')(ae∙ : a∙ ~ a'∙)
                 → γ∙ ,[ e ][ e∙ ]∙ a∙ ~ γ'∙ ,[ e' ][ e'∙ ]∙ a'∙
  cong-subExt∙ ~refl ~refl ~refl ~refl e e∙ e' e'∙ ~refl ~refl = ~refl

  -- β₁ but with arbitrary equalities
  ▹β₁-EX∙ : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{A}{A∙ : Ty∙ Γ∙ A}{A'}{A'∙ : Ty∙ Δ∙ A'}
            {e : A [ γ ]T ~ A'}{e∙ : A∙ [ γ∙ ]T∙ ~ A'∙}{a}{a∙ : Tm∙ Δ∙ A'∙ a} → p∙ ∘∙ (γ∙ ,[ e ][ e∙ ]∙ a∙) ~ γ∙
  ▹β₁-EX∙ {Γ}{Γ∙}{Δ}{Δ∙}{γ}{γ∙}{A}{A∙}{A'}{A'∙}{e}{e∙}{a}{a∙} =
    let
      a' = coe (cong (Tm Δ) (e ⁻¹)) a
      a'∙ = coeTm∙ Δ∙ (e ⁻¹) (e∙ ⁻¹) a∙
      a≡a' = coe-eq (cong (Tm Δ) (e ⁻¹)) a
      a≡a'∙ = coeTm∙-eq Δ∙ (e ⁻¹) (e∙ ⁻¹) a∙
      e₀ : (γ ,[ e ] a) ~ (γ ,[ ~refl ] a')
      e₀ = congᵣᵣᵣᵢᵣ (λ a b c d e → _,[_]_ {Γ} {Δ} a {b} {c} d e) ~refl ~refl (e ⁻¹) a≡a'
      e₀∙ : (γ∙ ,[ e ][ e∙ ]∙ a∙) ~ (γ∙ ,[ ~refl ][ ~refl ]∙ a'∙)
      e₀∙ = cong-subExt∙ ~refl ~refl (e ⁻¹) (e∙ ⁻¹) _ _ _ _ a≡a' a≡a'∙
    in (cong₂ (λ δ → _∘∙_ (p∙ {A∙ = A∙}) {Θ∙ = Δ∙} {δ = δ}) e₀ e₀∙) ◼ ▹β₁∙

  -- β₂ but with arbitrary equalities
  ▹β₂-EX∙ : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}{A}{A∙ : Ty∙ Γ∙ A}{A'}{A'∙ : Ty∙ Δ∙ A'}
            {e : A [ γ ]T ~ A'}{e∙ : A∙ [ γ∙ ]T∙ ~ A'∙}{a}{a∙ : Tm∙ Δ∙ A'∙ a} → q∙ [ γ∙ ,[ e ][ e∙ ]∙ a∙ ]t∙ ~ a∙
  ▹β₂-EX∙ {Γ}{Γ∙}{Δ}{Δ∙}{γ}{γ∙}{A}{A∙}{A'}{A'∙}{e}{e∙}{a}{a∙} =
    let
      a' = coe (cong (Tm Δ) (e ⁻¹)) a
      a'∙ = coeTm∙ Δ∙ (e ⁻¹) (e∙ ⁻¹) a∙
      a≡a' = coe-eq (cong (Tm Δ) (e ⁻¹)) a
      a≡a'∙ = coeTm∙-eq Δ∙ (e ⁻¹) (e∙ ⁻¹) a∙
      e₀ : (γ ,[ e ] a) ~ (γ ,[ ~refl ] a')
      e₀ = congᵣᵣᵣᵢᵣ (λ a b c d e → _,[_]_ {Γ} {Δ} a {b} {c} d e) ~refl ~refl (e ⁻¹) a≡a'
      e₀∙ : (γ∙ ,[ e ][ e∙ ]∙ a∙) ~ (γ∙ ,[ ~refl ][ ~refl ]∙ a'∙)
      e₀∙ = cong-subExt∙ ~refl ~refl (e ⁻¹) (e∙ ⁻¹) _ _ _ _ a≡a' a≡a'∙
    in cong₂ (λ γ → _[_]t∙ (q∙ {A∙ = A∙}) {Δ∙ = Δ∙} {γ = γ}) e₀ e₀∙ ◼ ▹β₂∙ ◼ a≡a'∙ ⁻¹

  -- substitution lift
  ↑∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ) → Sub∙ (Δ∙ ▹∙ A∙ [ γ∙ ]T∙) (Γ∙ ▹∙ A∙) (↑ γ)
  ↑∙ γ∙ = γ∙ ∘∙ p∙ ,[ [∘]T ][ [∘]T∙ ]∙ q∙

  -- singleton substitution
  sg∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a}(a∙ : Tm∙ Γ∙ A∙ a) → Sub∙ Γ∙ (Γ∙ ▹∙ A∙) (sg a)
  sg∙ a∙ = id∙ ,[ [id]T ][ [id]T∙ ]∙ a∙

  ε[]T∙ : ∀ {A}{A∙ : Ty∙ ◇∙ A}{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ} → A∙ [ ε∙ ]T∙ [ γ∙ ]T∙ ~ A∙ [ ε∙ ]T∙
  ε[]T∙ {A}{A∙}{Δ∙ = Δ∙} = ([∘]T∙ ⁻¹) ◼ cong₂ (λ f → _[_]T∙ A∙ {Δ∙ = Δ∙} {γ = f}) ◇η ◇η∙

  -- variation on ↑
  ↑ε∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ ◇∙ A}{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ) → (Sub∙ (Δ∙ ▹∙ A∙ [ ε∙ ]T∙) (Γ∙ ▹∙ A∙ [ ε∙ ]T∙)) (↑ε γ)
  ↑ε∙ {Γ}{Γ∙}{A}{A∙}{Δ} γ∙ = γ∙ ∘∙ p∙ ,[ ε[]T ◼ ε[]T ⁻¹ ][ ε[]T∙ ◼ ε[]T∙ ⁻¹ ]∙ q∙

  -- composition with an extended substitution on the left (uses η)
  subExt∘∙ : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{Θ}{Θ∙ : Con∙ Θ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ){A}{A∙ : Ty∙ Γ∙ A}{A'}{A'∙ : Ty∙ Δ∙ A'}
             (e : A [ γ ]T ~ A')(e∙ : A∙ [ γ∙ ]T∙ ~ A'∙){a}(a∙ : Tm∙ Δ∙ A'∙ a){δ}(δ∙ : Sub∙ Θ∙ Δ∙ δ)
             → (γ∙ ,[ e ][ e∙ ]∙ a∙) ∘∙ δ∙ ~ (γ∙ ∘∙ δ∙) ,[ [∘]T ◼ cong (λ A → A [ δ ]T) e ][ [∘]T∙ ◼ cong₂ (λ A A∙ → _[_]T∙ {A = A} A∙ δ∙) e e∙ ]∙ a∙ [ δ∙ ]t∙
  subExt∘∙ {Γ}{Γ∙}{Δ}{Δ∙}{Θ}{Θ∙}{γ} γ∙ {A}{A∙} e e∙ {a} a∙ {δ} δ∙ =
    ▹η∙ ⁻¹
    ◼ cong-subExt∙ e₀ e₀∙
        ([∘]T ⁻¹ ◼ cong (λ f → A [ f ]T) e₀ ◼ [∘]T)
        ([∘]T∙ ⁻¹ ◼ cong₂ (λ γ → _[_]T∙ A∙ {Δ∙ = Θ∙} {γ = γ}) e₀ e₀∙ ◼ [∘]T∙) _ _ _ _
        ([∘]t ◼ cong₂ (λ C (b : Tm Δ C) → b [ δ ]t) ([∘]T ⁻¹ ◼ cong (λ f → A [ f ]T) ▹β₁-EX ◼ e) ▹β₂-EX ◼ (▹β₂-EX ⁻¹))
        ([∘]t∙ ◼ cong₄ (λ A (A∙ : Ty∙ Δ∙ A) a (a∙ : Tm∙ Δ∙ A∙ a) → a∙ [ δ∙ ]t∙) ([∘]T ⁻¹ ◼ cong (λ f → A [ f ]T) ▹β₁-EX ◼ e)
                       ([∘]T∙ ⁻¹ ◼ cong₂ (λ γ → _[_]T∙ A∙ {γ = γ}) ▹β₁-EX ▹β₁-EX∙ ◼ e∙) ▹β₂-EX ▹β₂-EX∙
               ◼ (▹β₂-EX∙ ⁻¹))
    ◼ ▹η∙
    where
      e₀ : p ∘ ((γ ,[ e ] a) ∘ δ) ~ p ∘ (γ ∘ δ ,[ [∘]T ◼ cong (λ A → A [ δ ]T) e ] a [ δ ]t)
      e₀ = ass ⁻¹ ◼ cong (λ f → f ∘ δ) ▹β₁-EX ◼ (▹β₁-EX ⁻¹)

      e₀∙ : p∙ ∘∙ ((γ∙ ,[ e ][ e∙ ]∙ a∙) ∘∙ δ∙) ~ p∙ ∘∙ (γ∙ ∘∙ δ∙ ,[ [∘]T ◼ cong (λ A → A [ δ ]T) e ][ [∘]T∙ ◼ cong₂ (λ A A∙ → _[_]T∙ {A = A} A∙ δ∙) e e∙ ]∙ a∙ [ δ∙ ]t∙)
      e₀∙ = ass∙ ⁻¹ ◼ cong₂ (λ γ γ∙ → _∘∙_ {γ = γ} γ∙ δ∙) ▹β₁-EX ▹β₁-EX∙ ◼ ▹β₁-EX∙ ⁻¹

  -- commutation of ↑ε∙ and sg∙ (uses η)
  ↑ε-sg∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ ◇∙ A}{a}(a∙ : Tm∙ ◇∙ A∙ a){Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ)
         → (sg∙ (a∙ [ ε∙ ]t∙)) ∘∙ γ∙ ~ (↑ε∙ γ∙) ∘∙ (sg∙ (a∙ [ ε∙ ]t∙))
  ↑ε-sg∙ {Γ}{Γ∙}{A}{A∙}{a} a∙ {Δ}{Δ∙}{γ} γ∙ =
    subExt∘∙ id∙ _ _ (a∙ [ ε∙ ]t∙) γ∙
    ◼ cong-subExt∙ (idl ◼ idr ⁻¹ ◼ cong (_∘_ γ) (▹β₁-EX ⁻¹) ◼ ass ⁻¹)
                   (idl∙ ◼ idr∙ ⁻¹ ◼ cong₂ (λ δ → _∘∙_ γ∙ {Θ∙ = Δ∙} {δ = δ}) (▹β₁-EX ⁻¹) (▹β₁-EX∙ ⁻¹) ◼ ass∙ ⁻¹)
                   (ε[]T ◼ (ε[]T ⁻¹) ◼ [∘]T)
                   (ε[]T∙ ◼ (ε[]T∙ ⁻¹) ◼ [∘]T∙) _ _ _ _
                   ([∘]t ⁻¹ ◼ cong (_[_]t a) ◇η ◼ (▹β₂-EX ⁻¹))
                   ([∘]t∙ ⁻¹ ◼ cong₂ (λ γ → _[_]t∙ a∙ {Δ∙ = Δ∙} {γ = γ}) ◇η ◇η∙ ◼ ▹β₂-EX∙ ⁻¹)
    ◼ subExt∘∙ (γ∙ ∘∙ p∙) _ _ q∙ (sg∙ (a∙ [ ε∙ ]t∙)) ⁻¹

  Ty-↑ε-sg∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ ◇∙ A}{a}(a∙ : Tm∙ ◇∙ A∙ a){P}(P∙ : Ty∙ (Γ∙ ▹∙ A∙ [ ε∙ ]T∙) P){Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ)
           → P∙ [ sg∙ (a∙ [ ε∙ ]t∙) ]T∙ [ γ∙ ]T∙ ~ P∙ [ ↑ε∙ γ∙ ]T∙ [ sg∙ (a∙ [ ε∙ ]t∙) ]T∙
  Ty-↑ε-sg∙ {Γ}{Γ∙}{A}{A∙}{a} a∙ P∙ {Δ}{Δ∙}{γ} γ∙ = [∘]T∙ ⁻¹ ◼ cong₂ (λ γ → _[_]T∙ P∙ {Δ∙ = Δ∙} {γ = γ}) (↑ε-sg a γ) (↑ε-sg∙ a∙ γ∙) ◼ [∘]T∙


record DepModel {i i' j j' k k' l l' : Level} (Ci : CwF {i}{j}{k}{l}) (C : DepCwF {i}{i'}{j}{j'}{k}{k'}{l}{l'} Ci) (Mi : Model {i}{j}{k}{l} Ci)
                : Set (i ⊔ j ⊔ k ⊔ l ⊔ lsuc i' ⊔ lsuc j' ⊔ lsuc k' ⊔ lsuc l') where
  open CwF Ci
  open CwF-tools Ci
  open DepCwF C
  open DepCwF-tools Ci C
  open Model Mi
  field
    Π∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}(A∙ : Ty∙ Γ∙ A){B} → Ty∙ (Γ∙ ▹∙ A∙) B → Ty∙ Γ∙ (Π {Γ} A B)
    Π[]∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}
                → (Π∙ A∙ B∙) [ γ∙ ]T∙ ~ Π∙ (A∙ [ γ∙ ]T∙) (B∙ [ ↑∙ γ∙ ]T∙)
    lam∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{A}(A∙ : Ty∙ Γ∙ A){B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}(t∙ : Tm∙ (Γ∙ ▹∙ A∙) B∙ t) → Tm∙ Γ∙ (Π∙ A∙ B∙) (lam A t)
    lam[]∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}{t∙ : Tm∙ (Γ∙ ▹∙ A∙) B∙ t}{Δ}{Δ∙ : Con∙ Δ}
                {γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ} → (lam∙ A∙ t∙) [ γ∙ ]t∙ ~ lam∙ (A∙ [ γ∙ ]T∙) (t∙ [ ↑∙ γ∙ ]t∙)
    app∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}(t∙ : Tm∙ Γ∙ (Π∙ A∙ B∙) t){u}(u∙ : Tm∙ Γ∙ A∙ u)
                → Tm∙ Γ∙ (B∙ [ sg∙ u∙ ]T∙) (app t u)
    app[]∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}{t∙ : Tm∙ Γ∙ (Π∙ A∙ B∙) t}{u}{u∙ : Tm∙ Γ∙ A∙ u}
                {Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}
                → (app∙ t∙ u∙) [ γ∙ ]t∙ ~ app∙ (coeTm∙ Δ∙ Π[] Π[]∙ (t∙ [ γ∙ ]t∙)) (u∙ [ γ∙ ]t∙)
    Πβ∙       : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}{t∙ : Tm∙ (Γ∙ ▹∙ A∙) B∙ t}{a}{a∙ : Tm∙ Γ∙ A∙ a}
                → app∙ (lam∙ A∙ t∙) a∙ ~ t∙ [ sg∙ a∙ ]t∙
    Πη∙       : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}{t∙ : Tm∙ Γ∙ (Π∙ A∙ B∙) t}
                → t∙ ~ lam∙ A∙ {B∙ = B∙ [ ↑∙ p∙ ]T∙ [ sg∙ q∙ ]T∙} (app∙ (coeTm∙ (Γ∙ ▹∙ A∙) Π[] Π[]∙ (t∙ [ p∙ ]t∙)) q∙)
    𝔹∙        : Ty∙ ◇∙ 𝔹
    𝕥∙        : Tm∙ ◇∙ 𝔹∙ 𝕥
    𝕗∙        : Tm∙ ◇∙ 𝔹∙ 𝕗

    -- Large recursor
    ifᵀ∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{b}(b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b){A𝕥}(A𝕥∙ : Ty∙ Γ∙ A𝕥){A𝕗}(A𝕗∙ : Ty∙ Γ∙ A𝕗) → Ty∙ Γ∙ (ifᵀ b A𝕥 A𝕗)
    ifᵀ[]∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{b}{b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b}{A𝕥}{A𝕥∙ : Ty∙ Γ∙ A𝕥}{A𝕗}{A𝕗∙ : Ty∙ Γ∙ A𝕗}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}
                → (ifᵀ∙ b∙ A𝕥∙ A𝕗∙) [ γ∙ ]T∙ ~ ifᵀ∙ (coeTm∙ Δ∙ ε[]T ε[]T∙ (b∙ [ γ∙ ]t∙)) (A𝕥∙ [ γ∙ ]T∙) (A𝕗∙ [ γ∙ ]T∙)
    ifᵀβ₁∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A𝕥}{A𝕥∙ : Ty∙ Γ∙ A𝕥}{A𝕗}{A𝕗∙ : Ty∙ Γ∙ A𝕗} → ifᵀ∙ (𝕥∙ [ ε∙ ]t∙) A𝕥∙ A𝕗∙  ~ A𝕥∙
    ifᵀβ₂∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A𝕥}{A𝕥∙ : Ty∙ Γ∙ A𝕥}{A𝕗}{A𝕗∙ : Ty∙ Γ∙ A𝕗} → ifᵀ∙ (𝕗∙ [ ε∙ ]t∙) A𝕥∙ A𝕗∙  ~ A𝕗∙

    -- Small induction principle
    ifᵗ∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{P}(P∙ : Ty∙ (Γ∙ ▹∙ 𝔹∙ [ ε∙ ]T∙) P){P𝕥}(P𝕥∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕥∙ [ ε∙ ]t∙) ]T∙) P𝕥)
                {P𝕗}(P𝕗∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕗∙ [ ε∙ ]t∙) ]T∙) P𝕗){b}(b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b)
                → Tm∙ Γ∙ (P∙ [ sg∙ b∙ ]T∙) (ifᵗ P P𝕥 P𝕗 b)
    ifᵗ[]∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{P}{P∙ : Ty∙ (Γ∙ ▹∙ 𝔹∙ [ ε∙ ]T∙) P}{P𝕥}{P𝕥∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕥∙ [ ε∙ ]t∙) ]T∙) P𝕥}
                {P𝕗}{P𝕗∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕗∙ [ ε∙ ]t∙) ]T∙) P𝕗}{b}{b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b}{Δ}{Δ∙ : Con∙ Δ}{γ}{γ∙ : Sub∙ Δ∙ Γ∙ γ}
               → (ifᵗ∙ P∙ P𝕥∙ P𝕗∙ b∙) [ γ∙ ]t∙
                 ~ ifᵗ∙ (P∙ [ ↑ε∙ γ∙ ]T∙)
                        (coeTm∙ Δ∙ (Ty-↑ε-sg 𝕥 P γ) (Ty-↑ε-sg∙ 𝕥∙ P∙ γ∙) (P𝕥∙ [ γ∙ ]t∙))
                        (coeTm∙ Δ∙ (Ty-↑ε-sg 𝕗 P γ) (Ty-↑ε-sg∙ 𝕗∙ P∙ γ∙) (P𝕗∙ [ γ∙ ]t∙))
                        (coeTm∙ Δ∙ ε[]T ε[]T∙ (b∙ [ γ∙ ]t∙))
    ifᵗβ₁∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{P}{P∙ : Ty∙ (Γ∙ ▹∙ 𝔹∙ [ ε∙ ]T∙) P}{P𝕥}{P𝕥∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕥∙ [ ε∙ ]t∙) ]T∙) P𝕥}
                {P𝕗}{P𝕗∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕗∙ [ ε∙ ]t∙) ]T∙) P𝕗}
               → ifᵗ∙ P∙ P𝕥∙ P𝕗∙ (𝕥∙ [ ε∙ ]t∙) ~ P𝕥∙
    ifᵗβ₂∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{P}{P∙ : Ty∙ (Γ∙ ▹∙ 𝔹∙ [ ε∙ ]T∙) P}{P𝕥}{P𝕥∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕥∙ [ ε∙ ]t∙) ]T∙) P𝕥}
                {P𝕗}{P𝕗∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕗∙ [ ε∙ ]t∙) ]T∙) P𝕗}
               → ifᵗ∙ P∙ P𝕥∙ P𝕗∙ (𝕗∙ [ ε∙ ]t∙) ~ P𝕗∙

-- Then the Prop-valued version

record CwFPred {i}{i'}{j}{j'}{k}{k'}{l}{l'} (C : CwF {i}{j}{k}{l}) : Set (i ⊔ j ⊔ k ⊔ l ⊔ lsuc i' ⊔ lsuc j' ⊔ lsuc k' ⊔ lsuc l') where
  infixl  _∘∙_
  infixl  _,[_]∙_
  infixl  _[_]T∙ _[_]t∙
  infixl  _▹∙_
  module Ci = CwF C
  field
    Con∙      : Ci.Con → Prop i'
    Sub∙      : ∀{Δ} → Con∙ Δ → ∀{Γ} → Con∙ Γ → Ci.Sub Δ Γ → Prop j'
    _∘∙_      : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ} → Sub∙ Δ∙ Γ∙ γ → ∀{Θ}{Θ∙ : Con∙ Θ}{δ}
                → Sub∙ Θ∙ Δ∙ δ → Sub∙ Θ∙ Γ∙ (Ci._∘_ {Γ = Γ}{Δ = Δ} γ {Θ = Θ} δ)
    id∙       : ∀{Γ}{Γ∙ : Con∙ Γ} → Sub∙ Γ∙ Γ∙ (Ci.id {Γ})
    ◇∙        : Con∙ Ci.◇
    ε∙        : ∀{Γ}{Γ∙ : Con∙ Γ} → Sub∙ Γ∙ ◇∙ (Ci.ε {Γ})
    Ty∙       : ∀{Γ} → Con∙ Γ → Ci.Ty Γ → Prop k'
    _[_]T∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A} → Ty∙ Γ∙ A → ∀{Δ}{Δ∙ : Con∙ Δ}{γ} → Sub∙ Δ∙ Γ∙ γ → Ty∙ Δ∙ (Ci._[_]T {Γ = Γ} A {Δ = Δ} γ)
    Tm∙       : ∀{Γ}(Γ∙ : Con∙ Γ){A} → Ty∙ Γ∙ A → Ci.Tm Γ A → Prop l'
    _[_]t∙    : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a} → Tm∙ Γ∙ A∙ a → ∀{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ)
                → Tm∙ Δ∙ (A∙ [ γ∙ ]T∙) (Ci._[_]t {Γ = Γ}{A = A} a {Δ = Δ} γ)
    _▹∙_      : ∀{Γ}(Γ∙ : Con∙ Γ){A} → Ty∙ Γ∙ A → Con∙ (Γ Ci.▹ A)
    _,[_]∙_   : ∀{Γ}{Γ∙ : Con∙ Γ}{Δ}{Δ∙ : Con∙ Δ}{γ}(γ∙ : Sub∙ Δ∙ Γ∙ γ){A}{A∙ : Ty∙ Γ∙ A}{A'}{A'∙ : Ty∙ Δ∙ A'}(e : A Ci.[ γ ]T ~ A')
                 → ∀{a} → Tm∙ Δ∙ A'∙ a → Sub∙ Δ∙ (Γ∙ ▹∙ A∙) (Ci._,[_]_ {Γ}{Δ} γ {A} e a)
    p∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A} → Sub∙ (Γ∙ ▹∙ A∙) Γ∙ (Ci.p {Γ}{A})
    q∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A} → Tm∙ (Γ∙ ▹∙ A∙) (A∙ [ p∙ {Γ}{Γ∙}{A}{A∙} ]T∙) (Ci.q {Γ}{A})

module CwFPred-tools {i i' j j' k k' l l' : Level} (Ci : CwF {i}{j}{k}{l}) (C : CwFPred {i}{i'}{j}{j'}{k}{k'}{l}{l'} Ci) where
  open CwF Ci
  open CwF-tools Ci
  open CwFPred C

  sg∙ : ∀ {Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{a}(a∙ : Tm∙ Γ∙ A∙ a) → Sub∙ Γ∙ (Γ∙ ▹∙ A∙) (sg a)
  sg∙ {A∙ = A∙} a∙ = _,[_]∙_ id∙ {A∙ = A∙} [id]T a∙


record ModelPred {i i' j j' k k' l l' : Level} (Ci : CwF {i}{j}{k}{l}) (C : CwFPred {i}{i'}{j}{j'}{k}{k'}{l}{l'} Ci) (Mi : Model {i}{j}{k}{l} Ci)
                : Set (i ⊔ j ⊔ k ⊔ l ⊔ lsuc i' ⊔ lsuc j' ⊔ lsuc k' ⊔ lsuc l') where
  open CwF Ci
  open CwF-tools Ci
  open CwFPred C
  open CwFPred-tools Ci C
  open Model Mi
  field
    Π∙        : ∀{Γ}{Γ∙ : Con∙ Γ}{A}(A∙ : Ty∙ Γ∙ A){B} → Ty∙ (Γ∙ ▹∙ A∙) B → Ty∙ Γ∙ (Π {Γ} A B)
    lam∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{A}(A∙ : Ty∙ Γ∙ A){B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}(t∙ : Tm∙ (Γ∙ ▹∙ A∙) B∙ t) → Tm∙ Γ∙ (Π∙ A∙ B∙) (lam A t)
    app∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{A}{A∙ : Ty∙ Γ∙ A}{B}{B∙ : Ty∙ (Γ∙ ▹∙ A∙) B}{t}(t∙ : Tm∙ Γ∙ (Π∙ A∙ B∙) t){u}(u∙ : Tm∙ Γ∙ A∙ u)
                → Tm∙ Γ∙ (B∙ [ sg∙ u∙ ]T∙) (app t u)
    𝔹∙        : Ty∙ ◇∙ 𝔹
    𝕥∙        : Tm∙ ◇∙ 𝔹∙ 𝕥
    𝕗∙        : Tm∙ ◇∙ 𝔹∙ 𝕗
    ifᵀ∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{b}(b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b){A𝕥}(A𝕥∙ : Ty∙ Γ∙ A𝕥){A𝕗}(A𝕗∙ : Ty∙ Γ∙ A𝕗) → Ty∙ Γ∙ (ifᵀ b A𝕥 A𝕗)
    ifᵗ∙      : ∀{Γ}{Γ∙ : Con∙ Γ}{P}(P∙ : Ty∙ (Γ∙ ▹∙ 𝔹∙ [ ε∙ ]T∙) P){P𝕥}(P𝕥∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕥∙ [ ε∙ ]t∙) ]T∙) P𝕥)
                {P𝕗}(P𝕗∙ : Tm∙ Γ∙ (P∙ [ sg∙ (𝕗∙ [ ε∙ ]t∙) ]T∙) P𝕗){b}(b∙ : Tm∙ Γ∙ (𝔹∙ [ ε∙ ]T∙) b)
                → Tm∙ Γ∙ (P∙ [ sg∙ b∙ ]T∙) (ifᵗ P P𝕥 P𝕗 b)