Coinhabited pairs of types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.coinhabited-pairs-of-types where
Imports 
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.propositions

Idea

Two types A and B are said to be coinhabited if A is inhabited if and only if B is.

Definitions

The predicate of being coinhabited

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

  is-coinhabited-Prop : Prop (l1 ⊔ l2)
  is-coinhabited-Prop = iff-Prop (is-inhabited-Prop A) (is-inhabited-Prop B)

  is-coinhabited : UU (l1 ⊔ l2)
  is-coinhabited = type-Prop is-coinhabited-Prop

Forward and backward implications of coinhabited types

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

  forward-implication-is-coinhabited :
    is-coinhabited A B → is-inhabited A → is-inhabited B
  forward-implication-is-coinhabited = forward-implication

  forward-implication-is-coinhabited' : is-coinhabited A B → A → is-inhabited B
  forward-implication-is-coinhabited' e a =
    forward-implication e (unit-trunc-Prop a)

  backward-implication-is-coinhabited :
    is-coinhabited A B → is-inhabited B → is-inhabited A
  backward-implication-is-coinhabited = backward-implication

  backward-implication-is-coinhabited' : is-coinhabited A B → B → is-inhabited A
  backward-implication-is-coinhabited' e b =
    backward-implication e (unit-trunc-Prop b)

Every type is coinhabited with itself

module _
  {l : Level} (A : UU l)
  where

  is-reflexive-is-coinhabited : is-coinhabited A A
  is-reflexive-is-coinhabited = id-iff

Coinhabitedness is a transitive relation

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  where

  is-transitive-is-coinhabited :
    is-coinhabited B C → is-coinhabited A B → is-coinhabited A C
  is-transitive-is-coinhabited = _∘iff_

Coinhabitedness is a symmetric relation

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

  is-symmetric-is-coinhabited : is-coinhabited A B → is-coinhabited B A
  is-symmetric-is-coinhabited = inv-iff

See also

Recent changes