# 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.

## Instances For

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.

## Instances For

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.

## Instances For

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.sumEmbeddingEquivProdEmbeddingDisjoint.trans Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted

## Instances For

Embeddings from a single-member type are equivalent to members of the target type.