# Flat dependent function types

Content created by Fredrik Bakke.

Created on 2023-11-24.

{-# OPTIONS --cohesion --flat-split #-}

module modal-type-theory.flat-dependent-function-types where

Imports
open import foundation.universe-levels

open import modal-type-theory.flat-modality


## 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