# Equivalences on embeddings #

This file shows some advanced equivalences on embeddings, useful for constructing larger embeddings from smaller ones.

Embeddings from a sum type are equivalent to two separate embeddings with disjoint ranges.

## Equations

- One or more equations did not get rendered due to their size.

Embeddings whose range lies within a set are equivalent to embeddings to that set.
This is `Function.Embedding.codRestrict`

as an equiv.

## Equations

- One or more equations did not get rendered due to their size.

Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings, in which the second embedding cannot take values in the range of the first.

## Equations

- One or more equations did not get rendered due to their size.

A combination of the above results, allowing us to turn one embedding over a sum type into two dependent embeddings, the second of which avoids any members of the range of the first. This is helpful for constructing larger embeddings out of smaller ones.

## Equations

- Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted = Equiv.trans Equiv.sumEmbeddingEquivProdEmbeddingDisjoint Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted