------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4