Crisp function types

Content created by Fredrik Bakke.

Created on 2024-09-06.
Last modified on 2024-09-06.

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

module modal-type-theory.crisp-function-types where

Imports

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import modal-type-theory.action-on-identifications-flat-modality
open import modal-type-theory.crisp-dependent-function-types
open import modal-type-theory.flat-modality
open import modal-type-theory.functoriality-flat-modality

Idea

We say a function type is crisp^¶ if it is formed in a crisp context.

A function f from A to B may be assumed to be a crisp function^¶ given that its domain and codomain are crisp. By this we mean it is a crisp element of its type, written @♭ f : A → B. We may also assume that a function is defined on crisp elements^¶ if its definition assumes that the elements of its domain are crisp, written f : @♭ A → B. Being crisp, and being defined on crisp elements are independent properties. A function may be crisp and defined on cohesive elements, and it may be cohesive but defined on crisp elements. Indeed, all configurations are possible when both A and B are crisp:

	Crisp function	Cohesive function
Defined on crisp elements	`@♭ (@♭ A → B)`	`@♭ A → B`
Defined on cohesive elements	`@♭ (A → B)`	`A → B`

Note, since assuming that a hypothesis is crisp is less general, assuming that a hypothesis assumes that a hypothesis is crisp is more general. Hence assuming the function is cohesive and defined on crisp elements f : @♭ A → B is the weakest assumption one can make given that A is crisp, while assuming it is crisp and defined on cohesive elements @♭ f : A → B is the strongest, given that B is also crisp.

Properties

Flat distributes in one direction over function types

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

  map-distributive-flat-crisp-function-types : ♭ (@♭ A → B) → (@♭ A → ♭ B)
  map-distributive-flat-crisp-function-types = map-distributive-flat-crisp-Π

  map-distributive-flat-function-types : ♭ (A → B) → (♭ A → ♭ B)
  map-distributive-flat-function-types f (intro-flat x) =
    map-distributive-flat-Π f (intro-flat x)

Postcomposition by the flat counit induces an equivalence `♭ (♭ A → ♭ B) ≃ ♭ (♭ A → B)`

This is Theorem 6.14 in [Shu18].

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

  map-inv-action-flat-map-postcomp-counit-flat : ♭ (♭ A → B) → ♭ (♭ A → ♭ B)
  map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
    intro-flat (λ where (intro-flat y) → intro-flat (f (intro-flat y)))

  is-section-map-inv-action-flat-map-postcomp-counit-flat :
    is-section
      ( action-flat-map (postcomp (♭ A) counit-flat))
      ( map-inv-action-flat-map-postcomp-counit-flat)
  is-section-map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
    ap-flat (eq-htpy (λ where (intro-flat _) → refl))

  is-retraction-map-inv-action-flat-map-postcomp-counit-flat :
    is-retraction
      ( action-flat-map (postcomp (♭ A) counit-flat))
      ( map-inv-action-flat-map-postcomp-counit-flat)
  is-retraction-map-inv-action-flat-map-postcomp-counit-flat (intro-flat f) =
    ap-flat
      ( eq-htpy
        ( λ where
          (intro-flat x) → is-crisp-retraction-intro-flat (f (intro-flat x))))

  is-equiv-action-flat-map-postcomp-counit-flat :
    is-equiv (action-flat-map (postcomp (♭ A) (counit-flat {A = B})))
  is-equiv-action-flat-map-postcomp-counit-flat =
    is-equiv-is-invertible
      ( map-inv-action-flat-map-postcomp-counit-flat)
      ( is-section-map-inv-action-flat-map-postcomp-counit-flat)
      ( is-retraction-map-inv-action-flat-map-postcomp-counit-flat)

  equiv-action-flat-map-postcomp-counit-flat : ♭ (♭ A → ♭ B) ≃ ♭ (♭ A → B)
  pr1 equiv-action-flat-map-postcomp-counit-flat =
    action-flat-map (postcomp (♭ A) counit-flat)
  pr2 equiv-action-flat-map-postcomp-counit-flat =
    is-equiv-action-flat-map-postcomp-counit-flat

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-09-06. Fredrik Bakke. Basic properties of the flat modality (#1078).

agda-unimath