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 Ξ£ #-}

infixr 4 _,_

Similarly, for the unit type:

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