Flat dependent pair types
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2024-03-12.
{-# OPTIONS --cohesion --flat-split #-} module modal-type-theory.flat-dependent-pair-types where
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.retractions open import foundation.sections open import foundation.universe-levels open import modal-type-theory.flat-modality
Idea
We study interactions between the flat modality and dependent pair types.
Definitions
Σ-♭ : {@♭ l1 l2 : Level} (@♭ A : UU l1) (@♭ B : A → UU l2) → UU (l1 ⊔ l2) Σ-♭ A B = Σ (♭ A) (λ where (cons-flat x) → ♭ (B x))
Properties
Flat distributes over Σ-types
module _ {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} where map-distributive-flat-Σ : ♭ (Σ A B) → Σ-♭ A B pr1 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat x pr2 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat y map-inv-distributive-flat-Σ : Σ-♭ A B → ♭ (Σ A B) map-inv-distributive-flat-Σ (cons-flat x , cons-flat y) = cons-flat (x , y) is-section-distributive-flat-Σ : (map-inv-distributive-flat-Σ ∘ map-distributive-flat-Σ) ~ id is-section-distributive-flat-Σ (cons-flat _) = refl is-retraction-distributive-flat-Σ : (map-distributive-flat-Σ ∘ map-inv-distributive-flat-Σ) ~ id is-retraction-distributive-flat-Σ (cons-flat _ , cons-flat _) = refl section-distributive-flat-Σ : section map-distributive-flat-Σ pr1 section-distributive-flat-Σ = map-inv-distributive-flat-Σ pr2 section-distributive-flat-Σ = is-retraction-distributive-flat-Σ retraction-distributive-flat-Σ : retraction map-distributive-flat-Σ pr1 retraction-distributive-flat-Σ = map-inv-distributive-flat-Σ pr2 retraction-distributive-flat-Σ = is-section-distributive-flat-Σ is-equiv-distributive-flat-Σ : is-equiv map-distributive-flat-Σ pr1 is-equiv-distributive-flat-Σ = section-distributive-flat-Σ pr2 is-equiv-distributive-flat-Σ = retraction-distributive-flat-Σ equiv-distributive-flat-Σ : ♭ (Σ A B) ≃ Σ-♭ A B pr1 equiv-distributive-flat-Σ = map-distributive-flat-Σ pr2 equiv-distributive-flat-Σ = is-equiv-distributive-flat-Σ inv-equiv-distributive-flat-Σ : Σ-♭ A B ≃ ♭ (Σ A B) inv-equiv-distributive-flat-Σ = inv-equiv equiv-distributive-flat-Σ
See also
- Flat discrete types for types that are flat modal.
References
- [Lic]
- Dan Licata. Dlicata335/cohesion-agda. GitHub repository. URL: https://github.com/dlicata335/cohesion-agda.
- [Shu18]
- Michael Shulman. Brouwer's fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856–941, 06 2018. arXiv:1509.07584, doi:10.1017/S0960129517000147.
Recent changes
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).