依存和型

module sigma-type where

open import identity-type

定義

infixr  _,_
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

積型は依存和型の特別な場合である:

infixl  _×_
_×_ : Set → Set → Set
A × B = Σ[ _ ∈ A ] B

private variable
  A B : Set

×Id : ∀ {p q : A × B}
  → fst p ＝ fst q
  → snd p ＝ snd q
  → p ＝ q
×Id refl refl = refl