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

infixr 4 _,_

Ξ£-syntax : βˆ€ {β„“ β„“'} (A : Type β„“) (F : A β†’ Type β„“') β†’ Type _
Ξ£-syntax X F = Ξ£ X F

syntax Ξ£-syntax X (Ξ» x β†’ F) = Ξ£[ x ∈ X ] F
infix 4 Ξ£-syntax

instance
  Ξ£-of-instances : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'} ⦃ x : A ⦄ ⦃ y : B x ⦄ β†’ Ξ£ A B
  Ξ£-of-instances ⦃ x ⦄ ⦃ y ⦄ = x , y

Similarly, for the unit type:

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