Telescopes?

Telescope.agda

module Telescope where

open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec

infixr 6 _∷_

data Telescope (F : Set) : Set₁ where
  []  : Telescope F
  _∷_ : (A : F → Set) (As : Telescope (Σ F A)) → Telescope F

⟦_⟧ : ∀ {F} → Telescope F → Set
⟦_⟧ {F} [] = F
⟦ A ∷ As ⟧ = ⟦ As ⟧

x : Telescope ⊤
x = (λ _ → ℕ) ∷ (λ { (_ , n) → Vec ℕ n }) ∷ (λ { ((_ , n) , xs) → n ∈ xs }) ∷ []

q : ⟦ x ⟧
q = ((tt , 3) , (0 ∷ 3 ∷ 0 ∷ [])) , there here

So, in other words, ⟦ x ⟧ is the type of all vectors which contain their length as an element. Correct?

So, in other words, ⟦ x ⟧ is the type of all vectors which contain their length as an element. Correct?

Yeah :)

Yeah :)