依存和型

module foundations.sigma-type where

open import foundations.universe

依存和型を定義する。

private variable ℓ ℓ′ : Level

record Σ (A : Type ℓ) (B : A → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
  constructor _,_

  field
    fst : A
    snd : B fst

open Σ using (fst; snd) public

以下のようなsyntax宣言を使うことで、依存和型をΣ[ x ∈ A ] Bと書けるようになる。

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

_ : ∀ (A : Type ℓ) (B : A → Type ℓ′) (x : A) (y : B x) → Σ[ a ∈ A ] B a
_ = λ A B x y → x , y