Set presented types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-02-17.
Last modified on 2024-08-22.

module foundation.set-presented-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-coproduct-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.fibers-of-maps
open import foundation.functoriality-coproduct-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.images
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.set-truncations
open import foundation.subtypes
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions
open import foundation-core.sets

Idea

A type A is said to be set presented if there exists a map f : X → A from a set X such that the composite X → A → type-trunc-Set A is an equivalence.

Definitions

Set presentations of types

module _
  {l1 l2 : Level} (A : Set l1) (B : UU l2)
  where

  has-set-presentation-Prop : Prop (l1 ⊔ l2)
  has-set-presentation-Prop =
    ∃ (type-Set A → B) (λ f → is-equiv-Prop (unit-trunc-Set ∘ f))

  has-set-presentation : UU (l1 ⊔ l2)
  has-set-presentation = type-Prop has-set-presentation-Prop

  is-prop-has-set-presentation : is-prop has-set-presentation
  is-prop-has-set-presentation = is-prop-type-Prop has-set-presentation-Prop

Propositions

Types set presented by coproducts are coproducts

Given a type B that is set presented by a coproduct

              B
            ∧   \
         f /     \ η
          /   ~   ∨
  (A1 + A2) -----> ║B║₀,

then B computes as the coproduct of the images of the restrictions of f along the left and right inclusion of the coproduct A1 + A2

  B ≃ im (f ∘ inl) + im (f ∘ inr).

module _
  {l1 l2 l3 : Level} {A1 : UU l1} {A2 : UU l2} {B : UU l3}
  (f : A1 + A2 → B) (e : (A1 + A2) ≃ ║ B ║₀)
  (H : unit-trunc-Set ∘ f ~ map-equiv e)
  where

  map-is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) → B
  map-is-coproduct-codomain = rec-coproduct pr1 pr1

  triangle-is-coproduct-codomain :
    ( ( map-is-coproduct-codomain) ∘
      ( map-coproduct (map-unit-im (f ∘ inl)) (map-unit-im (f ∘ inr)))) ~ f
  triangle-is-coproduct-codomain (inl x) = refl
  triangle-is-coproduct-codomain (inr x) = refl

  abstract
    is-emb-map-is-coproduct-codomain : is-emb map-is-coproduct-codomain
    is-emb-map-is-coproduct-codomain =
      is-emb-coproduct
        ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
        ( is-emb-inclusion-subtype (λ b → trunc-Prop _))
        ( λ (b1 , u) (b2 , v) →
          apply-universal-property-trunc-Prop u
            ( function-Prop _ empty-Prop)
            ( λ where
              ( x , refl) →
                apply-universal-property-trunc-Prop v
                  ( function-Prop _ empty-Prop)
                  ( λ where
                    ( y , refl) r →
                      is-empty-eq-coproduct-inl-inr x y
                        ( is-injective-is-equiv
                          ( is-equiv-map-equiv e)
                          ( ( inv (H (inl x))) ∙
                            ( ap unit-trunc-Set r) ∙
                            ( H (inr y)))))))

  abstract
    is-surjective-map-is-coproduct-codomain :
      is-surjective map-is-coproduct-codomain
    is-surjective-map-is-coproduct-codomain b =
      apply-universal-property-trunc-Prop
        ( apply-effectiveness-unit-trunc-Set
          ( inv (is-section-map-inv-equiv e (unit-trunc-Set b)) ∙ inv (H a)))
        ( trunc-Prop (fiber map-is-coproduct-codomain b))
        ( λ p →
          unit-trunc-Prop
            ( ( map-coproduct
                ( map-unit-im (f ∘ inl))
                ( map-unit-im (f ∘ inr))
                ( a)) ,
              ( triangle-is-coproduct-codomain a ∙ inv p)))
      where
      a : A1 + A2
      a = map-inv-equiv e (unit-trunc-Set b)

  is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) ≃ B
  pr1 is-coproduct-codomain = map-is-coproduct-codomain
  pr2 is-coproduct-codomain =
    is-equiv-is-emb-is-surjective
      is-surjective-map-is-coproduct-codomain
      is-emb-map-is-coproduct-codomain

Recent changes