The universal property of flat discrete crisp types

Content created by Fredrik Bakke.

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

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

module modal-type-theory.universal-property-flat-discrete-crisp-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.universal-property-equivalences
open import foundation.universe-levels

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

Idea

The universal property of a flat discrete crisp type A states that under the flat modality ♭, A is colocal at the counit of ♭.

By this we mean that for every crisp type B the map

  coev-flat : ♭ (A → ♭ B) → ♭ (A → B)

is an equivalence.

Definitions

The universal property of flat discrete crisp types

coev-flat :
  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2} → ♭ (A → ♭ B) → ♭ (A → B)
coev-flat {A = A} (intro-flat f) = intro-flat (postcomp A counit-flat f)

universal-property-flat-discrete-crisp-type :
  {@♭ l1 : Level} (@♭ A : UU l1) → UUω
universal-property-flat-discrete-crisp-type A =
  {@♭ l : Level} {@♭ B : UU l} → is-equiv (coev-flat {A = A} {B = B})

Properties

Flat discrete crisp types satisfy the universal property of flat discrete crisp types

This is Corollary 6.15 of [Shu18].

module _
  {@♭ l : Level} {@♭ A : UU l}
  where

  abstract
    universal-property-is-flat-discrete-crisp :
      @♭ is-flat-discrete-crisp A →
      universal-property-flat-discrete-crisp-type A
    universal-property-is-flat-discrete-crisp
      is-disc-A {B = B} =
      is-equiv-htpy-equiv
        ( ( action-flat-equiv
            ( equiv-precomp (inv-equiv (counit-flat , is-disc-A)) B)) ∘e
          ( equiv-action-flat-map-postcomp-counit-flat) ∘e
          ( action-flat-equiv (equiv-precomp (counit-flat , is-disc-A) (♭ B))))
        ( λ where
          (intro-flat f) →
            crisp-ap
              ( intro-flat)
              ( eq-htpy
                ( λ x →
                  ap
                    ( counit-flat ∘ f)
                    ( inv (is-section-map-inv-is-equiv is-disc-A x)))))

See also

References

[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