# Coinhabited pairs of types

```agda
module foundation.coinhabited-pairs-of-types where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

Two types `A` and `B` are said to be
{{#concept "coinhabited" Agda=is-coinhabited}} if `A` is
[inhabited](foundation.inhabited-types.md)
[if and only if](foundation.logical-equivalences.md) `B` is.

## Definitions

### The predicate of being coinhabited

```agda
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

```agda
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

```agda
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

```agda
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

```agda
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

- [Mere logical equivalence of types](foundation.mere-logical-equivalences.md)
  is a related but stronger notion than coinhabitedness.