sigma.agda

open import Data.Nat
open import Data.Char

data Σ : (a : Set) → (P : a → Set) → Set where
  Sigma : {a : Set} → {P : a → Set} → (x : a) → P x → Σ a P

data Vect : ℕ → Set → Set where
  Nil : {a : Set} → Vect zero a
  _∷_ : {a : Set} → {n : ℕ} → a → Vect n a → Vect (suc n) a
infixr 5 _∷_

v : Vect 5 Char
v = 'h' ∷ 'e' ∷ 'l' ∷ 'l' ∷ 'o' ∷ Nil

vec : Σ ℕ (λ n → Vect n Char)
vec = Sigma 2 ('3' ∷ '4' ∷ Nil)

vec' : Σ ℕ (λ n → Vect n Char)
vec' = Sigma _ ('3' ∷ '4' ∷ Nil)