1
module Common.Product where
3
open import Common.Level
8
------------------------------------------------------------------------
10
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
18
syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
20
∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
23
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
26
_,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B