Functional correspondences
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and malarbol.
Created on 2022-09-13.
Last modified on 2024-02-06.
module foundation.functional-correspondences where
Imports
open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.function-extensionality open import foundation.fundamental-theorem-of-identity-types open import foundation.subtype-identity-principle open import foundation.univalence open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes open import foundation-core.torsorial-type-families
Idea
A functional dependent correspondence is a dependent binary correspondence
C : Π (a : A) → B a → 𝒰
from a type A
to a type family B
over A
such
that for every a : A
the type Σ (b : B a), C a b
is contractible. The type
of dependent functions from A
to B
is equivalent to the type of functional
dependent correspondences.
Definition
is-functional-correspondence-Prop : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) → Prop (l1 ⊔ l2 ⊔ l3) is-functional-correspondence-Prop {A = A} {B} C = Π-Prop A (λ x → is-contr-Prop (Σ (B x) (C x))) is-functional-correspondence : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) → UU (l1 ⊔ l2 ⊔ l3) is-functional-correspondence C = type-Prop (is-functional-correspondence-Prop C) is-prop-is-functional-correspondence : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) → is-prop (is-functional-correspondence C) is-prop-is-functional-correspondence C = is-prop-type-Prop (is-functional-correspondence-Prop C) functional-correspondence : {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) → UU (l1 ⊔ l2 ⊔ lsuc l3) functional-correspondence l3 A B = type-subtype (is-functional-correspondence-Prop {l3 = l3} {A} {B}) module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : functional-correspondence l3 A B) where correspondence-functional-correspondence : (x : A) → B x → UU l3 correspondence-functional-correspondence = pr1 C is-functional-functional-correspondence : is-functional-correspondence correspondence-functional-correspondence is-functional-functional-correspondence = pr2 C
Properties
Characterization of equality in the type of functional dependent correspondences
equiv-functional-correspondence : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} (C : functional-correspondence l3 A B) (D : functional-correspondence l4 A B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) equiv-functional-correspondence {A = A} {B} C D = (x : A) (y : B x) → correspondence-functional-correspondence C x y ≃ correspondence-functional-correspondence D x y module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : functional-correspondence l3 A B) where id-equiv-functional-correspondence : equiv-functional-correspondence C C id-equiv-functional-correspondence x y = id-equiv is-torsorial-equiv-functional-correspondence : is-torsorial (equiv-functional-correspondence C) is-torsorial-equiv-functional-correspondence = is-torsorial-Eq-subtype ( is-torsorial-Eq-Π ( λ x → is-torsorial-equiv-fam ( correspondence-functional-correspondence C x))) ( is-prop-is-functional-correspondence) ( correspondence-functional-correspondence C) ( id-equiv-functional-correspondence) ( is-functional-functional-correspondence C) equiv-eq-functional-correspondence : (D : functional-correspondence l3 A B) → (C = D) → equiv-functional-correspondence C D equiv-eq-functional-correspondence .C refl = id-equiv-functional-correspondence is-equiv-equiv-eq-functional-correspondence : (D : functional-correspondence l3 A B) → is-equiv (equiv-eq-functional-correspondence D) is-equiv-equiv-eq-functional-correspondence = fundamental-theorem-id is-torsorial-equiv-functional-correspondence equiv-eq-functional-correspondence extensionality-functional-correspondence : (D : functional-correspondence l3 A B) → (C = D) ≃ equiv-functional-correspondence C D pr1 (extensionality-functional-correspondence D) = equiv-eq-functional-correspondence D pr2 (extensionality-functional-correspondence D) = is-equiv-equiv-eq-functional-correspondence D eq-equiv-functional-correspondence : (D : functional-correspondence l3 A B) → equiv-functional-correspondence C D → C = D eq-equiv-functional-correspondence D = map-inv-equiv (extensionality-functional-correspondence D)
The type of dependent functions (x : A) → B x
is equivalent to the type of functional dependent correspondences from A
to B
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where functional-correspondence-function : ((x : A) → B x) → functional-correspondence l2 A B pr1 (functional-correspondence-function f) x y = f x = y pr2 (functional-correspondence-function f) x = is-torsorial-Id (f x) function-functional-correspondence : {l3 : Level} → functional-correspondence l3 A B → ((x : A) → B x) function-functional-correspondence C x = pr1 (center (is-functional-functional-correspondence C x)) is-retraction-function-functional-correspondence : (f : (x : A) → B x) → function-functional-correspondence ( functional-correspondence-function f) = f is-retraction-function-functional-correspondence f = eq-htpy ( λ x → ap pr1 ( contraction ( is-functional-functional-correspondence ( functional-correspondence-function f) ( x)) ( f x , refl))) module _ {l3 : Level} (C : functional-correspondence l3 A B) where map-is-section-function-functional-correspondence : (x : A) (y : B x) → function-functional-correspondence C x = y → correspondence-functional-correspondence C x y map-is-section-function-functional-correspondence x ._ refl = pr2 ( center (is-functional-functional-correspondence C x)) is-equiv-map-is-section-function-functional-correspondence : (x : A) (y : B x) → is-equiv (map-is-section-function-functional-correspondence x y) is-equiv-map-is-section-function-functional-correspondence x = fundamental-theorem-id ( is-functional-functional-correspondence C x) ( map-is-section-function-functional-correspondence x) equiv-is-section-function-functional-correspondence : equiv-functional-correspondence ( functional-correspondence-function ( function-functional-correspondence C)) ( C) pr1 ( equiv-is-section-function-functional-correspondence x y) = map-is-section-function-functional-correspondence x y pr2 (equiv-is-section-function-functional-correspondence x y) = is-equiv-map-is-section-function-functional-correspondence x y is-section-function-functional-correspondence : (C : functional-correspondence l2 A B) → functional-correspondence-function (function-functional-correspondence C) = C is-section-function-functional-correspondence C = eq-equiv-functional-correspondence ( functional-correspondence-function ( function-functional-correspondence C)) ( C) ( equiv-is-section-function-functional-correspondence C) is-equiv-functional-correspondence-function : is-equiv functional-correspondence-function is-equiv-functional-correspondence-function = is-equiv-is-invertible function-functional-correspondence is-section-function-functional-correspondence is-retraction-function-functional-correspondence equiv-functional-correspondence-function : ((x : A) → B x) ≃ functional-correspondence l2 A B pr1 equiv-functional-correspondence-function = functional-correspondence-function pr2 equiv-functional-correspondence-function = is-equiv-functional-correspondence-function
Recent changes
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-31. Fredrik Bakke. Rename
is-torsorial-path
tois-torsorial-Id
(#1016). - 2024-01-11. Fredrik Bakke. Make type family implicit for
is-torsorial-Eq-structure
andis-torsorial-Eq-Π
(#995). - 2023-12-21. Fredrik Bakke. Action on homotopies of functions (#973).
- 2023-10-21. Egbert Rijke and Fredrik Bakke. Implement
is-torsorial
throughout the library (#875).