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

open import Agda.Primitive
open import Lib

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

-- Terminal family
Fam-⊤ : ∀ {i j} → Fam {i} {j}
Fam-⊤ .Fam.Ty   = ⊤
Fam-⊤ .Fam.Tm _ = ⊤

-- Presheaf family
Fam-Psh : ∀ {i} → Fam {lsuc i} {i}
Fam-Psh {i} .Fam.Ty   = Set i
Fam-Psh {i} .Fam.Tm A = A

-- Join of two families
_∗_ : ∀ {i₁ i₂ j₁ j₂} → Fam {i₁} {j₁} → Fam {i₂} {j₂} → Fam {i₁ ⊔ i₂ ⊔ j₁} {j₁ ⊔ j₂}
(C ∗ D) .Fam.Ty = Σ (C .Fam.Ty) λ A → C .Fam.Tm A → D .Fam.Ty
(C ∗ D) .Fam.Tm (A , B) = Σ (C .Fam.Tm A) λ a → D .Fam.Tm (B a)

-- Family of dependent types and terms
Ext : ∀ {ic id jd} (A : Set ic) (D : Fam {id} {jd}) → Fam
Ext A D .Fam.Ty   = A → D .Fam.Ty
Ext A D .Fam.Tm B = ∀ a → D .Fam.Tm (B a)

-- Left-nested length-indexed telescopes of a family
LIxTele : ∀ {i j} → ℕ → Fam {i} {j} → Fam {i ⊔ j} {j}
LIxTele zero C = Fam-⊤
LIxTele (suc n) C = LIxTele n C ∗ C

-- Left-nested telescopes
LTele : ∀ {i j} → Fam {i} {j} → Fam {i ⊔ j} {j}
LTele C .Fam.Ty = Σ ℕ λ n → LIxTele n C .Fam.Ty
LTele C .Fam.Tm (n , A) = LIxTele n C .Fam.Tm A

-- Non-empty left-nested length-indexed telescopes of a family
LIxTele₁ : ∀ {i j} → ℕ → Fam {i} {j} → Fam {i ⊔ j} {j}
LIxTele₁ {j = j} zero C .Fam.Ty = Lift {j = j} (C .Fam.Ty)
LIxTele₁ zero C .Fam.Tm A = C .Fam.Tm (A .lower)
LIxTele₁ (suc n) C = LIxTele₁ n C ∗ C

-- Right-nested length-indexed telescopes of a family
RIxTele : ∀ {i j} → ℕ → Fam {i} {j} → Fam {i ⊔ j} {j}
RIxTele zero C = Fam-⊤
RIxTele (suc n) C = C ∗ RIxTele n C

-- Right-nested telescopes
RTele : ∀ {i j} → Fam {i} {j} → Fam {i ⊔ j} {j}
RTele C .Fam.Ty = Σ ℕ λ n → RIxTele n C .Fam.Ty
RTele C .Fam.Tm (n , A) = RIxTele n C .Fam.Tm A