Subsingleton induction

Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.

Created on 2023-10-20.
Last modified on 2024-01-05.

module foundation.subsingleton-induction where
Imports
open import foundation.dependent-pair-types
open import foundation.singleton-induction
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.sections

Idea

Subsingleton induction on a type A is a slight variant of singleton induction which in turn is a principle analogous to induction for the unit type. Subsingleton induction uses the observation that a type equipped with an element is contractible if and only if it is a proposition.

Subsingleton induction states that given a type family B over A, to construct a section of B it suffices to provide an element of B a for some a : A.

Definition

Subsingleton induction

is-subsingleton :
  (l1 : Level) {l2 : Level} (A : UU l2)  UU (lsuc l1  l2)
is-subsingleton l A = {B : A  UU l} (a : A)  section (ev-point a {B})

ind-is-subsingleton :
  {l1 l2 : Level} {A : UU l1} 
  ({l : Level}  is-subsingleton l A)  {B : A  UU l2} (a : A) 
  B a  (x : A)  B x
ind-is-subsingleton is-subsingleton-A a = pr1 (is-subsingleton-A a)

compute-ind-is-subsingleton :
  {l1 l2 : Level} {A : UU l1} (H : {l : Level}  is-subsingleton l A) 
  {B : A  UU l2} (a : A)  ev-point a {B}  ind-is-subsingleton H {B} a ~ id
compute-ind-is-subsingleton is-subsingleton-A a = pr2 (is-subsingleton-A a)

Properties

Propositions satisfy subsingleton induction

abstract
  ind-subsingleton :
    {l1 l2 : Level} {A : UU l1} (is-prop-A : is-prop A)
    {B : A  UU l2} (a : A)  B a  (x : A)  B x
  ind-subsingleton is-prop-A {B} a =
    ind-singleton a (is-proof-irrelevant-is-prop is-prop-A a) B

abstract
  compute-ind-subsingleton :
    {l1 l2 : Level} {A : UU l1}
    (is-prop-A : is-prop A) {B : A  UU l2} (a : A) 
    ev-point a {B}  ind-subsingleton is-prop-A {B} a ~ id
  compute-ind-subsingleton is-prop-A {B} a =
    compute-ind-singleton a (is-proof-irrelevant-is-prop is-prop-A a) B

A type satisfies subsingleton induction if and only if it is a proposition

is-subsingleton-is-prop :
  {l1 l2 : Level} {A : UU l1}  is-prop A  is-subsingleton l2 A
is-subsingleton-is-prop is-prop-A {B} a =
  is-singleton-is-contr a (is-proof-irrelevant-is-prop is-prop-A a) B

abstract
  is-prop-ind-subsingleton :
    {l1 : Level} (A : UU l1) 
    ({l2 : Level} {B : A  UU l2} (a : A)  B a  (x : A)  B x)  is-prop A
  is-prop-ind-subsingleton A S =
    is-prop-is-proof-irrelevant
      ( λ a  is-contr-ind-singleton A a  B  S {B = B} a))

abstract
  is-prop-is-subsingleton :
    {l1 : Level} (A : UU l1)  ({l2 : Level}  is-subsingleton l2 A)  is-prop A
  is-prop-is-subsingleton A S = is-prop-ind-subsingleton A (pr1  S)

Recent changes