Skip to content

Instantly share code, notes, and snippets.

@copumpkin copumpkin/Telescope.agda
Last active Aug 4, 2018

Embed
What would you like to do?
Telescopes?
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) , (030 ∷ [])) , there here
@timjb

This comment has been minimized.

Copy link

timjb commented Jul 14, 2013

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

@copumpkin

This comment has been minimized.

Copy link
Owner Author

copumpkin commented Aug 10, 2013

Yeah :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.