------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Nary.NonDependent where
------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------
open import Level using (Level; 0ℓ; _⊔_; Lift)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Product.Base using (_×_; _,_)
open import Data.Product.Nary.NonDependent
using (Product; uncurryₙ; Equalₙ; curryₙ; fromEqualₙ; toEqualₙ)
open import Function.Base using (_∘′_; _$′_; const; flip)
open import Relation.Unary using (IUniversal)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst; cong)
private
variable
a b r : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Re-exporting the basic operations
open import Function.Nary.NonDependent.Base public
------------------------------------------------------------------------
-- Congruence
module _ n {ls} {as : Sets n ls} {R : Set r} (f : as ⇉ R) where
private
g : Product n as → R
g = uncurryₙ n f
-- Congruentₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
-- a₁₁ ≡ a₁₂ → ⋯ → aₙ₁ ≡ aₙ₂ →
-- f a₁₁ ⋯ aₙ₁ ≡ f a₁₂ ⋯ aₙ₂
Congruentₙ : Set (r Level.⊔ ⨆ n ls)
Congruentₙ = ∀ {l r} → Equalₙ n l r ⇉ (g l ≡ g r)
congₙ : Congruentₙ
congₙ = curryₙ n (cong g ∘′ fromEqualₙ n)
-- Congruence at a specific location
module _ m n {ls ls′} {as : Sets m ls} {bs : Sets n ls′}
(f : as ⇉ (A → bs ⇉ B)) where
private
g : Product m as → A → Product n bs → B
g vs a ws = uncurryₙ n (uncurryₙ m f vs a) ws
congAt : ∀ {vs ws a₁ a₂} → a₁ ≡ a₂ → g vs a₁ ws ≡ g vs a₂ ws
congAt {vs} {ws} = cong (λ a → g vs a ws)
------------------------------------------------------------------------
-- Injectivity
module _ n {ls} {as : Sets n ls} {R : Set r} (con : as ⇉ R) where
-- Injectiveₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
-- con a₁₁ ⋯ aₙ₁ ≡ con a₁₂ ⋯ aₙ₂ →
-- a₁₁ ≡ a₁₂ × ⋯ × aₙ₁ ≡ aₙ₂
private
c : Product n as → R
c = uncurryₙ n con
Injectiveₙ : Set (r Level.⊔ ⨆ n ls)
Injectiveₙ = ∀ {l r} → c l ≡ c r → Product n (Equalₙ n l r)
injectiveₙ : (∀ {l r} → c l ≡ c r → l ≡ r) → Injectiveₙ
injectiveₙ con-inj eq = toEqualₙ n (con-inj eq)
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