The Regensburg extension of the fundamental theorem of identity types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-28.
Last modified on 2024-10-29.

module
  foundation.regensburg-extension-fundamental-theorem-of-identity-types
  where
Imports 
open import foundation.0-connected-types
open import foundation.connected-maps
open import foundation.connected-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fiber-inclusions
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.functoriality-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.maps-in-subuniverses
open import foundation.propositional-truncations
open import foundation.separated-types
open import foundation.subuniverses
open import foundation.surjective-maps
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels

Idea

The Regensburg extension of the fundamental theorem of identity types asserts that for any subuniverse P, and any pointed connected type A equipped with a type family B over A, the following are logically equivalent:

  1. Every family of maps f : (x : A) → (* ＝ x) → B x is a family of P-maps, i.e., a family of maps with fibers in P.
  2. The total space Σ A B is P-separated, i.e., its identity types are in P.

In other words, the extended fundamental theorem of identity types asserts that for any higher group BG equipped with a higher group action X, every homomorphism of higher group actions f : (u : BG) → (* ＝ u) → X u consists of a family of P maps if and only if the type of orbits of X is P-separated.

Proof: Suppose that every family of maps f : (x : A) → (* ＝ x) → B x is a family of P-maps. The fiber of such f x : (* ＝ x) → B x at y is equivalent to the type (* , f * refl) ＝ (x , y). Our assumption is therefore equivalent to the assumption that the type (* , f * refl) ＝ (x , y) is in P for every f, x, and y. By the universal property of identity types, this condition is equivalent to the condition that (* , y') ＝ (x , y) is in P for every y', x, and y. Finally, since A is assumed to be connected, this condition is equivalent to the condition that Σ A B is P-separated.

This theorem was stated and proven for the first time during the Interactions of Proof Assistants and Mathematics summer school in Regensburg, 2023, as part of Egbert Rijke’s tutorial on formalization in agda-unimath.

Theorem

module _
  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3)
  {A : UU l1} (a : A) {B : A → UU l2}
  where

  abstract
    forward-implication-extended-fundamental-theorem-id :
      is-0-connected A →
      ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) →
      is-separated P (Σ A B)
    forward-implication-extended-fundamental-theorem-id H K (x , y) (x' , y') =
      apply-universal-property-trunc-Prop
        ( mere-eq-is-0-connected H a x)
        ( P _)
        ( λ where
          refl →
            is-in-subuniverse-equiv P
              ( compute-fiber-map-out-of-identity-type
                ( ind-Id a (λ u v → B u) y)
                ( x')
                ( y'))
              ( K (ind-Id a (λ u v → B u) y) x' y'))

  abstract
    backward-implication-extended-fundamental-theorem-id :
      is-separated P (Σ A B) →
      (f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)
    backward-implication-extended-fundamental-theorem-id K f x y =
      is-in-subuniverse-equiv' P
        ( compute-fiber-map-out-of-identity-type f x y)
        ( K (a , f a refl) (x , y))

  abstract
    extended-fundamental-theorem-id :
      is-0-connected A →
      ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-in-subuniverse-map P (f x)) ↔
      is-separated P (Σ A B)
    pr1 (extended-fundamental-theorem-id H) =
      forward-implication-extended-fundamental-theorem-id H
    pr2 (extended-fundamental-theorem-id H) =
      backward-implication-extended-fundamental-theorem-id

Corollaries

Characterizing families of surjective maps out of identity types

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

  forward-implication-extended-fundamental-theorem-id-surjective :
    is-0-connected A →
    ( (f : (x : A) → (a ＝ x) → B x) → (x : A) → is-surjective (f x)) →
    is-inhabited (B a) → is-0-connected (Σ A B)
  forward-implication-extended-fundamental-theorem-id-surjective H K L =
    is-0-connected-mere-eq-is-inhabited
      ( map-trunc-Prop (fiber-inclusion B a) L)
      ( forward-implication-extended-fundamental-theorem-id
        ( is-inhabited-Prop)
        ( a)
        ( H)
        ( K))

  backward-implication-extended-fundamental-theorem-id-surjective :
    is-0-connected (Σ A B) →
    (f : (x : A) → (a ＝ x) → B x) (x : A) → is-surjective (f x)
  backward-implication-extended-fundamental-theorem-id-surjective L =
    backward-implication-extended-fundamental-theorem-id
      ( is-inhabited-Prop)
      ( a)
      ( mere-eq-is-0-connected L)

  extended-fundamental-theorem-id-surjective :
    is-0-connected A → is-inhabited (B a) →
    ( (f : (x : A) → (a ＝ x) → B x) → (x : A) → is-surjective (f x)) ↔
    is-0-connected (Σ A B)
  pr1 (extended-fundamental-theorem-id-surjective H K) L =
    forward-implication-extended-fundamental-theorem-id-surjective H L K
  pr2 ( extended-fundamental-theorem-id-surjective H K) =
    backward-implication-extended-fundamental-theorem-id-surjective

Characterizing families of connected maps out of identity types

module _
  {l1 l2 : Level} (k : 𝕋)
  {A : UU l1} (a : A) {B : A → UU l2}
  where

  forward-implication-extended-fundamental-theorem-id-connected :
    is-0-connected A →
    ( (f : (x : A) → (a ＝ x) → B x) → (x : A) → is-connected-map k (f x)) →
    is-inhabited (B a) → is-connected (succ-𝕋 k) (Σ A B)
  forward-implication-extended-fundamental-theorem-id-connected H K L =
    is-connected-succ-is-connected-eq
      ( map-trunc-Prop (fiber-inclusion B a) L)
      ( forward-implication-extended-fundamental-theorem-id
        ( is-connected-Prop k)
        ( a)
        ( H)
        ( K))

  backward-implication-extended-fundamental-theorem-id-connected :
    is-connected (succ-𝕋 k) (Σ A B) →
    (f : (x : A) → (a ＝ x) → B x) (x : A) → is-connected-map k (f x)
  backward-implication-extended-fundamental-theorem-id-connected K =
    backward-implication-extended-fundamental-theorem-id
      ( is-connected-Prop k)
      ( a)
      ( λ x y → is-connected-eq-is-connected K)

  extended-fundamental-theorem-id-connected :
    is-0-connected A → is-inhabited (B a) →
    ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-connected-map k (f x)) ↔
    is-connected (succ-𝕋 k) (Σ A B)
  pr1 (extended-fundamental-theorem-id-connected H K) L =
    forward-implication-extended-fundamental-theorem-id-connected H L K
  pr2 (extended-fundamental-theorem-id-connected H K) =
    backward-implication-extended-fundamental-theorem-id-connected

Characterizing families of truncated maps out of identity types

module _
  {l1 l2 : Level} (k : 𝕋) {A : UU l1} (a : A) {B : A → UU l2}
  where

  forward-implication-extended-fundamental-theorem-id-truncated :
    is-0-connected A →
    ((f : (x : A) → (a ＝ x) → B x) → (x : A) → is-trunc-map k (f x)) →
    is-trunc (succ-𝕋 k) (Σ A B)
  forward-implication-extended-fundamental-theorem-id-truncated =
    forward-implication-extended-fundamental-theorem-id
      ( is-trunc-Prop k)
      ( a)

  backward-implication-extended-fundamental-theorem-id-truncated :
    is-trunc (succ-𝕋 k) (Σ A B) →
    (f : (x : A) → (a ＝ x) → B x) (x : A) → is-trunc-map k (f x)
  backward-implication-extended-fundamental-theorem-id-truncated =
    backward-implication-extended-fundamental-theorem-id
      ( is-trunc-Prop k)
      ( a)

  extended-fundamental-theorem-id-truncated :
    is-0-connected A →
    ((f : (x : A) → (a ＝ x) → B x) (x : A) → is-trunc-map k (f x)) ↔
    is-trunc (succ-𝕋 k) (Σ A B)
  pr1 (extended-fundamental-theorem-id-truncated H) =
    forward-implication-extended-fundamental-theorem-id-truncated H
  pr2 (extended-fundamental-theorem-id-truncated H) =
    backward-implication-extended-fundamental-theorem-id-truncated

See also

The Regensburg extension of the fundamental theorem is used in the following files:

References

Two special cases of the extended fundamental theorem of identity types are stated in [Rij22]: The case where P is the subuniverse of k-truncated types is stated as Theorem 19.6.2; and the case where P is the subuniverse of inhabited types is stated as Exercise 19.14.

[Rij22]
Egbert Rijke. Introduction to Homotopy Type Theory. 12 2022. arXiv:2212.11082.

Recent changes