open import Prim.Extension
open import Prim.Interval
open import Prim.Type
open import Prim.Kan

module Prim.Data.Sigma where

Primitives: Sigma typesπŸ”—

The dependent sum type, total space, or type of dependent pairs, is defined as a record, so that it enjoys definitional Ξ·.

record Ξ£ {β„“ β„“β€²} (A : Type β„“) (B : A β†’ Type β„“β€²) : Type (β„“ βŠ” β„“β€²) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Ξ£ public

{-# BUILTIN SIGMA Ξ£ #-}

syntax Ξ£ A (Ξ» x β†’ B) = Ξ£[ x ∈ A ] B

infixr 4 _,_
infix 5 Ξ£

Similarly, for the unit type:

record ⊀ : Type where
  instance constructor tt
{-# BUILTIN UNIT ⊀ #-}