# Subsingleton induction

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

Created on 2023-10-20.

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)


## Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

ConceptFile
Propositions (foundation-core)foundation-core.propositions
Propositions (foundation)foundation.propositions
Subterminal typesfoundation.subterminal-types
Subsingleton inductionfoundation.subsingleton-induction
Empty types (foundation-core)foundation-core.empty-types
Empty types (foundation)foundation.empty-types
Unit typefoundation.unit-type
Logical equivalencesfoundation.logical-equivalences
Propositional extensionalityfoundation.propositional-extensionality
Mere logical equivalencesfoundation.mere-logical-equivalences
Conjunctionfoundation.conjunction
Disjunctionfoundation.disjunction
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Negationfoundation.negation
Double negationfoundation.double-negation
Propositional truncationsfoundation.propositional-truncations
Universal property of propositional truncationsfoundation.universal-property-propositional-truncation
The induction principle of propositional truncationsfoundation.induction-principle-propositional-truncation
Functoriality of propositional truncationsfoundation.functoriality-propositional-truncations
Propositional resizingfoundation.propositional-resizing
Impredicative encodings of the logical operationsfoundation.impredicative-encodings