------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic properties of the function type
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Properties where
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Function.Base using (flip; _∘_)
open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core
using (trans; cong; cong′)
private
variable
a b c d p : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Implicit and explicit function spaces are isomorphic
Π↔Π : {B : A → Set b} → ((x : A) → B x) ↔ ({x : A} → B x)
Π↔Π = mk↔ₛ′ (λ f {x} → f x) (λ f _ → f) cong′ cong′
------------------------------------------------------------------------
-- Function spaces can be reordered
ΠΠ↔ΠΠ : (R : A → B → Set p) →
((x : A) (y : B) → R x y) ↔ ((y : B) (x : A) → R x y)
ΠΠ↔ΠΠ _ = mk↔ₛ′ flip flip cong′ cong′
------------------------------------------------------------------------
-- Assuming extensionality then → preserves ↔
→-cong-↔ : {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
Extensionality a c → Extensionality b d →
A ↔ B → C ↔ D → (A → C) ↔ (B → D)
→-cong-↔ extAC extBD A↔B C↔D = mk↔ₛ′
(λ h → C↔D.to ∘ h ∘ A↔B.from)
(λ g → C↔D.from ∘ g ∘ A↔B.to )
(λ h → extBD λ x → trans (C↔D.strictlyInverseˡ _) (cong h (A↔B.strictlyInverseˡ x)))
(λ g → extAC λ x → trans (C↔D.strictlyInverseʳ _) (cong g (A↔B.strictlyInverseʳ x)))
where module A↔B = Inverse A↔B; module C↔D = Inverse C↔D
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