telescope.agda

module tele where

open import Function.Bundles
open import Level hiding (lift; zero; suc)
open import Data.Product
open import Data.Product.Properties using (Σ-≡,≡↔≡)
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin hiding (lift)

open import Relation.Binary.PropositionalEquality

data tele {ℓ} (I : Set ℓ) : Setω
levelₜ : ∀ {ℓ} {I : Set ℓ} → tele I → Level
⟦_⟧ₜ : ∀ {ℓ} {I : Set ℓ} (T : tele I) → I → Set (levelₜ T)

data tele I where
  nil : tele I
  con : ∀ {ℓ} (T : tele I) (A : ∀ i → ⟦ T ⟧ₜ i → Set ℓ) → tele I

levelₜ nil           = 0ℓ
levelₜ (con {ℓ} T A) = levelₜ T ⊔ ℓ

⟦ nil     ⟧ₜ i = ⊤
⟦ con T A ⟧ₜ i = Σ (⟦ T ⟧ₜ i) (A i)

module _ {ℓᵢ} {I : Set ℓᵢ} where

  -- Πₜ constructs an n-ary dependent function over a telescope
  Πₜ : ∀ {ℓ} (T : tele I) → (∀ i → ⟦ T ⟧ₜ i → Set ℓ) → I → Set (levelₜ T ⊔ ℓ)
  Πₜ nil       F i = F i tt
  Πₜ (con T A) F i = Πₜ T (λ i t → (a : A i t) → F i (t , a)) i

  Σₜ : (T : tele I) → I → Set (levelₜ T)
  Σₜ T i = aux T λ _ _ → ⊤
    where aux : ∀ {ℓ} (T : tele I) → (∀ i → ⟦ T ⟧ₜ i → Set ℓ) → Set (levelₜ T ⊔ ℓ)
          aux nil       F = F i tt
          aux (con T A) F = aux T λ i t → Σ (A i t) λ a → F i (t , a)

  uncurryₜ : ∀ {ℓ} {T : tele I} {X : ∀ i → ⟦ T ⟧ₜ i → Set ℓ} {i} → Πₜ T X i → ∀ t → X i t
  uncurryₜ {T = nil}     f tt      = f
  uncurryₜ {T = con T _} f (t , a) = uncurryₜ {T = T} f t a

  curryₜ : ∀ {ℓ} {T : tele I} {X : ∀ i → ⟦ T ⟧ₜ i → Set ℓ} {i} → (∀ t → X i t) → Πₜ T X i
  curryₜ {T = nil}     f = f tt
  curryₜ {T = con T _} f = curryₜ {T = T} λ t a → f (t , a)

  _+ₜ_ : (T : tele I) → tele (Σ I ⟦ T ⟧ₜ) → tele I
  +ₜ-proj₁ : ∀ {T U i} → ⟦ T +ₜ U ⟧ₜ i → ⟦ T ⟧ₜ i
  +ₜ-proj₂ : ∀ {T U i} (x : ⟦ T +ₜ U ⟧ₜ i) → ⟦ U ⟧ₜ (i , +ₜ-proj₁ x)

  T +ₜ nil     = T
  T +ₜ con U A = con (T +ₜ U) λ i x → A _ (+ₜ-proj₂ x)

  +ₜ-proj₁ {U = nil}     x       = x
  +ₜ-proj₁ {U = con U A} (x , a) = +ₜ-proj₁ x

  +ₜ-proj₂ {U = nil}     x       = tt
  +ₜ-proj₂ {U = con U A} (x , a) = +ₜ-proj₂ x , a

  +ₜ-inj : ∀ {T U i} (x : ⟦ T ⟧ₜ i) → ⟦ U ⟧ₜ (i , x) → ⟦ T +ₜ U ⟧ₜ i
  +ₜ-inj-proj₁ : ∀ {T U i} (x : ⟦ T ⟧ₜ i) (y : ⟦ U ⟧ₜ (i , x)) → x ≡ +ₜ-proj₁ (+ₜ-inj x y)
  +ₜ-inj-proj₂ : ∀ {T U i} (x : ⟦ T ⟧ₜ i) (y : ⟦ U ⟧ₜ (i , x)) → subst (λ x → ⟦ U ⟧ₜ (i , x)) (+ₜ-inj-proj₁ x y) y ≡ +ₜ-proj₂ (+ₜ-inj x y)

  +ₜ-inj {U = nil}     x y       = x
  +ₜ-inj {U = con U A} {i = i} x (y , a) .proj₁ = +ₜ-inj x y
  +ₜ-inj {U = con U A} {i = i} x (y , a) .proj₂ =
    subst (λ where (u , v) → A (i , u) v)
          (Σ-≡,≡↔≡ .Inverse.f (+ₜ-inj-proj₁ x y , +ₜ-inj-proj₂ x y))
          a 

  +ₜ-inj-proj₁ {U = nil}     x y = refl
  +ₜ-inj-proj₁ {U = con U A} x (y , a) = +ₜ-inj-proj₁ x y

  +ₜ-inj-proj₂ {U = nil}     x tt       = refl
  +ₜ-inj-proj₂ {U = con U A} x (y , a)  = {!!} -- Σ-≡,≡↔≡ .Inverse.f ({!+ₜ-inj-proj₂ x y!} , {!!})

  

{-

record tele-ext : Setω where
  constructor _,_
  field
    {ext-ℓ} : Level
    pre : tele
    ext : ⟦ pre ⟧ₜ → Set ext-ℓ

  extₜ : tele
  extₜ = con pre ext
open tele-ext public

length : tele → ℕ
length nil       = zero
length (con T A) = suc (length T)

prefix : (T : tele) → Fin (length T) → tele-ext
prefix (con T A) zero    = T , A
prefix (con T A) (suc i) = prefix T i

suffix : (T : tele) (i : Fin (length T)) → ⟦ extₜ (prefix T i) ⟧ₜ → tele
suffix-ext : ∀ {T i} (x : ⟦ extₜ (prefix T i) ⟧ₜ) → ⟦ suffix T i x ⟧ₜ → ⟦ T ⟧ₜ

suffix (con T A) zero    x = nil
suffix (con T A) (suc i) x = con (suffix T i x) λ s → A (suffix-ext x s)

suffix-ext {T = con T A} {i = zero}  p s       = p
suffix-ext {T = con T A} {i = suc i} p (s , a) = suffix-ext p s , a

_+ₜ_ : (T : tele) → (⟦ T ⟧ₜ → tele) → tele
+ₜ-inj₁ : ∀ {T U} → ⟦ T +ₜ U ⟧ₜ → ⟦ T ⟧ₜ

nil     +ₜ U = U tt
con T A +ₜ U = {!!}
  where aux : ∀ {ℓ} (T : tele) (X : ⟦ T ⟧ₜ → Set ℓ) (U : Σ ⟦ T ⟧ₜ X → tele) → tele
        aux nil       X U = {!!}
        aux (con T A) X U = {!<!}

+ₜ-inj₁ = {!!}
-}