------------------------------------------------------------------------ -- The Agda standard library -- -- Products ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Product where open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) private variable a b c ℓ p q r s : Level A B C : Set a ------------------------------------------------------------------------ -- Definition of dependent products open import Data.Product.Base public -- These are here as they are not 'basic' but instead "very dependent", -- i.e. the result type depends on the full input 'point' (x , y). map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → ((x , y) : Σ A P) → Σ (B x) (Q y) map-Σ f g (x , y) = (f x , g y) -- This is a "non-dependent" version of map-Σ whereby the input is actually -- a pair (i.e. _×_ ) but the output type still depends on the input 'point' (x , y). map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y map-Σ′ f g (x , y) = (f x , g y) -- This is a generic zipWith for Σ where different functions are applied to each -- component pair, and recombined. zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → ((a , p) : Σ A P) → ((b , q) : Σ B Q) → S (a ∙ b) (p ∘ q) zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q) ------------------------------------------------------------------------ -- 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