module Fam where

open import Agda.Primitive
open import Lib

record Fam : Set₁ where
  field Ty : Set
        Tm : Ty → Set
open Fam public

-- The terminal family
Fam-⊤ : Fam
Fam-⊤ .Ty   = ⊤
Fam-⊤ .Tm _ = ⊤

-- Join of two families
_∗_ : Fam → Fam → Fam
(C ∗ D) .Ty         = Σ (C .Ty) λ A → C .Tm A → D .Ty
(C ∗ D) .Tm (A , B) = Σ (C .Tm A) λ a → D .Tm (B a)

-- Left-nested length-indexed telescopes of a family
LIxTele : ℕ → Fam → Fam
LIxTele zero    C = Fam-⊤
LIxTele (suc n) C = LIxTele n C ∗ C

-- Left-nested telescopes
LTele : Fam → Fam
LTele C .Ty         = Σ ℕ λ n → LIxTele n C .Ty
LTele C .Tm (n , A) = LIxTele n C .Tm A

-- Non-empty left-nested length-indexed telescopes of a family
LIxTele₁ : ℕ → Fam → Fam
LIxTele₁ zero    C = C
LIxTele₁ (suc n) C = LIxTele₁ n C ∗ C

-- Right-nested length-indexed telescopes of a family
RIxTele : ℕ → Fam → Fam
RIxTele zero    C = Fam-⊤
RIxTele (suc n) C = C ∗ RIxTele n C

-- Right-nested telescopes
RTele : Fam → Fam
RTele C .Ty         = Σ ℕ λ n → RIxTele n C .Ty
RTele C .Tm (n , A) = RIxTele n C .Tm A