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 β€ #-}