# 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