------------------------------------------------------------------------
-- 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
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