Dependent universal property of flat discrete crisp 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.dependent-universal-property-flat-discrete-crisp-types where
Imports 
open import foundation.equivalences
open import foundation.universe-levels

open import modal-type-theory.flat-modality

Idea

The dependent universal property of a flat discrete crisp type A states that for any crisp type family defined on crisp elements @♭ B : @♭ A → 𝒰, postcomposition by the counit of the flat modality induces an equivalence under the flat modality.

Definitions

The dependent universal property of flat discrete crisp types

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

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

Properties

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

This remains to be formalized.

See also

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