/
Product.agda
43 lines (29 loc) · 1.09 KB
/
Product.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
------------------------------------------------------------------------
-- The Agda standard library
--
-- Products
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Product where
open import Function.Base
open import Level
open import Relation.Nullary.Negation.Core
private
variable
a b c ℓ : Level
A B : Set a
------------------------------------------------------------------------
-- Definition of dependent products
open import Data.Product.Base public
------------------------------------------------------------------------
-- Negation of existential quantifier
∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄ P = ¬ ∃ P
-- Unique existence (parametrised by an underlying equality).
∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
-- Syntax
infix 2 ∄-syntax
∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
∄-syntax = ∄
syntax ∄-syntax (λ x → B) = ∄[ x ] B