Home
module foundations.implicit-function where
Imports
open import foundations.universe
open import foundations.bi-invertible-map
open import foundations.quasi-inverse
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.sigma-type
open import foundations.identity-type
private variable
ℓ : Level
A : Type ℓ
B : A → Type ℓ
toImplicitΠ : ((a : A) → B a) → (∀ {a : A} → B a)
toImplicitΠ f = f _
biinvToImplicitΠ : biinv (toImplicitΠ {A = A} {B = B})
biinvToImplicitΠ = QuasiInv⇒biinv (record
{ g = λ x a → x {a = a}
; linv = λ _ → refl
; rinv = λ _ → refl
})
explicitΠ≃implicitΠ : ((a : A) → B a) ≃ (∀ {a : A} → B a)
explicitΠ≃implicitΠ = toImplicitΠ , biinvToImplicitΠ
toExplicitΠ : ({a : A} → B a) → (∀ (a : A) → B a)
toExplicitΠ = biinvToImplicitΠ .fst .fst