Flat dependent function 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-function-types where
Idea
We study interactions between the flat modality and dependent function types.
Properties
Flat distributes over dependent function types
module _ {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} where map-crisp-distributive-flat-Π : ♭ ((x : A) → B x) → ((@♭ x : A) → ♭ (B x)) map-crisp-distributive-flat-Π (cons-flat f) x = cons-flat (f x) module _ {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} where map-crisp-distributive-flat-function-types : ♭ (A → B) → (@♭ A → ♭ B) map-crisp-distributive-flat-function-types = map-crisp-distributive-flat-Π map-distributive-flat-function-types : ♭ (A → B) → (♭ A → ♭ B) map-distributive-flat-function-types f (cons-flat x) = map-crisp-distributive-flat-function-types f x
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).
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).