Crisp pullbacks
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-pullbacks where
Imports
open import foundation.action-on-identifications-functions open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-pullbacks open import foundation.homotopies open import foundation.identity-types open import foundation.morphisms-cospan-diagrams open import foundation.pullbacks open import foundation.standard-pullbacks open import foundation.universe-levels open import modal-type-theory.action-on-identifications-crisp-functions open import modal-type-theory.action-on-identifications-flat-modality open import modal-type-theory.crisp-dependent-pair-types open import modal-type-theory.crisp-identity-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
We say a pullback is crisp¶ if it is formed in a crisp context.
Comment. The results in this file should hold more generally for
crisp maps defined on crisp elements
@♭ f : @♭ A → X
and @♭ g : @♭ B → X
.
Properties
Flat distributes over standard pullbacks
module _ {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3} (@♭ f : A → X) (@♭ g : B → X) where map-distributive-flat-standard-pullback : ♭ (standard-pullback f g) → standard-pullback (action-flat-map f) (action-flat-map g) map-distributive-flat-standard-pullback (intro-flat (x , y , p)) = ( intro-flat x , intro-flat y , ap-flat p) map-inv-distributive-flat-standard-pullback : @♭ standard-pullback (action-flat-map f) (action-flat-map g) → ♭ (standard-pullback f g) map-inv-distributive-flat-standard-pullback (intro-flat x , intro-flat y , p) = intro-flat (x , y , ap counit-flat p) is-crisp-section-map-distributive-flat-standard-pullback : (@♭ x : ♭ (standard-pullback f g)) → map-inv-distributive-flat-standard-pullback ( map-distributive-flat-standard-pullback x) = ( x) is-crisp-section-map-distributive-flat-standard-pullback ( intro-flat (x , y , p)) = crisp-ap ( intro-flat) ( eq-pair-eq-fiber ( eq-pair-eq-fiber ( is-crisp-section-ap-flat p))) is-crisp-retraction-map-distributive-flat-standard-pullback : (@♭ x : standard-pullback (action-flat-map f) (action-flat-map g)) → map-distributive-flat-standard-pullback ( map-inv-distributive-flat-standard-pullback x) = ( x) is-crisp-retraction-map-distributive-flat-standard-pullback ( intro-flat x , intro-flat y , p) = eq-pair-eq-fiber ( eq-pair-eq-fiber ( crisp-based-ind-Id ( λ where (intro-flat y) p → crisp-ap intro-flat (ap counit-flat p) = p) ( refl) ( p)))
Computing the flat counit on a standard pullback
The counit of the flat modality computes as the counit on each component of a crisp dependent pair type.
module _ {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3} (@♭ f : A → X) (@♭ g : B → X) where counit-flat-hom-cospan-diagram : hom-cospan-diagram (action-flat-map f) (action-flat-map g) f g counit-flat-hom-cospan-diagram = ( counit-flat , counit-flat , counit-flat , inv-htpy (naturality-counit-flat f) , inv-htpy (naturality-counit-flat g)) compute-counit-flat-standard-pullback : ( map-standard-pullback ( f) ( g) ( action-flat-map f) ( action-flat-map g) ( counit-flat-hom-cospan-diagram)) ∘ ( map-distributive-flat-standard-pullback f g) ~ counit-flat {A = standard-pullback f g} compute-counit-flat-standard-pullback (intro-flat (x , y , p)) = eq-pair-eq-fiber ( eq-pair-eq-fiber ( right-unit ∙ is-crisp-section-ap-flat p))
A crisp standard pullback is flat discrete if its factors are
module _ {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3} (@♭ f : A → X) (@♭ g : B → X) where is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors : is-flat-discrete-crisp X → is-flat-discrete-crisp A → is-flat-discrete-crisp B → is-flat-discrete-crisp (standard-pullback f g) is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors bX bA bB = is-flat-discrete-crisp-Σ ( bA) ( λ a → is-flat-discrete-crisp-Σ ( bB) ( λ b → is-flat-discrete-crisp-Id (is-emb-is-equiv bX)))
A crisp pullback is flat discrete if its factors are
module _ {@♭ l1 l2 l3 : Level} {@♭ A : UU l1} {@♭ B : UU l2} {@♭ X : UU l3} (@♭ f : A → X) (@♭ g : B → X) where is-flat-discrete-crisp-pullback-is-flat-discrete-crisp-factors : {@♭ l4 : Level} {@♭ C : UU l4} (@♭ c : cone f g C) → @♭ is-pullback f g c → is-flat-discrete-crisp X → is-flat-discrete-crisp A → is-flat-discrete-crisp B → is-flat-discrete-crisp C is-flat-discrete-crisp-pullback-is-flat-discrete-crisp-factors c H bX bA bB = is-flat-discrete-crisp-equiv' ( gap f g c , H) ( is-flat-discrete-crisp-standard-pullback-is-flat-discrete-crisp-factors ( f) ( g) ( bX) ( bA) ( bB))
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
- 2024-09-06. Fredrik Bakke. Basic properties of the flat modality (#1078).