Flat dependent pair 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-pair-types where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import modal-type-theory.flat-modality


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


Σ-♭ : {@l1 l2 : Level} (@A : UU l1) (@B : A  UU l2)  UU (l1  l2)
Σ-♭ A B = Σ ( A)  where (cons-flat x)   (B x))


Flat distributes over Σ-types

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

  map-distributive-flat-Σ :  (Σ A B)  Σ-♭ A B
  pr1 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat x
  pr2 (map-distributive-flat-Σ (cons-flat (x , y))) = cons-flat y

  map-inv-distributive-flat-Σ : Σ-♭ A B   (Σ A B)
  map-inv-distributive-flat-Σ (cons-flat x , cons-flat y) = cons-flat (x , y)

  is-section-distributive-flat-Σ :
    (map-inv-distributive-flat-Σ  map-distributive-flat-Σ) ~ id
  is-section-distributive-flat-Σ (cons-flat _) = refl

  is-retraction-distributive-flat-Σ :
    (map-distributive-flat-Σ  map-inv-distributive-flat-Σ) ~ id
  is-retraction-distributive-flat-Σ (cons-flat _ , cons-flat _) = refl

  section-distributive-flat-Σ : section map-distributive-flat-Σ
  pr1 section-distributive-flat-Σ = map-inv-distributive-flat-Σ
  pr2 section-distributive-flat-Σ = is-retraction-distributive-flat-Σ

  retraction-distributive-flat-Σ : retraction map-distributive-flat-Σ
  pr1 retraction-distributive-flat-Σ = map-inv-distributive-flat-Σ
  pr2 retraction-distributive-flat-Σ = is-section-distributive-flat-Σ

  is-equiv-distributive-flat-Σ : is-equiv map-distributive-flat-Σ
  pr1 is-equiv-distributive-flat-Σ = section-distributive-flat-Σ
  pr2 is-equiv-distributive-flat-Σ = retraction-distributive-flat-Σ

  equiv-distributive-flat-Σ :  (Σ A B)  Σ-♭ A B
  pr1 equiv-distributive-flat-Σ = map-distributive-flat-Σ
  pr2 equiv-distributive-flat-Σ = is-equiv-distributive-flat-Σ

  inv-equiv-distributive-flat-Σ : Σ-♭ A B   (Σ A B)
  inv-equiv-distributive-flat-Σ = inv-equiv equiv-distributive-flat-Σ

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