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
open import foundation.universe-levels

open import modal-type-theory.flat-modality


We study interactions between the flat modality and dependent function types.


Flat distributes over dependent function types

module _
  {@l1 l2 : Level} {@A : UU l1} {@B : A  UU l2}

  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}

  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


Dan Licata. Dlicata335/cohesion-agda. GitHub repository. URL: https://github.com/dlicata335/cohesion-agda.
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