Definitions: Mathlib.Data, part 5 of 6

Let $o$ be an element of $\operatorname{Options}$. Then $\operatorname{getPPNumericProjProd}$ applied to $o$ is an element of $\mathrm{Bool}$ defined as $\operatorname{get}$ applied to $o$, $\operatorname{name}$ applied to the product and $\operatorname{defValue}$ applied to the product.

the product (from the name)

The product is an element of $\operatorname{Option}$ applied to $\mathrm{Bool}$.

the injection arrow of h and x6 (from the name)

Assume that $\EqtMACRoH {\ProdmkMACRoU {x_{2}}{x_{3}}}{\ProdmkMACRoU {x_{4}}{x_{5}}}$. Let $x_{6}$ be a function from elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {x_{2}}{x_{4}}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {x_{3}}{x_{5}}$ to elements of $P$. Then the injection arrow of $h$ and $x_{6}$ is an element of $P$.

the injection arrow of h and x6 (from the name)

Assume that $\EqtMACRoH {\ProdmkMACRoU {x_{2}}{x_{3}}}{\ProdmkMACRoU {x_{4}}{x_{5}}}$. Let $x_{6}$ be a function from elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {x_{2}}{x_{4}}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {x_{3}}{x_{5}}$ to elements of $P$. Then the injection arrow of $h$ and $x_{6}$ is an element of $P$.

product of x1 and l (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Let $l$ be a list of elements of $x$. Then a product of $x_{1}$ and $l$ is an element of the function that maps $x_{1}$ and $l$ to $\operatorname{foldr}$ applied to the function that maps $i$ and $x_{2}$ to $\mathrm{Prod}$ applied to $x_{1}$ applied to $i$ and $x_{2}$, $\mathrm{PUnit}$ and $l$.

the eliminator of x3 and h (from the name)

Let $x_{3}$ be a product of $x_{1}$ and $l$. Assume that $i$ is an element of $l$. Then the eliminator of $x_{3}$ and $h$ is an element of $x_{1}$ applied to $i$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{List\_\_TProd\_\_elim\_\_\_f}$, $x_{3}$, $i$ and $h$.

the eliminator of v and i (from the name)

Assume that for all elements $i_{1}$ of $x$, $i_{1}$ is an element of $l$. Let $v$ be a product of $x_{1}$ and $l$. Let $i$ be an element of $x$. Then the eliminator of $v$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the eliminator of $v$ and $h$ applied to $i$.

Let $l$ be a list of elements of $x$. Let $\mathrm{\_f}$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\operatorname{mk}$ applied to $l$, $i$ and $\mathrm{\_f}$ is a product of $x_{1}$ and $l$ defined as the function that maps $\mathrm{\_f}$ to $\operatorname{brecOn}$ applied to $l$, $\mathrm{List\_\_TProd\_\_mk\_\_\_f}$, $i$ and $\mathrm{\_f}$.

the product equivalence product of hnd and h (from the name)

Assume that $\operatorname{Nodup}$ holds for $l$. Assume that for all elements $i_{1}$ of $x$, $i_{1}$ is an element of $l$. Then the product equivalence product of $\mathrm{hnd}$ and $h$ is an equivalence from the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ to the set of products of $x_{1}$ and $l$.

Let $l$ be a list of elements of $x$. Let $\mathrm{\_t}$ be a function from elements $i$ of $x$ to elements of $\wp x_{1} (i)$. Then $\operatorname{tprod}$ applied to $l$, $i$ and $\mathrm{\_t}$ is an element of the power set of the set of products of $x_{1}$ and $l$ defined as the function that maps $\mathrm{\_t}$ to $\operatorname{brecOn}$ applied to $l$, $\mathrm{Set\_\_tprod\_\_\_f}$, $i$ and $\mathrm{\_t}$.

Let $F$ be a function from type vectors of $n$ to sets. Then we can say that $\mathrm{MvQPF}$ holds for $F$.

$\operatorname{IsUniform}$, if for all type vectors $x$ of $n$, for all elements $a$ and $\mathrm{a'}$ of $\operatorname{A}$ applied to $\operatorname{P}$ applied to $F$, for all arrows $f$ of $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ and $a$ and $x$, for all arrows $\mathrm{f'}$ of $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ and $\mathrm{a'}$ and $x$, if the absolute value of $\operatorname{mk}$ applied to $a$ and $f$ is equal to the absolute value of $\operatorname{mk}$ applied to $\mathrm{a'}$ and $\mathrm{f'}$, then for all elements $i$ of $\mathrm{Fin2}$ applied to $n$, the image of $f$ applied to $i$ and the universal set is equal to the image of $\mathrm{f'}$ applied to $i$ and the universal set.

$\operatorname{LiftPPreservation}$, if for all type vectors $x$ of $n$, for all functions $p$ from elements $i$ of $\mathrm{Fin2}$ applied to $n$ and elements of $x$ applied to $i$ to propositions, for all objects $x_{1}$ of $\operatorname{P}$ applied to $F$ and $x$, $\operatorname{LiftP}$ holds for $p$ and the absolute value of $x_{1}$, if and only if $\operatorname{LiftP}$ holds for $p$ and $x_{1}$.

Let $F$ be a function from type vectors of $n$ to sets. Then $\operatorname{P}$ applied to $F$ is a multivariate functor of $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

$\operatorname{SuppPreservation}$, if for all type vectors $x$ of $n$, for all objects $x_{1}$ of $\operatorname{P}$ applied to $F$ and $x$, $\operatorname{supp}$ applied to the absolute value of $x_{1}$ is equal to $\operatorname{supp}$ applied to $x_{1}$.

the absolute value of x1 (from the name)

Let $x_{1}$ be an object of $\operatorname{P}$ applied to $F$ and $x$. Then the absolute value of $x_{1}$ is an element of $F$ applied to $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{1}$.

the representation of x1 (from the name)

Let $x_{1}$ be an element of $F$ applied to $x$. Then the representation of $x_{1}$ is an object of $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{1}$.

Let $F$ be a function from type vectors of $n + 1$ to sets. Let $x_{1}$ be a type vector of $n$. Then an element of $\operatorname{Cofix}$ applied to $F$ and $x_{1}$ is an element of the function that maps $F$ and $x_{1}$ to $\mathrm{Quot}$ applied to $\operatorname{Mcongr}$.

the absolute value of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then the absolute value of $x_{1}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Mcongr}$ and $x_{1}$.

Let $g$ be a function from elements of $x_{1}$ to elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{corec}$ applied to $g$ and $x_{2}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Mcongr}$ and $\operatorname{corecF}$ applied to $g$ and $x_{2}$.

Let $g$ be a function from elements of $x_{1}$ to elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\mathrm{Sum}$ applied to $\operatorname{Cofix}$ applied to $F$ and $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{corec'}$ applied to $g$ and $x_{2}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as $\operatorname{corec}$ applied to $\operatorname{elim}$ applied to $\operatorname{comp}$ applied to $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{inl}$ and $\operatorname{dest}$ and $g$ and $\operatorname{inr}$ applied to $x_{2}$.

Let $g$ be a function from sets $X$ and functions from elements of $x_{1}$ to elements of $X$ to elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $X$. Let $x_{2}$ be an element of $x_{1}$. Then $\mathrm{MvQPF\_\_Cofix\_\_corec'\_u2081\_}$ applied to $X$, $g$ and $x_{2}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as the function that maps $x_{2}$ to $\operatorname{corec}$ applied to the function that maps $x_{3}$ to $X$ applied to $x_{1}$ and $\mathrm{id}$, $g$ and $x_{2}$.

Let $g$ be a function from sets $X$ and functions from elements of $\operatorname{Cofix}$ applied to $F$ and $x$ to elements of $X$ and functions from elements of $x_{1}$ to elements of $X$ and elements of $x_{1}$ to elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $X$. Let $x_{2}$ be an element of $x_{1}$. Then $\mathrm{MvQPF\_\_Cofix\_\_corec\_u2081\_}$ applied to $X$, $g$ and $x_{2}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as the function that maps $x_{2}$ to $\operatorname{corec'}$ applied to the function that maps $x_{3}$ to $X$ applied to $\mathrm{Sum}$ applied to $\operatorname{Cofix}$ applied to $F$ and $x$ and $x_{1}$, $\operatorname{inl}$, $\operatorname{inr}$ and $x_{3}$, $g$ and $x_{2}$.

Let $x_{1}$ be an element of $\operatorname{Cofix}$ applied to $F$ and $x$. Then $\operatorname{dest}$ applied to $x_{1}$ is an element of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\operatorname{Cofix}$ applied to $F$ and $x$.

the map function for the functor of g and x2 (from the docstring)

Let $g$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\operatorname{Cofix}$ applied to $F$ and $x$. Then the map function for the functor of $g$ and $x_{2}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x_{1}$.

Let $x_{1}$ be an element of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\operatorname{Cofix}$ applied to $F$ and $x$. Then $\operatorname{mk}$ applied to $x_{1}$ is an element of $\operatorname{Cofix}$ applied to $F$ and $x$ defined as $\operatorname{corec}$ applied to the function that maps $x_{1}$ to $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and the function that maps $i$ to $\operatorname{dest}$ applied to $i$ and $x_{1}$ and $x_{1}$.

the representation of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{Cofix}$ applied to $F$ and $x$. Then the representation of $x_{1}$ is an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{corec}$ applied to $\operatorname{P}$ applied to $F$, $\operatorname{comp}$ applied to $\operatorname{repr}$ and $\operatorname{dest}$ and $x_{1}$.

Let $r$ be a function from elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ and elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ to propositions. Then $\operatorname{IsPrecongr}$ holds for $r$, if for all elements $x_{1}$ and $y$ of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$, if $r$ holds for $x_{1}$ and $y$, then the absolute value of $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{mk}$ applied to $r$ and $\operatorname{dest}$ applied to $\operatorname{P}$ applied to $F$ and $x_{1}$ is equal to the absolute value of $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{mk}$ applied to $r$ and $\operatorname{dest}$ applied to $\operatorname{P}$ applied to $F$ and $y$.

Let $x_{1}$ and $y$ be elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then $\operatorname{Mcongr}$ holds for $x_{1}$ and $y$, if there exists a function $r$ from elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ and elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ to propositions, such that $\operatorname{IsPrecongr}$ holds for $r$ and $r$ holds for $x_{1}$ and $y$.

Let $g$ be a function from elements of $x_{1}$ to elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{corecF}$ applied to $g$ and $x_{2}$ is an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{corec}$ applied to $\operatorname{P}$ applied to $F$, the function that maps $x_{2}$ to the representation of $g$ applied to $x_{2}$ and $x_{2}$.

the representation of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then the representation of $x_{1}$ is an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{corecF}$ applied to $\operatorname{comp}$ applied to $\operatorname{abs}$ and $\operatorname{dest}$ applied to $\operatorname{P}$ applied to $F$ and $x_{1}$.

composition of G and v (from the name)

Let $F$ be a function from type vectors of $n$ to sets. Let $G$ be a function from elements of $\mathrm{Fin2}$ applied to $n$ and type vectors of $m$ to sets. Let $v$ be a type vector of $m$. Then a composition of $G$ and $v$ is an element of the function that maps $F$, $G$ and $v$ to $F$ applied to the function that maps $i$ to $G$ applied to $i$ and $v$.

Let $x_{1}$ be a composition of $G$ and $x$. Then $\operatorname{get}$ applied to $x_{1}$ is an element of $F$ applied to the function that maps $i$ to $G$ applied to $i$ and $x$ defined as $x_{1}$.

the map of f and x4 (from the name)

Let $f$ be an arrow of $x$ and $x_{1}$. Let $x_{4}$ be a composition of $G$ and $x$. Then the map of $f$ and $x_{4}$ is a composition of $G$ and $x_{1}$ defined as $\operatorname{map}$ applied to the function that maps $\mathrm{\_i}$ to $\operatorname{map}$ applied to $f$ and $x_{4}$.

the map of f (from the name)

Let $f$ be an arrow of $x$ and $x_{1}$. Then the map of $f$ is an arrow of the function that maps $i$ to $G$ applied to $i$ and $x$ and the function that maps $i_{1}$ to $G$ applied to $i_{1}$ and $x_{1}$ defined as the function that maps $\mathrm{\_i}$ to $\operatorname{map}$ applied to $f$.

Let $x_{1}$ be an element of $F$ applied to the function that maps $i$ to $G$ applied to $i$ and $x$. Then $\operatorname{mk}$ applied to $x_{1}$ is a composition of $G$ and $x$ defined as $x_{1}$.

constant of A and _v (from the name)

Let $n$ be a natural number. Let $A$ be a set. Let $\mathrm{\_v}$ be a type vector of $n$. Then a constant of $A$ and $\mathrm{\_v}$ is an element of the function that maps $n$, $A$ and $\mathrm{\_v}$ to $A$.

Let $x_{1}$ be a constant of $A$ and $x$. Then $\operatorname{get}$ applied to $x_{1}$ is an element of $A$ defined as $x_{1}$.

the map of x2 (from the name)

Let $x_{2}$ be a constant of $A$ and $x$. Then the map of $x_{2}$ is a constant of $A$ and $x_{1}$ defined as $x_{2}$.

Let $x_{1}$ be an element of $A$. Then $\operatorname{mk}$ applied to $x_{1}$ is a constant of $A$ and $x$ defined as $x_{1}$.

Let $F$ be a function from type vectors of $n + 1$ to sets. Let $x$ be a type vector of $n$. Then an element of $\operatorname{Fix}$ applied to $F$ and $x$ is an element of the function that maps $F$ and $x$ to $\mathrm{Quotient}$ applied to $\operatorname{wSetoid}$ applied to $x$.

Let $x_{1}$ be an element of $\operatorname{Fix}$ applied to $F$ and $x$. Then $\operatorname{dest}$ applied to $x_{1}$ is an element of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\operatorname{Fix}$ applied to $F$ and $x$.

Let $g$ be a function from elements $x_{3}$ of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\Sigma$ applied to $x_{1}$ to elements of $x_{1}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{fst}$ and $x_{3}$. Let $x_{2}$ be an element of $\operatorname{Fix}$ applied to $F$ and $x$. Then $\operatorname{drec}$ applied to $x_{3}$, $g$ and $x_{2}$ is an element of $x_{1}$ applied to $x_{2}$.

the map of g and x2 (from the name)

Let $g$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\operatorname{Fix}$ applied to $F$ and $x$. Then the map of $g$ and $x_{2}$ is an element of $\operatorname{Fix}$ applied to $F$ and $x_{1}$.

Let $x_{1}$ be an element of $F$ applied to $\operatorname{append1}$ applied to $x$ and $\operatorname{Fix}$ applied to $F$ and $x$. Then $\operatorname{mk}$ applied to $x_{1}$ is an element of $\operatorname{Fix}$ applied to $F$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $\operatorname{wMk'}$ applied to $\operatorname{P}$ applied to $F$ and $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{fixToW}$ and the representation of $x_{1}$.

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then we can say that $\operatorname{WEquiv}$ holds for $x_{1}$ and $x_{2}$.

Assume that $\operatorname{WEquiv}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $x_{1}$ be an element of $\operatorname{Fix}$ applied to $F$ and $x$. Then $\operatorname{fixToW}$ applied to $x_{1}$ is an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ and $x$.

Let $g$ be a function from elements of $F$ applied to $\operatorname{append1}$ applied to $x$ and $x_{1}$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then $\operatorname{recF}$ applied to $g$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{wRec}$ applied to $\operatorname{P}$ applied to $F$, the function that maps $a$, $\mathrm{f'}$, $\mathrm{\_f}$ and $\mathrm{rec}$ to $g$ applied to the absolute value of $\operatorname{mk}$ applied to $a$ and the split function of $\mathrm{f'}$ and $\mathrm{rec}$ and $x_{2}$.

Let $x_{1}$ be an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ and $x$. Then $\operatorname{wrepr}$ applied to $x_{1}$ is an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{recF}$ applied to $\operatorname{comp}$ applied to $\operatorname{wMk'}$ applied to $\operatorname{P}$ applied to $F$ and $\operatorname{repr}$ and $x_{1}$.

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $v$ be a type vector of $n$. Then an element of $\operatorname{Prj}$ applied to $i$ and $v$ is an element of the function that maps $i$ and $v$ to $v$ applied to $i$.

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Then $\operatorname{P}$ applied to $i$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $\mathrm{PUnit}$ and the function that maps $x$ and $j$ to $\mathrm{ULift}$ applied to $\mathrm{PLift}$ applied to $\EqtMACRoH {i}{j}$.

the absolute value of i and x1 (from the name)

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $x_{1}$ be an object of $\operatorname{P}$ applied to $i$ and $x$. Then the absolute value of $i$ and $x_{1}$ is an element of $\operatorname{Prj}$ applied to $i$ and $x$.

the map of f and x2 (from the name)

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $f$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\operatorname{Prj}$ applied to $i$ and $x$. Then the map of $f$ and $x_{2}$ is an element of $\operatorname{Prj}$ applied to $i$ and $x_{1}$ defined as $f$ applied to $i$ and $x_{2}$.

the representation of i and x1 (from the name)

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $x_{1}$ be an element of $\operatorname{Prj}$ applied to $i$ and $x$. Then the representation of $i$ and $x_{1}$ is an object of $\operatorname{P}$ applied to $i$ and $x$.

quotient of R and x1 (from the name)

Let $R$ be a function from type vectors $x_{1}$ of $n$ and elements of $F$ applied to $x_{1}$ and elements of $F$ applied to $x_{1}$ to propositions. Let $x$ be a type vector of $n$. Then a quotient of $x_{1}$ and $R$ is an element of the function that maps $R$, $x$ and $x$ to $\mathrm{Quot}$ applied to $x_{1}$ applied to $R$ and $x$.

the map of Hfunc and f (from the name)

Let $R$ be a function from type vectors $x_{6}$ of $n$ and elements of $F$ applied to $x_{6}$ and elements of $F$ applied to $x_{6}$ to propositions such that for all type vectors $x_{4}$ and $x_{5}$ of $n$, for all elements $a$ and $b$ of $F$ applied to $x_{4}$, for all arrows $f_{1}$ of $x_{4}$ and $x_{5}$, if $R$ holds for $x_{4}$, $a$ and $b$, then $R$ holds for $x_{5}$, $\operatorname{map}$ applied to $f_{1}$ and $a$ and $\operatorname{map}$ applied to $f_{1}$ and $b$. Let $f$ be an arrow of $x_{1}$ and $x_{2}$. Let $x_{3}$ be a quotient of $R$ and $x_{1}$. Then the map of $\mathrm{Hfunc}$ and $f$ is a quotient of $R$ and $x_{2}$.

product of F and v (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $v$ be a type vector of $n$. Then a product of $F$ and $v$ is an element of the function that maps $F$ and $v$ to the set of functions from elements $x$ of $A$ to elements of $F$ applied to $x$ and $v$.

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Then $\operatorname{P}$ applied to $F$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to the set of functions from elements $a$ of $A$ to elements of $\operatorname{A}$ applied to $\operatorname{P}$ applied to $F$ applied to $a$ and the function that maps $x_{1}$ and $i$ to $\Sigma$ applied to the function that maps $a_{1}$ to $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ applied to $a_{1}$, $x_{1}$ applied to $a_{1}$ and $i$.

the absolute value of F and x2 (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $x_{2}$ be an object of $\operatorname{P}$ applied to $F$ and $x_{1}$. Then the absolute value of $F$ and $x_{2}$ is a product of $F$ and $x_{1}$.

the representation of F and x2 (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $x_{2}$ be a product of $F$ and $x_{1}$. Then the representation of $F$ and $x_{2}$ is an object of $\operatorname{P}$ applied to $F$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $a$ to $\operatorname{fst}$ applied to the representation of $x_{2}$ applied to $a$ and the function that maps $\mathrm{\_i}$ and $a_{1}$ to $\operatorname{snd}$ applied to the representation of $x_{2}$ applied to $\operatorname{fst}$ applied to $a_{1}$, $\mathrm{\_i}$ and $\operatorname{snd}$ applied to $a_{1}$.

sigma of F and v (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $v$ be a type vector of $n$. Then a sigma of $F$ and $v$ is an element of the function that maps $F$ and $v$ to $\Sigma$ applied to the function that maps $x$ to $F$ applied to $x$ and $v$.

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Then $\operatorname{P}$ applied to $F$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $a$ to $\operatorname{A}$ applied to $\operatorname{P}$ applied to $F$ applied to $a$ and the function that maps $x_{1}$ to $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ applied to $\operatorname{fst}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{1}$.

the absolute value of F and x2 (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $x_{2}$ be an object of $\operatorname{P}$ applied to $F$ and $x_{1}$. Then the absolute value of $F$ and $x_{2}$ is a sigma of $F$ and $x_{1}$.

the representation of F and x2 (from the name)

Let $F$ be a function from elements of $A$ and type vectors of $n$ to sets. Let $x_{2}$ be a sigma of $F$ and $x_{1}$. Then the representation of $F$ and $x_{2}$ is an object of $\operatorname{P}$ applied to $F$ and $x_{1}$.

Let $F$ be a function from sets to sets. Then we can say that $\mathrm{QPF}$ holds for $F$.

Let $F$ be a function from sets to sets. Then an element of $\operatorname{Cofix}$ applied to $F$ is an element of the function that maps $F$ to $\mathrm{Quot}$ applied to $\operatorname{Mcongr}$.

Let $g$ be a function from elements of $x$ to elements of $F$ applied to $x$. Let $x_{1}$ be an element of $x$. Then $\operatorname{corec}$ applied to $g$ and $x_{1}$ is an element of $\operatorname{Cofix}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\operatorname{Mcongr}$ and $\operatorname{corecF}$ applied to $g$ and $x_{1}$.

Let $x$ be an element of $\operatorname{Cofix}$ applied to $F$. Then $\operatorname{dest}$ applied to $x$ is an element of $F$ applied to $\operatorname{Cofix}$ applied to $F$.

Let $F$ be a function from sets to sets. Then an element of $\operatorname{Fix}$ applied to $F$ is an element of the function that maps $F$ to $\mathrm{Quotient}$ applied to $\operatorname{Wsetoid}$.

Let $x$ be an element of $\operatorname{Fix}$ applied to $F$. Then $\operatorname{dest}$ applied to $x$ is an element of $F$ applied to $\operatorname{Fix}$ applied to $F$.

Let $x$ be an element of $F$ applied to $\operatorname{Fix}$ applied to $F$. Then $\operatorname{mk}$ applied to $x$ is an element of $\operatorname{Fix}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $\operatorname{mk}$ applied to the map of $\operatorname{fixToW}$ and the representation of $x$.

Let $r$ be a function from elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ to propositions. Then $\operatorname{IsPrecongr}$ holds for $r$, if for all elements $x$ and $y$ of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$, if $r$ holds for $x$ and $y$, then the absolute value of the map of $\operatorname{mk}$ applied to $r$ and $\operatorname{dest}$ applied to $x$ is equal to the absolute value of the map of $\operatorname{mk}$ applied to $r$ and $\operatorname{dest}$ applied to $y$.

$\operatorname{IsUniform}$, if for all sets $x$, for all elements $a$ and $\mathrm{a'}$ of $\operatorname{A}$ applied to $\operatorname{P}$ applied to $F$, for all functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ and $a$ to elements of $x$, for all functions $\mathrm{f'}$ from elements of $\operatorname{B}$ applied to $\operatorname{P}$ applied to $F$ and $\mathrm{a'}$ to elements of $x$, if the absolute value of $\operatorname{mk}$ applied to $a$ and $f$ is equal to the absolute value of $\operatorname{mk}$ applied to $\mathrm{a'}$ and $\mathrm{f'}$, then the image of $f$ and the universal set is equal to the image of $\mathrm{f'}$ and the universal set.

$\operatorname{LiftpPreservation}$, if for all sets $x$, for all functions $p$ from elements of $x$ to propositions, for all objects $x_{1}$ of $\operatorname{P}$ applied to $F$ and $x$, $\operatorname{Liftp}$ holds for $p$ and the absolute value of $x_{1}$, if and only if $\operatorname{Liftp}$ holds for $p$ and $x_{1}$.

Let $x$ and $x_{1}$ be elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$. Then $\operatorname{Mcongr}$ holds for $x$ and $x_{1}$, if there exists a function $r$ from elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ and elements of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ to propositions, such that $\operatorname{IsPrecongr}$ holds for $r$ and $r$ holds for $x$ and $x_{1}$.

Let $F$ be a function from sets to sets. Then $\operatorname{P}$ applied to $F$ is a functor defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

$\operatorname{SuppPreservation}$, if for all sets $x$, for all objects $x_{1}$ of $\operatorname{P}$ applied to $F$ and $x$, $\operatorname{supp}$ applied to the absolute value of $x_{1}$ is equal to $\operatorname{supp}$ applied to $x_{1}$.

Let $x$ and $x_{1}$ be elements of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$. Then we can say that $\operatorname{Wequiv}$ holds for $x$ and $x_{1}$.

Assume that $\operatorname{Wequiv}$ holds for $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $x$ be an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$. Then $\operatorname{Wrepr}$ applied to $x$ is an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$ defined as $\operatorname{recF}$ applied to $\operatorname{comp}$ applied to $\operatorname{mk}$ and $\operatorname{repr}$ and $x$.

the absolute value of x1 (from the name)

Let $x_{1}$ be an object of $\operatorname{P}$ applied to $F$ and $x$. Then the absolute value of $x_{1}$ is an element of $F$ applied to $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{1}$.

Let $g$ be a function from elements of $x$ to elements of $F$ applied to $x$. Let $x_{1}$ be an element of $x$. Then $\operatorname{corecF}$ applied to $g$ and $x_{1}$ is an element of $\operatorname{M}$ applied to $\operatorname{P}$ applied to $F$ defined as $\operatorname{corec}$ applied to the function that maps $x_{1}$ to the representation of $g$ applied to $x_{1}$ and $x_{1}$.

Let $x$ be an element of $\operatorname{Fix}$ applied to $F$. Then $\operatorname{fixToW}$ applied to $x$ is an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$.

Let $g$ be a function from elements of $F$ applied to $x$ to elements of $x$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $\operatorname{P}$ applied to $F$. Then $\operatorname{recF}$ applied to $g$ and $x_{1}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{QPF\_\_recF\_\_\_f}$ applied to $g$.

the representation of x1 (from the name)

Let $x_{1}$ be an element of $F$ applied to $x$. Then the representation of $x_{1}$ is an object of $\operatorname{P}$ applied to $F$ and $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{1}$.

the factor of s and x1 (from the name)

Let $r$ and $s$ be functions from elements of $x$ and elements of $x$ to propositions such that for all elements $x_{2}$ and $y$ of $x$, if $r$ holds for $x_{2}$ and $y$, then $s$ holds for $x_{2}$ and $y$. Let $x_{1}$ be an element of $\mathrm{Quot}$ applied to $r$. Then the factor of $s$ and $x_{1}$ is an element of $\mathrm{Quot}$ applied to $s$.

Let $\mathrm{qa}$ be an element of $\mathrm{Quot}$ applied to $\mathrm{ra}$. Let $\mathrm{qb}$ be an element of $\mathrm{Quot}$ applied to $\mathrm{rb}$. Let $f$ be a function from elements $a_{1}$ of $x$ and elements $b_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $\operatorname{mk}$ applied to $\mathrm{ra}$ and $a_{1}$ and $\operatorname{mk}$ applied to $\mathrm{rb}$ and $b_{1}$ such that for all elements $b$ of $x_{1}$, for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x$, if $\mathrm{ra}$ holds for $x_{5}$ and $x_{6}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{5}$ and $b$ and $f$ applied to $x_{6}$ and $b$ and for all elements $a$ of $x$, for all elements $x_{3}$ of $x_{1}$, for all elements $x_{4}$ of $x_{1}$, if $\mathrm{rb}$ holds for $x_{3}$ and $x_{4}$, then $\mathrm{HEq}$ holds for $f$ applied to $a$ and $x_{3}$ and $f$ applied to $a$ and $x_{4}$. Then $\mathrm{Quot\_\_hrecOn\_u2082\_}$ applied to $\mathrm{qa}$, $\mathrm{qb}$, $a_{1}$, $b_{1}$, $f$, $\mathrm{ca}$ and $\mathrm{cb}$ is an element of $x_{2}$ applied to $\mathrm{qa}$ and $\mathrm{qb}$.

Let $p$ be an element of $\mathrm{Quot}$ applied to $r$. Let $q$ be an element of $\mathrm{Quot}$ applied to $s$. Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $a$ of $x$, for all elements $x_{5}$ of $x_{1}$, for all elements $x_{6}$ of $x_{1}$, if $s$ holds for $x_{5}$ and $x_{6}$, then $\EqtMACRoH {f (a , x_{5})}{f (a , x_{6})}$ and for all elements $x_{3}$ of $x$, for all elements $x_{4}$ of $x$, for all elements $b$ of $x_{1}$, if $r$ holds for $x_{3}$ and $x_{4}$, then $\EqtMACRoH {f (x_{3} , b)}{f (x_{4} , b)}$. Then $\mathrm{Quot\_\_liftOn\_u2082\_}$ applied to $p$, $q$, $f$, $\mathrm{hr}$ and $\mathrm{hs}$ is an element of $x_{2}$ defined as the lift of $p$ and $q$.

the lift of x3 and x4 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $a$ of $x$, for all elements $x_{7}$ of $x_{1}$, for all elements $x_{8}$ of $x_{1}$, if $s$ holds for $x_{7}$ and $x_{8}$, then $\EqtMACRoH {f (a , x_{7})}{f (a , x_{8})}$ and for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x$, for all elements $b$ of $x_{1}$, if $r$ holds for $x_{5}$ and $x_{6}$, then $\EqtMACRoH {f (x_{5} , b)}{f (x_{6} , b)}$. Let $x_{3}$ be an element of $\mathrm{Quot}$ applied to $r$. Let $x_{4}$ be an element of $\mathrm{Quot}$ applied to $s$. Then the lift of $x_{3}$ and $x_{4}$ is an element of $x_{2}$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, if $\mathrm{ra}$ holds for $a$ and $b$, then $\mathrm{rb}$ holds for $f$ applied to $a$ and $f$ applied to $b$. Let $x_{2}$ be an element of $\mathrm{Quot}$ applied to $\mathrm{ra}$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{Quot}$ applied to $\mathrm{rb}$.

the right map of h and x1 (from the name)

Assume that for all elements $x_{2}$ and $x_{3}$ of $x$, if $\mathrm{ra}$ holds for $x_{2}$ and $x_{3}$, then $\mathrm{ra'}$ holds for $x_{2}$ and $x_{3}$. Let $x_{1}$ be an element of $\mathrm{Quot}$ applied to $\mathrm{ra}$. Then the right map of $h$ and $x_{1}$ is an element of $\mathrm{Quot}$ applied to $\mathrm{ra'}$ defined as the map of $\mathrm{id}$ and $x_{1}$.

the map of x3 and x4 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $a$ of $x$, for all elements $x_{7}$ of $x_{1}$, for all elements $x_{8}$ of $x_{1}$, if $s$ holds for $x_{7}$ and $x_{8}$, then $t$ holds for $f$ applied to $a$ and $x_{7}$ and $f$ applied to $a$ and $x_{8}$ and for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x$, for all elements $b$ of $x_{1}$, if $r$ holds for $x_{5}$ and $x_{6}$, then $t$ holds for $f$ applied to $x_{5}$ and $b$ and $f$ applied to $x_{6}$ and $b$. Let $x_{3}$ be an element of $\mathrm{Quot}$ applied to $r$. Let $x_{4}$ be an element of $\mathrm{Quot}$ applied to $s$. Then the map of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Quot}$ applied to $t$.

Let $q$ be an element of $\mathrm{Quot}$ applied to $r$. Then $\operatorname{out}$ applied to $q$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Quot\_\_exists\_rep}$ applied to $q$.

Let $x_{3}$ be an element of $\mathrm{Quot}$ applied to $r$. Let $x_{4}$ be an element of $\mathrm{Quot}$ applied to $s$. Let $f$ be a function from elements $a$ of $x$ and elements $b$ of $x_{1}$ to elements of $x_{2}$ applied to $\operatorname{mk}$ applied to $r$ and $a$ and $\operatorname{mk}$ applied to $s$ and $b$. Then $\mathrm{Quot\_\_recOnSubsingleton\_u2082\_}$ applied to $x_{3}$, $x_{4}$, $a$, $b$ and $f$ is an element of $x_{2}$ applied to $x_{3}$ and $x_{4}$ defined as the function that maps $b$ and $f$ to $\operatorname{recOnSubsingleton}$ applied to $x_{3}$, the function that maps $a$ to $\operatorname{recOnSubsingleton}$ applied to $x_{4}$ and the function that maps $b$ to $a$ applied to $a$ and $b$, $b$ and $f$.

Let $x_{1}$ be an element of $\mathrm{Quot}$ applied to $r$. Then $\operatorname{unquot}$ applied to $x_{1}$ is an element of $x$.

the choice of f (from the name)

Let $f$ be a function from elements $i$ of $x$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i$. Then the choice of $i$ is an element of $\mathrm{Quotient}$ applied to $\mathrm{inferInstance}$ defined as the function that maps $f$ to $\operatorname{mk}$ applied to $\mathrm{inferInstance}$, the function that maps $i$ to $\operatorname{out}$ applied to $i$ applied to $i$ and $f$.

the evaluation of q and i (from the name)

Let $q$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{inferInstance}$. Let $i$ be an element of $x$. Then the evaluation of $q$ and $i$ is an element of $\mathrm{Quotient}$ applied to $S$ applied to $i$.

Let $\mathrm{qa}$ be an element of $\mathrm{Quotient}$ applied to $x_{1}$. Let $f$ be a function from elements $a$ of $x$ to elements of $x_{2}$ applied to $\operatorname{mk''}$ applied to $a$ such that for all elements $x_{3}$ and $x_{4}$ of $x$, if $\operatorname{Equiv}$ holds for $x_{3}$ and $x_{4}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{3}$ and $f$ applied to $x_{4}$. Then $\operatorname{hrecOn'}$ applied to $\mathrm{qa}$, $a$, $f$ and $c$ is an element of $x_{2}$ applied to $\mathrm{qa}$ defined as the function that maps $c$ to $\operatorname{hrecOn}$ applied to $\mathrm{qa}$, $a$, $f$ and $c$.

Let $\mathrm{qa}$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{sa}$. Let $\mathrm{qb}$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{sb}$. Let $f$ be a function from elements $a$ of $x$ and elements $b$ of $x_{1}$ to elements of $x_{2}$ applied to $\operatorname{mk}$ applied to $\mathrm{sa}$ and $a$ and $\operatorname{mk}$ applied to $\mathrm{sb}$ and $b$ such that for all elements $x_{3}$ of $x$, for all elements $x_{4}$ of $x_{1}$, for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x_{1}$, if $\operatorname{Equiv}$ holds for $x_{3}$ and $x_{5}$, then if $\operatorname{Equiv}$ holds for $x_{4}$ and $x_{6}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{3}$ and $x_{4}$ and $f$ applied to $x_{5}$ and $x_{6}$. Then $\mathrm{Quotient\_\_hrecOn\_u2082\_}$ applied to $\mathrm{qa}$, $\mathrm{qb}$, $a$, $b$, $f$ and $c$ is an element of $x_{2}$ applied to $\mathrm{qa}$ and $\mathrm{qb}$.

Let $\mathrm{qa}$ be an element of $\mathrm{Quotient}$ applied to $x_{2}$. Let $\mathrm{qb}$ be an element of $\mathrm{Quotient}$ applied to $x_{3}$. Let $f$ be a function from elements $a$ of $x$ and elements $b$ of $x_{1}$ to elements of $x_{4}$ applied to $\operatorname{mk''}$ applied to $a$ and $\operatorname{mk''}$ applied to $b$ such that for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x_{1}$, for all elements $x_{7}$ of $x$, for all elements $x_{8}$ of $x_{1}$, if $\operatorname{Equiv}$ holds for $x_{5}$ and $x_{7}$, then if $\operatorname{Equiv}$ holds for $x_{6}$ and $x_{8}$, then $\mathrm{HEq}$ holds for $f$ applied to $x_{5}$ and $x_{6}$ and $f$ applied to $x_{7}$ and $x_{8}$. Then $\mathrm{Quotient\_\_hrecOn\_u2082\_'}$ applied to $\mathrm{qa}$, $\mathrm{qb}$, $a$, $b$, $f$ and $c$ is an element of $x_{4}$ applied to $\mathrm{qa}$ and $\mathrm{qb}$ defined as the function that maps $f$ and $c$ to $\mathrm{Quotient\_\_hrecOn\_u2082\_}$ applied to $\mathrm{qa}$, $\mathrm{qb}$, $a$, $b$, $f$ and $c$.

Let $q$ be an element of $\mathrm{Quotient}$ applied to $x_{2}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, if $\operatorname{r}$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn'}$ applied to $q$, $f$ and $h$ is an element of $x_{1}$ defined as $\operatorname{liftOn}$ applied to $q$, $f$ and $h$.

Let $x_{5}$ be an element of $\mathrm{Quotient}$ applied to $x_{3}$. Let $x_{6}$ be an element of $\mathrm{Quotient}$ applied to $x_{4}$. Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $x_{7}$ of $x$, for all elements $x_{8}$ of $x_{1}$, for all elements $x_{9}$ of $x$, for all elements $x_{10}$ of $x_{1}$, if $\operatorname{r}$ holds for $x_{7}$ and $x_{9}$, then if $\operatorname{r}$ holds for $x_{8}$ and $x_{10}$, then $\EqtMACRoH {f (x_{7} , x_{8})}{f (x_{9} , x_{10})}$. Then $\mathrm{Quotient\_\_liftOn\_u2082\_'}$ applied to $x_{5}$, $x_{6}$, $f$ and $h$ is an element of $x_{2}$ defined as $\mathrm{Quotient\_\_liftOn\_u2082\_}$ applied to $x_{5}$, $x_{6}$, $f$ and $h$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, if $\operatorname{Equiv}$ holds for $a$ and $b$, then $\operatorname{Equiv}$ holds for $f$ applied to $a$ and $f$ applied to $b$. Let $x_{2}$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{sa}$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{Quotient}$ applied to $\mathrm{sb}$ defined as the map of $f$ and $x_{2}$.

the map of f and x4 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, if $\operatorname{r}$ holds for $a$ and $b$, then $\operatorname{r}$ holds for $f$ applied to $a$ and $f$ applied to $b$. Let $x_{4}$ be an element of $\mathrm{Quotient}$ applied to $x_{2}$. Then the map of $f$ and $x_{4}$ is an element of $\mathrm{Quotient}$ applied to $x_{3}$ defined as the map of $f$ and $x_{4}$.

the map of x3 and x4 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $x_{5}$ and $x_{6}$ of $x$, if $\operatorname{Equiv}$ holds for $x_{5}$ and $x_{6}$, then for all elements $x_{7}$ and $x_{8}$ of $x_{1}$, if $\operatorname{Equiv}$ holds for $x_{7}$ and $x_{8}$, then $\operatorname{Equiv}$ holds for $f$ applied to $x_{5}$ and $x_{7}$ and $f$ applied to $x_{6}$ and $x_{8}$. Let $x_{3}$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{sa}$. Let $x_{4}$ be an element of $\mathrm{Quotient}$ applied to $\mathrm{sb}$. Then the map of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Quotient}$ applied to $\mathrm{sc}$.

the map of x6 and x7 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $x_{8}$ and $x_{9}$ of $x$, if $\operatorname{r}$ holds for $x_{8}$ and $x_{9}$, then for all elements $x_{10}$ and $x_{11}$ of $x_{1}$, if $\operatorname{r}$ holds for $x_{10}$ and $x_{11}$, then $\operatorname{r}$ holds for $f$ applied to $x_{8}$ and $x_{10}$ and $f$ applied to $x_{9}$ and $x_{11}$. Let $x_{6}$ be an element of $\mathrm{Quotient}$ applied to $x_{3}$. Let $x_{7}$ be an element of $\mathrm{Quotient}$ applied to $x_{4}$. Then the map of $x_{6}$ and $x_{7}$ is an element of $\mathrm{Quotient}$ applied to $x_{5}$ defined as the map of $x_{6}$ and $x_{7}$.

Let $a$ be an element of $x$. Then $\operatorname{mk''}$ applied to $a$ is an element of $\mathrm{Quotient}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $a$.

Let $x_{1}$ be an element of $\mathrm{Quotient}$ applied to $s$. Then $\operatorname{out}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{out}$ applied to $x_{1}$.

Let $q$ be an element of $\mathrm{Quotient}$ applied to $x_{1}$. Let $f$ be a function from elements $a$ of $x$ to elements of $x_{2}$ applied to $\operatorname{mk''}$ applied to $a$. Then $\operatorname{recOnSubsingleton'}$ applied to $q$, $a$ and $f$ is an element of $x_{2}$ applied to $q$ defined as the function that maps $f$ to $\operatorname{recOnSubsingleton}$ applied to $q$, $a$ and $f$.

Let $x_{5}$ be an element of $\mathrm{Quotient}$ applied to $x_{2}$. Let $x_{6}$ be an element of $\mathrm{Quotient}$ applied to $x_{3}$. Let $f$ be a function from elements $x_{7}$ of $x$ and elements $x_{8}$ of $x_{1}$ to elements of $x_{4}$ applied to $\operatorname{mk''}$ applied to $x_{7}$ and $\operatorname{mk''}$ applied to $x_{8}$. Then $\mathrm{Quotient\_\_recOnSubsingleton\_u2082\_'}$ applied to $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $f$ is an element of $x_{4}$ applied to $x_{5}$ and $x_{6}$ defined as the function that maps $x_{8}$ and $f$ to $\mathrm{Quotient\_\_recOnSubsingleton\_u2082\_}$ applied to $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $f$.

truncation of x (from the name)

Let $x$ be a set. Then a truncation of $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\mathrm{trueSetoid}$.

Let $q$ be a truncation of $x$. Let $f$ be a function from elements of $x$ to truncations of $x_{1}$. Then $\operatorname{bind}$ applied to $q$ and $f$ is a truncation of $x_{1}$.

the lift of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{2}$ be a truncation of $x$. Then the lift of $f$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{lift}$ applied to $f$, the function that maps $a$, $b$ and $h$ to $c$ applied to $a$ and $b$ and $x_{2}$.

Let $q$ be a truncation of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $q$, $f$ and $c$ is an element of $x_{1}$ defined as the lift of $f$ and $q$.

the map of f and q (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $q$ be a truncation of $x$. Then the map of $f$ and $q$ is a truncation of $x_{1}$ defined as $\operatorname{bind}$ applied to $q$ and $\operatorname{comp}$ applied to $\operatorname{mk}$ and $f$.

Let $a$ be an element of $x$. Then $\operatorname{mk}$ applied to $a$ is a truncation of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $a$.

Let $x_{1}$ be a truncation of $x$. Then $\operatorname{out}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{out}$ applied to $x_{1}$.

Let $q$ be a truncation of $x$. Let $f$ be a function from elements $a_{1}$ of $x$ to elements of $C$ applied to $\operatorname{mk}$ applied to $a_{1}$ such that for all elements $a$ and $b$ of $x$, $\EqtMACRoH {\operatorname{ndrec} (f (a), \operatorname{eq} (\operatorname{mk} (a), \operatorname{mk} (b)))}{f (b)}$. Then $\operatorname{recOn}$ applied to $q$, $a_{1}$, $f$ and $h$ is an element of $C$ applied to $q$.

Let $q$ be a truncation of $x$. Let $f$ be a function from elements $a$ of $x$ to elements of $C$ applied to $\operatorname{mk}$ applied to $a$. Then $\operatorname{recOnSubsingleton}$ applied to $q$, $a$ and $f$ is an element of $C$ applied to $q$.

the cast homomorphism of x (from the name)

Let $x$ be a set. Then the cast homomorphism of $x$ is a ring homomorphism of the set of nonnegative rational numbers and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{cast}$ and $\mathrm{NNRat\_\_cast\_one}$ and $\mathrm{NNRat\_\_cast\_mul}$, $\mathrm{NNRat\_\_cast\_zero}$ and $\mathrm{NNRat\_\_cast\_add}$.

the cast homomorphism of x (from the name)

Let $x$ be a set. Then the cast homomorphism of $x$ is a ring homomorphism of $\Rational$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{cast}$ and $\mathrm{Rat\_\_cast\_one}$ and $\mathrm{Rat\_\_cast\_mul}$, $\mathrm{Rat\_\_cast\_zero}$ and $\mathrm{Rat\_\_cast\_add}$.

the cast order embedding (from the name)

The cast order embedding is an order embedding of the set of nonnegative rational numbers and $K$ defined as the order embedding of $\operatorname{cast}$ and $\mathrm{NNRat\_\_cast\_strictMono}$.

the cast order embedding (from the name)

The cast order embedding is an order embedding of $\Rational$ and $K$ defined as the order embedding of $\operatorname{cast}$ and $\mathrm{Rat\_\_cast\_strictMono}$.

Let $a$ be a rational number. Let $\mathrm{div}$ be a function from integers $n$ and natural numbers $d$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (d , 0)$ and elements of $\mathrm{Proof}$ applied to $\NatCoprimeMACRoC {\IntnatAbsMACRoY {n}}{d}$ to elements of $C$ applied to $\frac{ n}{d}$. Then $\operatorname{divCasesOn}$ applied to $a$, $n$, $d$ and $\mathrm{div}$ is an element of $C$ applied to $a$.

$\operatorname{evalIntCeil}$ is an element of $\operatorname{NormNumExt}$.

the evaluation integer floor (from the name)

The evaluation integer floor is an element of $\operatorname{NormNumExt}$.

$\operatorname{evalIntFract}$ is an element of $\operatorname{NormNumExt}$.

the evaluation round (from the name)

The evaluation round is an element of $\operatorname{NormNumExt}$.

nonnegative rational number (from the name)

A nonnegative rational number is an element of $\SubtypeSet {q}{\mathrm{Leq} (0 , q)}$.

the cast of x1 (from the name)

Let $x_{1}$ be a nonnegative rational number. Then the cast of $x_{1}$ is an element of $K$ defined as $\operatorname{nnratCast}$ applied to $x_{1}$.

the denominator of q (from the docstring)

Let $q$ be a nonnegative rational number. Then the denominator of $q$ is a natural number defined as $\operatorname{den}$ applied to the cast of $q$.

the numerator of q (from the docstring)

Let $q$ be a nonnegative rational number. Then the numerator of $q$ is a natural number defined as the absolute value of $\operatorname{num}$ applied to the cast of $q$.

K is a nonnegative rational number cast (from the name)

Let $K$ be a set. Then we can say that $K$ is a nonnegative rational number cast.

Let $x$ be a nonnegative rational number. Then $\operatorname{nnratCast}$ applied to $x$ is an element of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

Let $x$ be a rational number. Then $\operatorname{pnatDen}$ applied to $x$ is a positive natural number defined as $\operatorname{den}$ applied to $x$.

the rational number square root of x and prec (from the name)

Let $x$ and $\mathrm{prec}$ be natural numbers. Then the rational number square root of $x$ and $\mathrm{prec}$ is a rational number defined as $\frac{ \NatsqrtMACRoD {(x \times \mathrm{prec} ^ {2})}}{\mathrm{prec}}$.

the square root of q (from the name)

Let $q$ be a rational number. Then the square root of $q$ is a rational number defined as $\mathrm{mkRat}$ applied to the square root of $\operatorname{num}$ applied to $q$ and $\NatsqrtMACRoD {\operatorname{den} (q)}$.

Let $x$ be a set. Then the elements of $\mathrm{Semiquot}$ applied to $x$ are a basic type.

q is pure (from the name)

Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then $q$ is pure, if for all elements $a$ of $x$, if $a$ is an element of $q$, then for all elements $b$ of $x$, if $b$ is an element of $q$, then $\EqtMACRoH {a}{b}$.

Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{Semiquot}$ applied to $x_{1}$. Then $\operatorname{bind}$ applied to $q$ and $f$ is an element of $\mathrm{Semiquot}$ applied to $x_{1}$ defined as $\operatorname{mk'}$ applied to the union of the function that maps $a$ to the union of the function that maps $h$ to $\operatorname{s}$ applied to $f$ applied to $a$ and $\operatorname{bind}$ applied to the value of $q$ and the function that maps $a_{1}$ to the map of the function that maps $b$ to $b$ and the value of $f$ applied to $a_{1}$.

Let $s$ be an element of $\wp x$. Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then $\operatorname{blur}$ applied to $s$ and $q$ is an element of $\mathrm{Semiquot}$ applied to $x$.

Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$ such that $\operatorname{s} (q)\leq s$. Then $\operatorname{blur'}$ applied to $q$ and $h$ is an element of $\mathrm{Semiquot}$ applied to $x$.

Let $q$ be a pure element of $\mathrm{Semiquot}$ applied to $x$. Then $\operatorname{get}$ applied to $q$ and $h$ is an element of $x$ defined as $\operatorname{liftOn}$ applied to $q$, $\mathrm{id}$ and $h$.

Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ of $x$, if $a$ is an element of $q$, then for all elements $b$ of $x$, if $b$ is an element of $q$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $q$, $f$ and $h$ is an element of $x_{1}$.

the map of f and q (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then the map of $f$ and $q$ is an element of $\mathrm{Semiquot}$ applied to $x_{1}$ defined as $\operatorname{mk'}$ applied to the image of $f$ and $\operatorname{s}$ applied to $q$ and the map of the function that maps $x_{2}$ to $f$ applied to $x_{2}$ and the value of $q$.

Assume that $a$ is an element of $s$. Then $\operatorname{mk}$ applied to $h$ is an element of $\mathrm{Semiquot}$ applied to $x$ defined as $\operatorname{mk'}$ applied to $s$ and $\operatorname{mk}$ applied to $a$.

Let $q$ be a truncation of $x$. Then $\operatorname{ofTrunc}$ applied to $q$ is an element of $\mathrm{Semiquot}$ applied to $x$ defined as $\operatorname{mk'}$ applied to the universal set and the map of the function that maps $a$ to $a$ and $q$.

Let $a$ be an element of $x$. Then $\operatorname{pure}$ applied to $a$ is an element of $\mathrm{Semiquot}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\mathrm{Set\_\_mem\_singleton}$ applied to $a$.

Let $\mathrm{self}$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then $\operatorname{s}$ applied to $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the truncation of q (from the name)

Let $q$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then the truncation of $q$ is a truncation of $x$ defined as the map of the function that maps $x_{1}$ to $\MembershipmemMACRoT {\operatorname{s} (q)}{x_{1}}$ and the value of $q$.

the universal set (from the name)

The universal set is an element of $\mathrm{Semiquot}$ applied to $x$.

the value of self (from the name)

Let $\mathrm{self}$ be an element of $\mathrm{Semiquot}$ applied to $x$. Then the value of $\mathrm{self}$ is a truncation of the set of elements of $\operatorname{s}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $s$ be a sequence of $x$. Let $f$ be a function from elements of $x$ to sequences of $x_{1}$. Then $\operatorname{bind}$ applied to $s$ and $f$ is a sequence of $x_{1}$ defined as the join of the map of $f$ and $s$.

the join of x1 (from the name)

Let $x_{1}$ be a sequence of the set of sequences of $x$. Then the join of $x_{1}$ is a sequence of $x$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a sequence of $x$. Then the map of $f$ and $x_{2}$ is a sequence of $x_{1}$.

Let $a$ be an element of $x$. Then $\operatorname{ret}$ applied to $a$ is a sequence of $x$ defined as $\ProdmkMACRoU {a}{\operatorname{nil}}$.

the sequence of x1 (from the name)

Let $x_{1}$ be a sequence of $x$. Then the sequence of $x_{1}$ is a sequence of $x$.

computation of x (from the name)

Let $x$ be a set. Then a computation of $x$ is an element of the function that maps $x$ to $\SubtypeSet {f}{\mathrm{forall} (\Natural , \lambda n . \mathrm{forall} (x , \lambda a . \mathrm{if} (\EqtMACRoH {f (n)}{\operatorname{some} (a)}, \EqtMACRoH {f (n + 1)}{\operatorname{some} (a)})))}$.

Let $f$ be a function from elements of $x$ to computations of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Sum}$ applied to the set of computations of $x$ and the set of computations of $x_{1}$. Then $\operatorname{f}$ applied to $f$ and $x_{2}$ is an element of $\mathrm{Sum}$ applied to $x_{1}$ and $\mathrm{Sum}$ applied to the set of computations of $x$ and the set of computations of $x_{1}$.

Let $x_{2}$ be an element of $\mathrm{Sum}$ applied to $x_{1}$ and the set of computations of $x_{1}$. Then $\operatorname{g}$ applied to $x_{2}$ is an element of $\mathrm{Sum}$ applied to $x_{1}$ and $\mathrm{Sum}$ applied to the set of computations of $x$ and the set of computations of $x_{1}$.

Let $R$ be a function from computations of $x$ and computations of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Sum}$ applied to $x$ and the set of computations of $x$. Then we can say that $\operatorname{BisimO}$ holds for $R$, $x_{1}$ and $x_{2}$.

Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{f}$ applied to $f$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

Let $x_{1}$ and $x_{2}$ be computations of $x$. Then $\operatorname{Equiv}$ holds for $x_{1}$ and $x_{2}$, if for all elements $a$ of $x$, $a$ is an element of $x_{1}$, if and only if $a$ is an element of $x_{2}$.

Let $R$ be a function from computations of $x$ and computations of $x$ to propositions. Then $\operatorname{IsBisimulation}$ holds for $R$, if for all computations $x_{1}$ and $x_{2}$ of $x$, if $R$ holds for $x_{1}$ and $x_{2}$, then $\operatorname{BisimO}$ holds for $R$, $\operatorname{destruct}$ applied to $x_{1}$ and $\operatorname{destruct}$ applied to $x_{2}$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $\mathrm{ca}$ be a computation of $x$. Let $\mathrm{cb}$ be a computation of $x_{1}$. Then $\operatorname{LiftRel}$ holds for $R$, $\mathrm{ca}$ and $\mathrm{cb}$, if for all elements $a$ of $x$, if $a$ is an element of $\mathrm{ca}$, then there exists an element $b$ of $x_{1}$ such that $b$ is an element of $\mathrm{cb}$ and $R$ holds for $a$ and $b$ and for all elements $b_{1}$ of $x_{1}$, if $b_{1}$ is an element of $\mathrm{cb}$, then there exists an element $a_{1}$ of $x$ such that $a_{1}$ is an element of $\mathrm{ca}$ and $R$ holds for $a_{1}$ and $b_{1}$.

Let $s$ be a computation of $x$. Let $a$ be an element of $x$. Then $\operatorname{Mem}$ holds for $s$ and $a$, if $\MembershipmemMACRoT {s}{\operatorname{some} (a)}$.

Let $s$ be a computation of $x$. Let $a$ be an element of $x$. Then $\operatorname{Promises}$ holds for $s$ and $a$, if for all elements $\mathrm{a'}$ of $x$, if $\mathrm{a'}$ is an element of $s$, then $\EqtMACRoH {a}{\mathrm{a'}}$.

Let $s$ be a computation of $x$. Let $a$ be an element of $x$. Let $n$ be a natural number. Then $\operatorname{Results}$ holds for $s$, $a$ and $n$, if there exists an element $h$ of $\MembershipmemMACRoT {s}{a}$, such that the length of $s$ is equal to $n$.

Let $s$ be a computation of $x$. Then we can say that $\operatorname{Terminates}$ holds for $s$.

Let $c$ be a computation of $x$. Let $f$ be a function from elements of $x$ to computations of $x_{1}$. Then $\operatorname{bind}$ applied to $c$ and $f$ is a computation of $x_{1}$ defined as $\operatorname{corec}$ applied to $\operatorname{f}$ applied to $f$ and $\operatorname{inl}$ applied to $c$.

Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{corec}$ applied to $f$ and $b$ is a computation of $x$ defined as $\operatorname{corec'}$ applied to $\operatorname{f}$ applied to $f$ and $\operatorname{inr}$ applied to $b$.

Let $c$ be a computation of $x$. Then $\operatorname{destruct}$ applied to $c$ is an element of $\mathrm{Sum}$ applied to $x$ and the set of computations of $x$.

Let $x$ be a set. Then $\operatorname{empty}$ applied to $x$ is a computation of $x$ defined as the constant of $\operatorname{none}$.

Let $s$ be a computation of $x$. Then $\operatorname{get}$ applied to $s$ is an element of $x$.

the head of c (from the name)

Let $c$ be a computation of $x$. Then the head of $c$ is an element of $\mathrm{Option}$ applied to $x$ defined as the head of $c$.

the join of c (from the name)

Let $c$ be a computation of the set of computations of $x$. Then the join of $c$ is a computation of $x$ defined as $\operatorname{bind}$ applied to $c$ and $\mathrm{id}$.

the length of s (from the name)

Let $s$ be a computation of $x$. Then the length of $s$ is a natural number.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{2}$. Then $\operatorname{lmap}$ applied to $f$ and $x_{3}$ is an element of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a computation of $x$. Then the map of $f$ and $x_{2}$ is a computation of $x_{1}$.

Assume that $a$ is an element of $s$. Let $h_{1}$ be an element of $C$ applied to $\operatorname{pure}$ applied to $a$. Let $h_{2}$ be a function from computations $s_{1}$ of $x$ and elements of $C$ applied to $s_{1}$ to elements of $C$ applied to $\operatorname{think}$ applied to $s_{1}$. Then $\operatorname{memRecOn}$ applied to $M$, $h_{1}$, $s_{1}$ and $h_{2}$ is an element of $C$ applied to $s$.

Let $x_{1}$ be a computation of $x$. Let $x_{2}$ be a function from elements of $\mathrm{Unit}$ to computations of $x$. Then $\operatorname{orElse}$ applied to $x_{1}$ and $x_{2}$ is a computation of $x$.

Let $a$ be an element of $x$. Then $\operatorname{pure}$ applied to $a$ is a computation of $x$ defined as the constant of $\operatorname{some}$ applied to $a$.

Let $s$ be a computation of $x$. Let $\mathrm{pure}$ be a function from elements $a$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{pure}$ applied to $a$. Let $\mathrm{think}$ be a function from computations $s_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{think}$ applied to $s_{1}$. Then $\operatorname{recOn}$ applied to $s$, $a$, $\mathrm{pure}$, $s_{1}$ and $\mathrm{think}$ is an element of $\mathrm{motive}$ applied to $s$.

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{rmap}$ applied to $f$ and $x_{3}$ is an element of $\mathrm{Sum}$ applied to $x$ and $x_{2}$.

Let $x_{1}$ be a computation of $x$. Then $\operatorname{run}$ applied to $x_{1}$ is an element of $x$.

Let $x_{1}$ be a computation of $x$. Let $x_{2}$ be a natural number. Then $\operatorname{runFor}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as the proposition that for all natural numbers $n$, for all elements $a$ of $x$, if $\EqtMACRoH {x_{1} (n)}{\operatorname{some} (a)}$, then $\EqtMACRoH {x_{1} (n + 1)}{\operatorname{some} (a)}$.

the tail of c (from the name)

Let $c$ be a computation of $x$. Then the tail of $c$ is a computation of $x$ defined as the tail of $c$.

Let $c$ be a computation of $x$. Then $\operatorname{think}$ applied to $c$ is a computation of $x$ defined as $\operatorname{cons}$ applied to $\operatorname{none}$ and $c$.

Let $c$ be a computation of $x$. Let $x_{1}$ be a natural number. Then $\operatorname{thinkN}$ applied to $c$ and $x_{1}$ is a computation of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Computation\_\_thinkN\_\_\_f}$ applied to $c$.

s is a sequence (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $\mathrm{Option}$ applied to $x$. Then $s$ is a sequence, if for all natural numbers $n$, if $\EqtMACRoH {s (n)}{\operatorname{none}}$, then $\EqtMACRoH {s (n + 1)}{\operatorname{none}}$.

sequence of x (from the name)

Let $x$ be a set. Then a sequence of $x$ is an element of the function that maps $x$ to $\SubtypeSet {f}{\operatorname{IsSeq} (f)}$.

Let $R$ be a function from sequences of $x$ and sequences of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Option}$ applied to the set of sequences of $x$. Then we can say that $\operatorname{BisimO}$ holds for $R$, $x_{1}$ and $x_{2}$.

Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Option}$ applied to $x_{1}$. Then $\operatorname{f}$ applied to $f$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x$ and $\mathrm{Option}$ applied to $x_{1}$.

Let $R$ be a function from sequences of $x$ and sequences of $x$ to propositions. Then $\operatorname{IsBisimulation}$ holds for $R$, if for all sequences $x_{1}$ and $x_{2}$ of $x$, if $R$ holds for $x_{1}$ and $x_{2}$, then $\operatorname{BisimO}$ holds for $R$, $\operatorname{destruct}$ applied to $x_{1}$ and $\operatorname{destruct}$ applied to $x_{2}$.

Let $s$ be a sequence of $x$. Let $a$ be an element of $x$. Then $\operatorname{Mem}$ holds for $s$ and $a$, if $\MembershipmemMACRoT {s}{\operatorname{some} (a)}$.

Let $R$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a sequence of $x$. Then $\operatorname{Pairwise}$ holds for $R$ and $s$, if for all natural numbers $i$ and $j$, if $i < j$, then for all elements $x_{1}$ of $x$, if $\MembershipmemMACRoT {\mathrm{Stream'\_\_Seq\_\_get?} (s , i)}{x_{1}}$, then for all elements $y$ of $x$, if $\MembershipmemMACRoT {\mathrm{Stream'\_\_Seq\_\_get?} (s , j)}{y}$, then $R$ holds for $x_{1}$ and $y$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then $\operatorname{TerminatedAt}$ holds for $s$ and $n$, if $\EqtMACRoH {\mathrm{Stream'\_\_Seq\_\_get?} (s , n)}{\operatorname{none}}$.

Let $s$ be a sequence of $x$. Then $\operatorname{Terminates}$ holds for $s$, if there exists a natural number $n$, such that $\operatorname{TerminatedAt}$ holds for $s$ and $n$.

Let $x_{1}$ and $x_{2}$ be sequences of $x$. Then $\operatorname{append}$ applied to $x_{1}$ and $x_{2}$ is a sequence of $x$.

Let $a$ be an element of $x$. Let $s$ be a sequence of $x$. Then $\operatorname{cons}$ applied to $a$ and $s$ is a sequence of $x$ defined as $\operatorname{cons}$ applied to $\operatorname{some}$ applied to $a$ and $s$.

Let $f$ be a function from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{corec}$ applied to $f$ and $b$ is a sequence of $x$ defined as $\operatorname{corec'}$ applied to $\operatorname{f}$ applied to $f$ and $\operatorname{some}$ applied to $b$.

Let $s$ be a sequence of $x$. Then $\operatorname{destruct}$ applied to $s$ is an element of $\mathrm{Option}$ applied to the set of sequences of $x$ defined as $\operatorname{map}$ applied to the function that maps $\mathrm{a'}$ to $\ProdmkMACRoU {\mathrm{a'}}{\operatorname{tail} (s)}$ and $\mathrm{Stream'\_\_Seq\_\_get?}$ applied to $s$ and $0$.

Let $s$ be a sequence of $x$. Let $x_{1}$ be a natural number. Then $\operatorname{drop}$ applied to $s$ and $x_{1}$ is a sequence of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Stream'\_\_Seq\_\_drop\_\_\_f}$ applied to $s$.

Let $s$ be a sequence of $x$. Then $\operatorname{enum}$ applied to $s$ is a sequence of $\mathrm{Prod}$ applied to $\Natural$ and $x$ defined as $\operatorname{zip}$ applied to $\operatorname{nats}$ and $s$.

the fold of init and f (from the name)

Let $s$ be a sequence of $x$. Let $\mathrm{init}$ be an element of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{1}$. Then the fold of $\mathrm{init}$ and $f$ is a sequence of $x_{1}$.

the force to list of s (from the name)

Let $s$ be a sequence of $x$. Then the force to list of $s$ is a list of elements of $x$ defined as $\operatorname{force}$ applied to $\operatorname{toMLList}$ applied to $s$.

Let $x_{1}$ be a sequence of $x$. Let $x_{2}$ be a natural number. Then $\mathrm{Stream'\_\_Seq\_\_get?}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as the proposition that $x_{1}$ is a sequence.

the head of s (from the name)

Let $s$ be a sequence of $x$. Then the head of $s$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\mathrm{Stream'\_\_Seq\_\_get?}$ applied to $s$ and $0$.

the join of x1 (from the name)

Let $x_{1}$ be a sequence of the set of sequences of $x$. Then the join of $x_{1}$ is a sequence of $x$.

the length of s and h (from the docstring)

Let $s$ be a sequence of $x$ such that $\operatorname{Terminates}$ holds for $s$. Then the length of $s$ and $h$ is a natural number defined as $\operatorname{find}$ applied to $h$.

the length of s (from the name)

Let $s$ be a sequence of $x$. Then the length of $s$ is a natural number defined as $\mathrm{dite}$ applied to $\operatorname{Terminates}$ applied to $s$, the function that maps $h$ to the length of $s$ and $h$ and the function that maps $h_{1}$ to the top.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a sequence of $x$. Then the map of $f$ and $x_{2}$ is a sequence of $x_{1}$.

$\operatorname{nats}$ is a sequence of $\Natural$ defined as the sequence of $\operatorname{nats}$.

$\operatorname{nil}$ is a sequence of $x$ defined as the constant of $\operatorname{none}$.

the sequence of l (from the name)

Let $l$ be a list of elements of $x$. Then the sequence of $l$ is a sequence of $x$ defined as the function that maps $x_{1}$ to $\mathrm{GetElem?\_\_getElem?}$ applied to $l$ and $x_{1}$.

the sequence of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{MLList}$ applied to $\mathrm{Id}$ and $x$. Then the sequence of $x_{1}$ is a sequence of $x$.

the sequence of s (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the sequence of $s$ is a sequence of $x$ defined as the map of $\operatorname{some}$ and $s$.

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\operatorname{omap}$ applied to $f$ and $x_{3}$ is an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{2}$.

Let $s$ be a sequence of $x$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from elements $x_{1}$ of $x$ and sequences $s_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $s_{1}$. Then $\operatorname{recOn}$ applied to $s$, $\mathrm{nil}$, $x_{1}$, $s_{1}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $s$.

the set of n and a (from the name)

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Let $a$ be an element of $x$. Then the set of $n$ and $a$ is a sequence of $x$ defined as $\operatorname{update}$ applied to $s$, $n$ and the function that maps $x_{1}$ to $a$.

Let $x_{1}$ be a natural number. Let $x_{2}$ be a sequence of $x$. Then $\operatorname{splitAt}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to the set of lists of elements of $x$ and the set of sequences of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Stream'\_\_Seq\_\_splitAt\_\_\_f}$ and $x_{2}$.

the tail of s (from the name)

Let $s$ be a sequence of $x$. Then the tail of $s$ is a sequence of $x$ defined as the tail of $s$.

Let $x_{1}$ be a natural number. Let $x_{2}$ be a sequence of $x$. Then $\operatorname{take}$ applied to $x_{1}$ and $x_{2}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Stream'\_\_Seq\_\_take\_\_\_f}$ and $x_{2}$.

the list of s and h (from the name)

Let $s$ be a sequence of $x$ such that $\operatorname{Terminates}$ holds for $s$. Then the list of $s$ and $h$ is a list of elements of $x$ defined as $\operatorname{take}$ applied to the length of $s$ and $h$ and $s$.

the list of s (from the name)

Let $s$ be a sequence of $x$. Then the list of $s$ is a computation of the set of lists of elements of $x$.

Let $s$ be a sequence of $x$. Then $\operatorname{toListOrStream}$ applied to $s$ is an element of $\mathrm{Sum}$ applied to the set of lists of elements of $x$ and $\mathrm{Stream'}$ applied to $x$ defined as $\mathrm{dite}$ applied to $\operatorname{Terminates}$ applied to $s$, the function that maps $h$ to $\operatorname{inl}$ applied to the list of $s$ and $h$ and the function that maps $h_{1}$ to $\operatorname{inr}$ applied to $\operatorname{toStream}$ applied to $s$ and $h_{1}$.

Let $x_{1}$ be a sequence of $x$. Then $\operatorname{toMLList}$ applied to $x_{1}$ is an element of $\mathrm{MLList}$ applied to $\mathrm{Id}$ and $x$.

Let $s$ be a sequence of $x$ such that it is not the case that $\operatorname{Terminates}$ holds for $s$. Then $\mathrm{Stream'}$ holds for $x$.

Let $s$ be a sequence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then $\operatorname{unzip}$ applied to $s$ is an element of $\mathrm{Prod}$ applied to the set of sequences of $x$ and the set of sequences of $x_{1}$ defined as $\ProdmkMACRoU {\operatorname{map} (\ProdfstMACRoZ , s)}{\operatorname{map} (\ProdsndMACRoAA , s)}$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Let $f$ be a function from elements of $x$ to elements of $x$. Then $\operatorname{update}$ applied to $s$, $n$ and $f$ is a sequence of $x$ defined as $\operatorname{update}$ applied to $s$, $n$ and $\operatorname{map}$ applied to $f$ and $n$.

Let $x_{2}$ be a sequence of $x$. Let $x_{3}$ be a sequence of $x_{1}$. Then $\operatorname{zip}$ applied to $x_{2}$ and $x_{3}$ is a sequence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{zipWith}$ applied to $\ProdmkMACRoU$, $x_{2}$ and $x_{3}$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a sequence of $x$. Let $x_{4}$ be a sequence of $x_{1}$. Then $\operatorname{zipWith}$ applied to $f$, $x_{3}$ and $x_{4}$ is a sequence of $x_{2}$ defined as the function that maps $n$ to the map of $\mathrm{Stream'\_\_Seq\_\_get?}$ applied to $x_{3}$ and $n$ and $\mathrm{Stream'\_\_Seq\_\_get?}$ applied to $x_{4}$ and $n$.

sequence of x (from the name)

Let $x$ be a set. Then a sequence of $x$ is an element of the function that maps $x$ to $\mathrm{Prod}$ applied to $x$ and the set of sequences of $x$.

the parallel of S (from the name)

Let $S$ be a sequence of the set of computations of $x$. Then the parallel of $S$ is a computation of $x$.

Let $C$ be a function from elements of $x$ to sets. Let $H$ be a function from computations $s$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S}{s}$ and elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{a_{1}}$ to elements of $C$ applied to $a_{1}$. Assume that $a$ is an element of the parallel of $S$. Then $\operatorname{parallelRec}$ applied to $C$, $s$, $a_{1}$, $H$ and $h$ is an element of $C$ applied to $a$.

Let $p$ be a function from elements of $x$ to propositions. Then $\operatorname{setSubtypeComm}$ applied to $p$ is an equivalence from $\wp (\SubtypeSet {a}{p (a)})$ to $\SubtypeSet {s}{\mathrm{forall} (x , \lambda a_{1} . \mathrm{if} (\MembershipmemMACRoT {s}{a_{1}}, p (a_{1})))}$.

Assume that $s$ is nonempty. Then $\operatorname{some}$ applied to $h$ is an element of $x$ defined as $\operatorname{choose}$ applied to $h$.

the membership equivalence (from the name)

The membership equivalence is an equivalence from $\wp x$ to the set of functions from elements of $x$ to propositions.

the bool indicator of s and x1 (from the name)

Let $s$ be an element of $\wp x$. Let $x_{1}$ be an element of $x$. Then the bool indicator of $s$ and $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\iteMACRoG {(\MembershipmemMACRoT {s}{x_{1}})}{\operatorname{true}}{\operatorname{false}}$.

the cardinality in s (from the docstring)

Let $s$ be an element of $\wp x$. Then the cardinality in $s$ is a natural number defined as the cardinality of the set of elements of $s$.

the cardinality of s (from the docstring)

Let $s$ be an element of $\wp x$. Then the cardinality of $s$ is a natural number defined as the natural number of the cardinality in $s$.

element of s (from the name)

Let $s$ be an element of $\wp x$. Then an element of $s$ is an element of the function that maps $s$ to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$.

S is a finite intersection (from the name)

Let $S$ be an element of $\wp (\wp x)$. Then we can say that $S$ is a finite intersection.

the finite intersection closure of S (from the name)

Let $S$ be an element of $\wp (\wp x)$. Then the finite intersection closure of $S$ is an element of $\wp (\wp x)$.

s is countable (from the name)

Let $s$ be an element of $\wp x$. Then $s$ is countable, if the set of elements of $s$ is countable.

Assume that $s$ is countable. Let $\mathrm{default}$ be an element of $x$. Let $x_{1}$ be a natural number. Then $\operatorname{enumerateCountable}$ applied to $h$, $\mathrm{default}$ and $x_{1}$ is an element of $x$.

set of x (from the name)

Let $x$ be a set. Then the sets of $x$ are a basic type.

Let $\mathrm{self}$ be an element of $\wp x$. Let $x_{1}$ be an element of $x$. Then $\operatorname{Mem}$ holds for $\mathrm{self}$ and $x_{1}$, if $\mathrm{Lean\_Set\_\_proj0}$ holds for $\mathrm{self}$ and $x_{1}$.

s is nonempty (from the name)

Let $s$ be an element of $\wp x$. Then $s$ is nonempty, if there exists an element $x_{1}$ of $x$, such that $x_{1}$ is an element of $s$.

Let $x_{1}$ and $x_{2}$ be elements of $\wp x$. Then $\operatorname{Subset}$ holds for $x_{1}$ and $x_{2}$, if for all elements $a$ of $x$, if $a$ is an element of $x_{1}$, then $a$ is an element of $x_{2}$.

the complement of s (from the docstring)

Let $s$ be an element of $\wp x$. Then the complement of $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is not an element of $s$.

the difference of s and t (from the name)

Let $s$ and $t$ be elements of $\wp x$. Then the difference of $s$ and $t$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is an element of $s$ and $a$ is not an element of $t$.

the image of f and s (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then the image of $f$ and $s$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exists an element $a$ of $x$, such that $a$ is an element of $s$ and $\EqtMACRoH {f (a)}{x_{2}}$.

Let $a$ be an element of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{insert}$ applied to $a$ and $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that $\EqtMACRoH {b}{a}$ or $b$ is an element of $s$.

the intersection of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\wp x$. Then the intersection of $x_{1}$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is an element of $x_{1}$ and $a$ is an element of $x_{2}$.

the powerset of s (from the name)

Let $s$ be an element of $\wp x$. Then the powerset of $s$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (t , s)$.

the singleton of a (from the docstring)

Let $a$ be an element of $x$. Then the singleton of $a$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to $\EqtMACRoH {b}{a}$.

the union of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\wp x$. Then the union of $x_{1}$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is an element of $x_{1}$ or $a$ is an element of $x_{2}$.

the universal set (from the docstring)

The universal set is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{\_a}$ to $\mathrm{True}$.

Let $\mathrm{sel}$ be a function from elements of $\wp x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{1}$ be an element of $\wp x$. Let $x_{2}$ be a natural number. Then $\operatorname{enumerate}$ applied to $\mathrm{sel}$, $x_{1}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Set\_\_enumerate\_\_\_f}$ applied to $\mathrm{sel}$ and $x_{1}$.

Let $s$ be an element of $\wp x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{EquitableOn}$ holds for $s$ and $f$, if for all elements $x_{5}$ and $x_{6}$ of $x$, if $x_{5}$ is an element of $s$, then if $x_{6}$ is an element of $s$, then $f (x_{5})\leq f (x_{6})+ 1$.

$\operatorname{finsetSetFinite}$ is an order isomorphism of the set of finite sets of $x$ and $\SubtypeSet {s}{\operatorname{Finite} (s)}$.

the subtype equivalence to finite set of hs (from the name)

Assume that $s$ is finite. Then the subtype equivalence to finite set of $\mathrm{hs}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})})}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\mathrm{hs})}{x_{2}})})}$.

the finite set of h (from the name)

Assume that $s$ is finite. Then the finite set of $h$ is a finite set of $x$ defined as the finite set of $s$.

the natural embedding of s and h (from the name)

Let $s$ be an infinite element of $\wp x$. Then the natural embedding of $s$ and $h$ is an embedding of $\Natural$ and the set of elements of $s$ defined as the natural embedding of the set of elements of $s$.

the finite exhaustion of hs (from the name)

Assume that $s$ is countable. Then the finite exhaustion of $\mathrm{hs}$ is a finite exhaustion of $s$.

finite exhaustion of s (from the name)

Let $s$ be an element of $\wp x$. Then the finite exhaustions of $s$ are a basic type.

the product of K and #2 (from the name)

Let $K$ be a finite exhaustion of $s$. Let $\mathrm{K'}$ be a finite exhaustion of $t$. Then the product of $K$ and $\mathrm{K'}$ is a finite exhaustion of $\operatorname{sprod}$ applied to $s$ and $t$.

the finite exhaustion of self and x1 (from the name)

Let $\mathrm{self}$ be a finite exhaustion of $s$. Let $x_{1}$ be a natural number. Then the finite exhaustion of $\mathrm{self}$ and $x_{1}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{invFunOn}$ applied to $f$, $s$ and $b$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $a$ of $x$, such that $a$ is an element of $s$ and $\EqtMACRoH {f (a)}{b}$, the function that maps $h_{1}$ to $\operatorname{choose}$ applied to $h_{1}$ and the function that maps $h_{2}$ to $\operatorname{choice}$ applied to $h$.

set of x (from the name)

Let $x$ be a set. Then a set of $x$ is an element of the function that maps $x$ to $\wp x$.

Let $s$ be a set of $x$. Then $\operatorname{run}$ applied to $s$ is an element of $\wp x$ defined as $s$.

the inclusion of h and x1 (from the name)

Assume that $s \leq t$. Let $x_{1}$ be an element of $s$. Then the inclusion of $h$ and $x_{1}$ is an element of $t$ defined as $x_{1}$.

Assume that $x_{2}$ is not an element of $t$. Then $\operatorname{subtypeInsertEquivOption}$ applied to $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {i}{(\MembershipmemMACRoT {\operatorname{insert} (x_{2} , t)}{i})})}{\mathrm{Option} (\SubtypeSet {i_{1}}{(\MembershipmemMACRoT {t}{i_{1}})})}$.

$\operatorname{sUnionPowersetGI}$ is a Galois insertion of the function that maps $x_{1}$ to the union of $x_{1}$ and the function that maps $x_{2}$ to the powerset of $x_{2}$ defined as $\mathrm{giSSupIic}$.

the sigma equivalence of s and hs (from the name)

Let $s$ be a function from elements of $x$ to elements of $\wp x_{1}$ such that for all elements $b$ of $x_{1}$, $\mathrm{ExistsUnique}$ holds for the function that maps $i_{1}$ to $\MembershipmemMACRoT {s (i_{1})}{b}$. Then the sigma equivalence of $s$ and $\mathrm{hs}$ is an equivalence from $\Sigma$ applied to the function that maps $i$ to the set of elements of $s$ applied to $i$ to $x_{1}$.

Let $t$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to the set of elements of $t$ applied to $i_{1}$. Then $\operatorname{sigmaToiUnion}$ applied to $t$ and $x_{2}$ is an element of the union of the function that maps $i$ to $t$ applied to $i$ defined as $\operatorname{snd}$ applied to $x_{2}$.

Assume that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $t$ is pairwise. Then $\operatorname{unionEqSigmaOfDisjoint}$ applied to $h$ is an equivalence from the set of elements of the union of the function that maps $i$ to $t$ applied to $i$ to $\Sigma$ applied to the function that maps $i_{1}$ to the set of elements of $t$ applied to $i_{1}$ defined as the inverse of the equivalence of $\operatorname{sigmaToiUnion}$ applied to $t$ and $\mathrm{Set\_\_sigmaToiUnion\_bijective}$ applied to $t$ and $h$.

the membership partition of f and x1 (from the name)

Let $f$ be a function from natural numbers to elements of $\wp x$. Let $x_{1}$ be a natural number. Then the membership partition of $f$ and $x_{1}$ is an element of $\wp (\wp x)$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{memPartition\_\_\_f}$ applied to $f$.

the set in f (from the docstring)

Let $f$ be a function from natural numbers to elements of $\wp x$. Let $x_{1}$ be a natural number. Let $x_{2}$ be an element of $x$. Then the set in $f$ is an element of $\wp x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{memPartitionSet\_\_\_f}$ applied to $f$ and $x_{2}$.

Let $s$ and $t$ be elements of $\wp x$. Let $a$ be an element of $x$. Then $\operatorname{antidiagonal}$ applied to $s$, $t$ and $a$ is an element of $\wp \mathrm{Prod} (x , x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $\ProdfstMACRoZ {x_{2}}$ is an element of $s$, $\ProdsndMACRoAA {x_{2}}$ is an element of $t$ and $\EqtMACRoH {\ProdfstMACRoZ {x_{2}}+ \ProdsndMACRoAA {x_{2}}}{a}$.

Let $s$ and $t$ be elements of $\wp x$. Let $a$ be an element of $x$. Then $\operatorname{mulAntidiagonal}$ applied to $s$, $t$ and $a$ is an element of $\wp \mathrm{Prod} (x , x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $\ProdfstMACRoZ {x_{2}}$ is an element of $s$, $\ProdsndMACRoAA {x_{2}}$ is an element of $t$ and $\EqtMACRoH {\ProdfstMACRoZ {x_{2}}\times \ProdsndMACRoAA {x_{2}}}{a}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{BijOn}$ holds for $f$, $s$ and $t$, if $\operatorname{MapsTo}$ holds for $f$, $s$ and $t$, $f$ is injective on $s$ and $\operatorname{SurjOn}$ holds for $f$, $s$ and $t$.

Let $x_{2}$ and $x_{3}$ be functions from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{EqOn}$ holds for $x_{2}$, $x_{3}$ and $s$, if for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $s$, then $\EqtMACRoH {x_{2} (x_{4})}{x_{3} (x_{4})}$.

f is injective on s (by hand)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $f$ is injective on $s$, if for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of $s$, then for all elements $x_{3}$ of $x$, if $x_{3}$ is an element of $s$, then if $\EqtMACRoH {f (x_{2})}{f (x_{3})}$, then $\EqtMACRoH {x_{2}}{x_{3}}$.

Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{InvOn}$ holds for $g$, $f$, $s$ and $t$, if $\operatorname{LeftInvOn}$ holds for $g$, $f$ and $s$ and $\operatorname{RightInvOn}$ holds for $g$, $f$ and $t$.

Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{LeftInvOn}$ holds for $g$, $f$ and $s$, if for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of $s$, then $\EqtMACRoH {g (f (x_{2}))}{x_{2}}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{MapsTo}$ holds for $f$, $s$ and $t$, if for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of $s$, then $\MembershipmemMACRoT {t}{f (x_{2})}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$ such that $\operatorname{MapsTo}$ holds for $f$, $s$ and $t$. Let $x_{2}$ be an element of $s$. Then $\operatorname{restrict}$ applied to $f$, $s$, $t$, $h$ and $x_{2}$ is an element of $t$ defined as the map of $f$ and $x_{2}$.

Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{RightInvOn}$ holds for $g$, $f$ and $t$, if $\operatorname{LeftInvOn}$ holds for $f$, $g$ and $t$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{SurjOn}$ holds for $f$, $s$ and $t$, if $t$ is less than or equal to the image of $f$ and $s$.

the diagonal of x (from the name)

Let $x$ be a set. Then the diagonal of $x$ is an element of $\wp \mathrm{Prod} (x , x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\EqtMACRoH {\ProdfstMACRoZ {p}}{\ProdsndMACRoAA {p}}$.

the graph of f and s (from the docstring)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then the graph of $f$ and $s$ is an element of $\wp \mathrm{Prod} (x , x_{1})$ defined as the image of the function that maps $x_{2}$ to $\ProdmkMACRoU {x_{2}}{f (x_{2})}$ and $s$.

the image of s and t (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then the image of $s$ and $t$ is an element of $\wp x_{2}$ defined as $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that there exists an element $a$ of $x$, such that $a$ is an element of $s$ and there exists an element $b$ of $x_{1}$ such that $b$ is an element of $t$ and $\EqtMACRoH {f (a , b)}{c}$.

the image factorization of s and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $s$. Then the image factorization of $s$ and $x_{2}$ is an element of the image of $f$ and $s$ defined as $f$ applied to $x_{2}$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{kernImage}$ applied to $f$ and $s$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that for all elements $x_{2}$ of $x$, if $\EqtMACRoH {f (x_{2})}{y}$, then $x_{2}$ is an element of $s$.

Let $s$ be an element of $\wp x$. Then $\operatorname{offDiag}$ applied to $s$ is an element of $\wp \mathrm{Prod} (x , x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $\ProdfstMACRoZ {x_{1}}$ is an element of $s$, $\ProdsndMACRoAA {x_{1}}$ is an element of $s$ and $\ProdfstMACRoZ {x_{1}}\neq \ProdsndMACRoAA {x_{1}}$.

the product of s and t (from the name)

Let $s$ be an element of $\wp x$. Let $t$ be a function from elements $i_{1}$ of $x$ to elements of $\wp x_{1} (i_{1})$. Then the product of $s$ and $i_{1}$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i))$ defined as the function that maps $t$ to $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that for all elements $i$ of $x$, if $i$ is an element of $s$, then $\MembershipmemMACRoT {i_{1} (i)}{f (i)}$ and $t$.

the preimage of f and s (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then the preimage of $f$ and $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{f (x_{2})}$.

the Cartesian product of s and t (from the docstring)

Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then the Cartesian product of $s$ and $t$ is an element of $\wp \mathrm{Prod} (x , x_{1})$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that $\ProdfstMACRoZ {p}$ is an element of $s$ and $\ProdsndMACRoAA {p}$ is an element of $t$.

the range of f (from the name)

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the range of $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that there exists an element $y$ of $x_{1}$, such that $\EqtMACRoH {f (y)}{x_{2}}$.

the range factorization of f and x2 (from the name)

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $x_{2}$ be an element of $x_{1}$. Then the range factorization of $f$ and $x_{2}$ is an element of the range of $f$ defined as $f$ applied to $x_{2}$.

the range splitting of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of the range of $f$. Then the range splitting of $f$ and $x_{2}$ is an element of $x$.

Let $t$ be an element of $\wp x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of the preimage of $f$ and $t$. Then $\operatorname{restrictPreimage}$ applied to $t$, $f$ and $x_{2}$ is an element of $t$ defined as $\operatorname{restrict}$ applied to $f$, the preimage of $f$ and $t$, $t$, $\mathrm{Set\_\_mapsTo\_preimage}$ applied to $f$ and $t$ and $x_{2}$.

the sequence of s and t (from the name)

Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1})$. Let $t$ be an element of $\wp x$. Then the sequence of $s$ and $t$ is an element of $\wp x_{1}$ defined as the image of $s$ and $t$.

the opposite of s (from the docstring)

Let $s$ be an element of $\wp x$. Then the opposite of $s$ is an element of the power set of the set of opposites of $x$ defined as the preimage of $\operatorname{unop}$ and $s$.

the opposite equivalence (from the name)

The opposite equivalence is an equivalence from $\wp x$ to the power set of the set of opposites of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$, $\operatorname{unop}$, $\mathrm{Set\_\_op\_unop}$ and $\mathrm{Set\_\_unop\_op}$.

the opposite equivalence self of s (from the name)

Let $s$ be an element of $\wp x$. Then the opposite equivalence self of $s$ is an equivalence from the set of elements of the opposite of $s$ to the set of elements of $s$.

the opposite of s (from the name)

Let $s$ be an element of the power set of the set of opposites of $x$. Then the opposite of $s$ is an element of $\wp x$ defined as the preimage of $\operatorname{op}$ and $s$.

s is a pairwise disjoint with respect to f (from the name)

Let $s$ be an element of $\wp x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then $s$ is a pairwise disjoint with respect to $f$, if $\operatorname{Pairwise}$ holds for $s$ and $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $f$.

Assume that $s$ is a pairwise disjoint with respect to $f$. Then $\operatorname{biUnionEqSigmaOfDisjoint}$ applied to $h$ is an equivalence from the set of elements of the union of the function that maps $i$ to the union of the function that maps $h_{1}$ to $f$ applied to $i$ to $\Sigma$ applied to the function that maps $i_{1}$ to the set of elements of $f$ applied to $i_{1}$.

the powerset cardinality of x and n (from the name)

Let $x$ be a set. Let $n$ be a natural number. Then the powerset cardinality of $x$ and $n$ is an element of the power set of the set of finite sets of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to $\mathrm{Eq} (\FinsetcardMACRoM {s}, n)$.

the complement of hm (from the name)

Assume that $m + n$ is equal to the cardinality of $x$. Then the complement of $\mathrm{hm}$ is an equivalence from the set of elements of the powerset cardinality of $x$ and $n$ to the set of elements of the powerset cardinality of $x$ and $m$.

Assume that $s$ is disjoint to $t$. Then $\operatorname{disjUnion}$ applied to $\mathrm{hst}$ is an element of the powerset cardinality of $x$ and $m + n$ defined as $\operatorname{disjUnion}$ applied to $s$, $t$ and $\mathrm{hst}$.

the map of f and s (from the name)

Let $n$ be a natural number. Let $f$ be an embedding of $x$ and $x_{1}$. Let $s$ be an element of the powerset cardinality of $x$ and $n$. Then the map of $f$ and $s$ is an element of the powerset cardinality of $x_{1}$ and $n$ defined as the map of $f$ and $s$.

the powerset cardinality of s_card (from the name)

Assume that $\FinsetcardMACRoM {s}= n$. Then the powerset cardinality of $\mathrm{s\_card}$ is an element of the powerset cardinality of $x$ and $n$ defined as $s$.

the powerset cardinality of n and f (from the name)

Let $n$ be a natural number. Let $x$ be a set. Let $f$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $x$. Then the powerset cardinality of $n$ and $f$ is an element of the powerset cardinality of $x$ and $n$ defined as the map of $f$ and the universal set.

the powerset cardinality (from the name)

The powerset cardinality is an equivalence from $x$ to the set of elements of the powerset cardinality of $x$ and $1$.

the product equivalence (from the name)

The product equivalence is an equivalence from $\Sigma$ applied to the function that maps $n$ to the set of elements of the powerset cardinality of $x$ and $n$ to the set of finite sets of $x$.

pullback of f and g (from the name)

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $g$ be a function from elements of $Z$ to elements of $Y$. Then a pullback of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\SubtypeSet {p}{(\EqtMACRoH {f (\ProdfstMACRoZ {p})}{g (\ProdsndMACRoAA {p})})}$.

the projection from the fiber product to the first factor of p (from the docstring)

Let $p$ be a pullback of $f$ and $g$. Then the projection from the fiber product to the first factor of $p$ is an element of $X$ defined as $\ProdfstMACRoZ {p}$.

the projection from the fiber product to the second factor of p (from the docstring)

Let $p$ be a pullback of $f$ and $g$. Then the projection from the fiber product to the second factor of $p$ is an element of $Z$ defined as $\ProdsndMACRoAA {p}$.

pullback self of f (from the name)

Let $f$ be a function from elements of $X$ to elements of $Y$. Then a pullback self of $f$ is an element of the function that maps $f$ to the set of pullbacks of $f$ and $f$.

the map first component of x (from the name)

Let $x$ be a pullback self of $\operatorname{snd}$. Then the map first component of $x$ is a pullback self of $f$ defined as the map pullback of $\operatorname{fst}$ and $x$.

the map second component of x (from the name)

Let $x$ be a pullback self of $\operatorname{fst}$. Then the map second component of $x$ is a pullback self of $g$.

the map pullback of mapZ and p (from the name)

Let $\mathrm{mapX}$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{mapY}$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Let $\mathrm{mapZ}$ be a function from elements of $x_{4}$ to elements of $x_{5}$. Assume that $\EqtMACRoH {\operatorname{comp} (x_{8} , \mathrm{mapX})}{\operatorname{comp} (\mathrm{mapY} , x_{6})}$. Assume that $\EqtMACRoH {\operatorname{comp} (x_{9} , \mathrm{mapZ})}{\operatorname{comp} (\mathrm{mapY} , x_{7})}$. Let $p$ be a pullback of $x_{6}$ and $x_{7}$. Then the map pullback of $\mathrm{mapZ}$ and $p$ is a pullback of $x_{8}$ and $x_{9}$ defined as $\ProdmkMACRoU {\mathrm{mapX} (\operatorname{fst} (p))}{\mathrm{mapZ} (\operatorname{snd} (p))}$.

the pullback diagonal of f (from the name)

Let $f$ be a function from elements of $X$ to elements of $Y$. Then the pullback diagonal of $f$ is an element of the power set of the set of pullbacks of $f$ and $f$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that the projection from the fiber product to the first factor of $p$ is equal to the projection from the fiber product to the second factor of $p$.

the pullback diagonal of f and x (from the name)

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $x$ be an element of $X$. Then the pullback diagonal of $f$ and $x$ is a pullback of $f$ and $f$ defined as $\ProdmkMACRoU {x}{x}$.

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x$ such that for all elements $x_{3}$ of $x_{1}$, $\MembershipmemMACRoT {s}{f (x_{3})}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{codRestrict}$ applied to $f$, $s$, $h$ and $x_{2}$ is an element of $s$ defined as $f$ applied to $x_{2}$.

Let $s$ be an element of $\wp x$. Let $f$ be a function from elements $a_{1}$ of $x$ to elements of $x_{1}$ applied to $a_{1}$. Let $a$ be an element of $s$. Then $\operatorname{domRestrict}$ applied to $s$, $a_{1}$, $f$ and $a$ is an element of $x_{1}$ applied to $a$ defined as the function that maps $a$ to $a_{1}$ applied to $f$ and $a$.

Assume that $s \leq t$. Let $f$ be a function from elements $a_{1}$ of $t$ to elements of $x_{1}$ applied to $a_{1}$. Let $a$ be an element of $s$. Then $\mathrm{Set\_\_domRestrict\_u2082\_}$ applied to $\mathrm{hst}$, $a_{1}$, $f$ and $a$ is an element of $x_{1}$ applied to $a$ defined as the function that maps $a$ to $a_{1}$ applied to $f$ and $a$.

Let $s$ be an element of $\wp G$. Let $t$ be an element of $\wp P$. Let $a$ be an element of $P$. Then $\operatorname{smulAntidiagonal}$ applied to $s$, $t$ and $a$ is an element of $\wp \mathrm{Prod} (G , P)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $\ProdfstMACRoZ {x_{1}}$ is an element of $s$, $\ProdsndMACRoAA {x_{1}}$ is an element of $t$ and $\EqtMACRoH {\HSMulhSMulMACRoAL {\ProdfstMACRoZ {x_{1}}}{\ProdsndMACRoAA {x_{1}}}}{a}$.

Let $s$ be an element of $\wp G$. Let $t$ be an element of $\wp P$. Let $a$ be an element of $P$. Then $\operatorname{vaddAntidiagonal}$ applied to $s$, $t$ and $a$ is an element of $\wp \mathrm{Prod} (G , P)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $\ProdfstMACRoZ {x_{1}}$ is an element of $s$, $\ProdsndMACRoAA {x_{1}}$ is an element of $t$ and the sum of $\ProdfstMACRoZ {x_{1}}$ and $\ProdsndMACRoAA {x_{1}}$ is equal to $a$.

set semiring of x (from the name)

Let $x$ be a set. Then a set semiring of $x$ is an element of the function that maps $x$ to $\wp x$.

the image of f (from the docstring)

Let $f$ be a monoid homomorphism of $x$ and $x_{1}$. Then the image of $f$ is a ring homomorphism of the set of set semirings of $x$ and the set of set semirings of $x_{1}$.

the set semiring (from the name)

The set semiring is an equivalence from $\wp x$ to the set of set semirings of $x$ defined as the identity of $\wp x$.

the singleton monoid homomorphism (from the name)

The singleton monoid homomorphism is a monoid homomorphism of $x$ and the set of set semirings of $x$.

the set (from the name)

The set is an equivalence from the set of set semirings of $x$ to $\wp x$ defined as the identity of the set of set semirings of $x$.

the sigma of s and t (from the name)

Let $s$ be an element of $\wp x$. Let $t$ be a function from elements $i_{1}$ of $x$ to elements of $\wp x_{1} (i_{1})$. Then the sigma of $s$ and $i_{1}$ is an element of $\wp \Sigma (\lambda i . x_{1} (i))$ defined as the function that maps $t$ to $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $\MembershipmemMACRoT {s}{\operatorname{fst} (x_{2})}$ and $\MembershipmemMACRoT {i_{1} (\operatorname{fst} (x_{2}))}{\operatorname{snd} (x_{2})}$ and $t$.

s is nontrivial (from the name)

Let $s$ be an element of $\wp x$. Then $s$ is nontrivial, if there exists an element $x_{1}$ of $x$, such that $x_{1}$ is an element of $s$ and there exists an element $y$ of $x$ such that $y$ is an element of $s$ and $x_{1} \neq y$.

Assume that $s$ is nontrivial. Then $\operatorname{choose}$ applied to $\mathrm{hs}$ is an element of $\mathrm{Prod}$ applied to $x$ and $x$.

s is a subsingleton (from the name)

Let $s$ be an element of $\wp x$. Then $s$ is a subsingleton, if for all elements $x_{1}$ of $x$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $x$, if $y$ is an element of $s$, then $\EqtMACRoH {x_{1}}{y}$.

Let $x$ be a set. Then we can say that $\mathrm{HasInfs}$ holds for $x$.

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{infs}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

Let $x$ be a set. Then we can say that $\mathrm{HasSups}$ holds for $x$.

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{sups}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

the union lift of h and hT (from the name)

Let $S$ be a function from elements of $x_{1}$ to elements of $\wp x$. Let $f$ be a function from elements $i_{1}$ of $x_{1}$ and elements of $S$ applied to $i_{1}$ to elements of $x_{2}$ such that for all elements $i$ and $j$ of $x_{1}$, for all elements $x_{4}$ of $x$, for all elements $\mathrm{hxi}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (i)}{x_{4}}$, for all elements $\mathrm{hxj}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (j)}{x_{4}}$, $\EqtMACRoH {f (i , x_{4})}{f (j , x_{4})}$. Let $T$ be an element of $\wp x$ such that $T$ is less than or equal to the union of $S$. Let $x_{3}$ be an element of $T$. Then the union lift of $h$ and $\mathrm{hT}$ is an element of $x_{2}$.

the lift cover of f and hS (from the name)

Let $S$ be a function from elements of $x_{1}$ to elements of $\wp x$. Let $f$ be a function from elements $i_{1}$ of $x_{1}$ and elements of $S$ applied to $i_{1}$ to elements of $x_{2}$ such that for all elements $i$ and $j$ of $x_{1}$, for all elements $x_{3}$ of $x$, for all elements $\mathrm{hxi}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (i)}{x_{3}}$, for all elements $\mathrm{hxj}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (j)}{x_{3}}$, $\EqtMACRoH {f (i , x_{3})}{f (j , x_{3})}$. Assume that the union of $S$ is equal to the universal set. Let $a$ be an element of $x$. Then the lift cover of $i_{1}$ and $\mathrm{hS}$ is an element of $x_{2}$.

the eliminator of f and a1 (from the name)

Let $f$ be a function from elements $a_{1}$ of $x$ and elements of $x_{1}$ applied to $a_{1}$ to elements of $x_{2}$. Let $a$ be an element of $\mathrm{PSigma}$ applied to $x_{1}$. Then the eliminator of $a_{1}$ and $f$ is an element of $x_{2}$.

the map of x5 and a (from the name)

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be a function from elements $a$ of $x$ and elements of $x_{2}$ applied to $a$ to elements of $x_{3}$ applied to $x_{4}$ applied to $a$. Let $x_{6}$ be an element of $\mathrm{PSigma}$ applied to $x_{2}$. Then the map of $a$ and $x_{5}$ is an element of $\mathrm{PSigma}$ applied to $x_{3}$.

the sigma of p (from the name)

Let $p$ be an element of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the sigma of $p$ is an element of $\Sigma$ applied to the function that maps $x_{2}$ to $x_{1}$ defined as $\operatorname{mk}$ applied to $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

the curry of x4 and x3 (from the name)

Let $f$ be a function from elements $x_{4}$ of $\Sigma$ applied to $x_{1}$ to elements of $x_{2}$ applied to $\operatorname{fst}$ applied to $x_{4}$ and $\operatorname{snd}$ applied to $x_{4}$. Let $x_{3}$ be an element of $x$. Let $y$ be an element of $x_{1}$ applied to $x_{3}$. Then the curry of $f$ and $x_{3}$ is an element of $x_{2}$ applied to $x_{3}$ and $y$ defined as the function that maps $y$ to $x_{4}$ applied to $\operatorname{mk}$ applied to $f$ and $x_{3}$ and $y$.

the map of x5 and a (from the name)

Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be a function from elements $a$ of $x$ and elements of $x_{2}$ applied to $a$ to elements of $x_{3}$ applied to $x_{4}$ applied to $a$. Let $x_{6}$ be an element of $\Sigma$ applied to $x_{2}$. Then the map of $a$ and $x_{5}$ is an element of $\Sigma$ applied to $x_{3}$ defined as the function that maps $x_{6}$ to $\operatorname{mk}$ applied to $x_{4}$ applied to $\operatorname{fst}$ applied to $x_{5}$, $a$ applied to $\operatorname{fst}$ applied to $x_{5}$ and $\operatorname{snd}$ applied to $x_{5}$ and $x_{6}$.

Let $f$ be a function from elements $x_{4}$ of $x$ and elements $y$ of $x_{1}$ applied to $x_{4}$ to elements of $x_{2}$ applied to $x_{4}$ and $y$. Let $x_{3}$ be an element of $\Sigma$ applied to $x_{1}$. Then $\operatorname{uncurry}$ applied to $x_{4}$, $y$, $f$ and $x_{3}$ is an element of $x_{2}$ applied to $\operatorname{fst}$ applied to $x_{3}$ and $\operatorname{snd}$ applied to $x_{3}$ defined as the function that maps $f$ and $x_{3}$ to $x_{4}$ applied to $\operatorname{fst}$ applied to $y$, $\operatorname{snd}$ applied to $y$, $f$ and $x_{3}$.

Let $x$ be a set. Then an element of $\mathrm{Stream'}$ applied to $x$ is an element of the function that maps $x$ to the set of functions from natural numbers to elements of $x$.

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\operatorname{All}$ holds for $p$ and $s$, if for all natural numbers $n$, $p$ holds for $\operatorname{get}$ applied to $s$ and $n$.

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\operatorname{Any}$ holds for $p$ and $s$, if there exists a natural number $n$, such that $p$ holds for $\operatorname{get}$ applied to $s$ and $n$.

Let $x_{1}$ be a list of elements of $x$. Let $x_{2}$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x$. Proof. Let $x_{1}$ be arbitrary. Let $x_{2}$ be arbitrary. By x1. By Stream'__appendStream'___f. By x2. By List__brecOn.

Let $f$ be an element of $\mathrm{Stream'}$ applied to the set of functions from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $f$ be arbitrary. Let $s$ be arbitrary. Let $n$ be arbitrary. By f. By n. By s. By n. By Stream'__get. By Stream'__get.

Let $a$ be an element of $x$. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x$.

the constant of a (from the name)

Let $a$ be an element of $x$. Then the constant of $a$ is an element of $\mathrm{Stream'}$ applied to $x$ defined as the function that maps $x_{1}$ to $a$.

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $f$ be arbitrary. Let $g$ be arbitrary. Let $x_{2}$ be arbitrary. By f. By g. By x2. By Stream'__iterate. By Stream'__map.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Prod}$ applied to $x_{1}$ and $x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $f$ be arbitrary. Let $x_{2}$ be arbitrary. By Prod__fst. By f. By Function__comp. By Prod__snd. By f. By Function__comp. By x2. By Stream'__corec.

Let $a$ be an element of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $a$ be arbitrary. Let $f$ be arbitrary. Let $g$ be arbitrary. By f. By g. By a. By Stream'__corec.

Let $\mathrm{cmd}$ be an element of $\mathrm{StateM}$ applied to $x$ and $x_{1}$. Let $s$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $\mathrm{cmd}$ be arbitrary. Let $s$ be arbitrary. By Prod__fst. By cmd. By StateT__run. By Prod__snd. By Function__comp. By cmd. By s. By StateT__run. By Stream'__corec.

the cycle of l and h (from the name)

Let $l$ be a list of elements of $x$ such that $l \neq \operatorname{nil}$. Then the cycle of $l$ and $h$ is an element of $\mathrm{Stream'}$ applied to $x$.

Let $n$ be a natural number. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x$. Proof. Let $n$ be arbitrary. Let $s$ be arbitrary. Let $i$ be arbitrary. By s. By i. By n. By plus. By Stream'__get.

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $\mathrm{Prod}$ applied to $\Natural$ and $x$. Proof. Let $s$ be arbitrary. Let $n$ be arbitrary. By n. By s. By n. By Stream'__get. By Prod__mk.

the even of s (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the even of $s$ is an element of $\mathrm{Stream'}$ applied to $x$ defined as $\operatorname{corec}$ applied to $\operatorname{head}$, the function that maps $s_{1}$ to the tail of the tail of $s_{1}$ and $s$.

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Let $n$ be a natural number. Then $\operatorname{get}$ applied to $s$ and $n$ is an element of $x$ defined as $s$ applied to $n$.

the head of s (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the head of $s$ is an element of $x$ defined as $\operatorname{get}$ applied to $s$ and $0$.

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for the set of lists of elements of $x$. Proof. Let $s$ be arbitrary. By s. By Stream'__head. By List__nil. By List__cons. By s. By Stream'__tail. By Stream'__initsCore.

Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x$.

Let $f$ be a function from elements of $x$ to elements of $x$. Let $a$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x$. Proof. Let $f$ be arbitrary. Let $a$ be arbitrary. Let $x_{1}$ be arbitrary. By x1. By f. By a. By Stream'__iterate___f. By Nat__brecOn.

the map of f and s (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the map of $f$ and $s$ is an element of $\mathrm{Stream'}$ applied to $x_{1}$ defined as the function that maps $n$ to $f$ applied to $\operatorname{get}$ applied to $s$ and $n$.

$\mathrm{Stream'}$ holds for $\Natural$. Proof. Let $n$ be arbitrary. By n.

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\mathrm{Stream'}$ holds for $x$. Proof. Let $s$ be arbitrary. By s. By Stream'__tail. By Stream'__even.

Let $a$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x$. Proof. Let $a$ be arbitrary. By a. By Stream'__const.

the tail of s (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the tail of $s$ is an element of $\mathrm{Stream'}$ applied to $x$ defined as the function that maps $i$ to $\operatorname{get}$ applied to $s$ and $i + 1$.

the tail of s (from the name)

Let $s$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the tail of $s$ is an element of $\mathrm{Stream'}$ applied to $\mathrm{Stream'}$ applied to $x$ defined as $\operatorname{corec}$ applied to $\mathrm{id}$, $\operatorname{tail}$ and the tail of $s$.

Let $x_{1}$ be a natural number. Let $x_{2}$ be an element of $\mathrm{Stream'}$ applied to $x$. Then $\operatorname{take}$ applied to $x_{1}$ and $x_{2}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Stream'\_\_take\_\_\_f}$ and $x_{2}$.

Let $g$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x$. Let $a$ be an element of $x$. Then $\mathrm{Stream'}$ holds for $x_{1}$. Proof. Let $g$ be arbitrary. Let $f$ be arbitrary. Let $a$ be arbitrary. By g. By f. By a. By Stream'__corec.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Stream'}$ applied to $x$. Let $x_{4}$ be an element of $\mathrm{Stream'}$ applied to $x_{1}$. Then $\mathrm{Stream'}$ holds for $x_{2}$. Proof. Let $f$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $n$ be arbitrary. By x3. By n. By Stream'__get. By x4. By n. By Stream'__get. By f.

Let $R$ be a function from elements of $\mathrm{Stream'}$ applied to $x$ and elements of $\mathrm{Stream'}$ applied to $x$ to propositions. Then $\operatorname{IsBisimulation}$ holds for $R$, if for all elements $x_{1}$ and $x_{2}$ of $\mathrm{Stream'}$ applied to $x$, if $R$ holds for $x_{1}$ and $x_{2}$, then the head of $x_{1}$ is equal to the head of $x_{2}$ and $R$ holds for the tail of $x_{1}$ and the tail of $x_{2}$.

Let $x$ and $x_{1}$ be elements of $\operatorname{Iterator}$. Then $\operatorname{ltb}$ applied to $x$ and $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\mathrm{String\_\_ltb\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $x$ and $x_{1}$.

Let $x$ and $x_{1}$ be elements of $\operatorname{Iterator}$. Let $\mathrm{ind}$ be a function from elements $x_{16}$ of $\mathrm{String}$ and elements $x_{17}$ of $\mathrm{String}$ and elements $x_{18}$ of $\operatorname{Raw}$ and elements $x_{19}$ of $\operatorname{Raw}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{17} , x_{19}))}{\operatorname{true}}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{16} , x_{18}))}{\operatorname{true}}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{get} (x_{16} , x_{18})}{\operatorname{get} (x_{17} , x_{19})}$ and elements of $\mathrm{motive}$ applied to $\operatorname{next}$ applied to $\operatorname{mk}$ applied to $x_{16}$ and $x_{18}$ and $\operatorname{next}$ applied to $\operatorname{mk}$ applied to $x_{17}$ and $x_{19}$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $x_{16}$ and $x_{18}$ and $\operatorname{mk}$ applied to $x_{17}$ and $x_{19}$. Let $\mathrm{eq}$ be a function from elements $x_{12}$ of $\mathrm{String}$ and elements $x_{13}$ of $\mathrm{String}$ and elements $x_{14}$ of $\operatorname{Raw}$ and elements $x_{15}$ of $\operatorname{Raw}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{13} , x_{15}))}{\operatorname{true}}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{12} , x_{14}))}{\operatorname{true}}$ and elements of $\mathrm{Proof}$ applied to the proposition that it is not the case that $\EqtMACRoH {\operatorname{get} (x_{12} , x_{14})}{\operatorname{get} (x_{13} , x_{15})}$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $x_{12}$ and $x_{14}$ and $\operatorname{mk}$ applied to $x_{13}$ and $x_{15}$. Let $x_{2}$ be a function from elements $x_{8}$ of $\mathrm{String}$ and elements $x_{9}$ of $\mathrm{String}$ and elements $x_{10}$ of $\operatorname{Raw}$ and elements $x_{11}$ of $\operatorname{Raw}$ and elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{9} , x_{11}))}{\operatorname{true}}$ and elements of $\mathrm{Proof}$ applied to the proposition that it is not the case that $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{8} , x_{10}))}{\operatorname{true}}$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $x_{8}$ and $x_{10}$ and $\operatorname{mk}$ applied to $x_{9}$ and $x_{11}$. Let $x_{3}$ be a function from elements $x_{4}$ of $\mathrm{String}$ and elements $x_{5}$ of $\mathrm{String}$ and elements $x_{6}$ of $\operatorname{Raw}$ and elements $x_{7}$ of $\operatorname{Raw}$ and elements of $\mathrm{Proof}$ applied to the proposition that it is not the case that $\EqtMACRoH {\operatorname{hasNext} (\operatorname{mk} (x_{5} , x_{7}))}{\operatorname{true}}$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $x_{4}$ and $x_{6}$ and $\operatorname{mk}$ applied to $x_{5}$ and $x_{7}$. Then $\operatorname{inductionOn}$ applied to $x$, $x_{1}$, $x_{16}$, $x_{17}$, $x_{18}$, $x_{19}$, $\mathrm{ind}$, $x_{12}$, $x_{13}$, $x_{14}$, $x_{15}$, $\mathrm{eq}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{2}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{3}$ is an element of $\mathrm{motive}$ applied to $x$ and $x_{1}$ defined as the function that maps $\mathrm{ind}$, $x_{12}$, $x_{13}$, $x_{14}$, $x_{15}$, $\mathrm{eq}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{2}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{3}$ to $\mathrm{String\_\_ltb\_\_inductionOn\_\_\_unary}$ applied to $x_{16}$, $x_{17}$, $x_{18}$, $x_{19}$, $\operatorname{mk}$ applied to $x$ and $x_{1}$, $\mathrm{ind}$, $x_{12}$, $x_{13}$, $x_{14}$, $x_{15}$, $\mathrm{eq}$, $x_{8}$, $x_{9}$, $x_{10}$, $x_{11}$, $x_{2}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{3}$.

Let $c$ be an element of $\mathrm{Char}$. Then $\operatorname{isAscii}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{decide}$ applied to $\mathrm{Lt} (\operatorname{toNat} (c), 128)$.

Let $x$ and $x_{1}$ be elements of $\mathrm{String}$. Then we can say that $\operatorname{IsPrefix}$ holds for $x$ and $x_{1}$.

Let $x$ and $x_{1}$ be elements of $\mathrm{String}$. Then we can say that $\operatorname{IsSuffix}$ holds for $x$ and $x_{1}$.

the head of s (from the name)

Let $s$ be an element of $\mathrm{String}$. Then the head of $s$ is an element of $\mathrm{Char}$ defined as $\operatorname{front}$ applied to $s$.

Let $n$ be a natural number. Let $c$ be an element of $\mathrm{optParam}$ applied to $\mathrm{Char}$ and $\operatorname{ofNat}$ applied to $32$. Let $s$ be an element of $\mathrm{String}$. Then $\operatorname{leftpad}$ applied to $n$, $c$ and $s$ is an element of $\mathrm{String}$ defined as $\operatorname{ofList}$ applied to $\operatorname{leftpad}$ applied to $n$, $c$ and $\operatorname{toList}$ applied to $s$.

Let $c$ be an element of $\mathrm{Char}$. Let $f$ be a function from elements of $\mathrm{String}$ to elements of $\mathrm{String}$. Let $x$ be an element of $\mathrm{String}$. Then $\operatorname{mapTokens}$ applied to $c$, $f$ and $x$ is an element of $\mathrm{String}$ defined as $\operatorname{comp}$ applied to $\operatorname{intercalate}$ applied to $\operatorname{singleton}$ applied to $c$, $\operatorname{comp}$ applied to $\operatorname{map}$ applied to $f$ and the function that maps $x$ to $\operatorname{splitToList}$ applied to $x$ and the function that maps $x_{1}$ to $\operatorname{decide}$ applied to $\EqtMACRoH {x_{1}}{c}$ and $x$.

Let $n$ be a natural number. Let $c$ be an element of $\mathrm{Char}$. Then $\operatorname{replicate}$ applied to $n$ and $c$ is an element of $\mathrm{String}$ defined as $\operatorname{ofList}$ applied to $\operatorname{replicate}$ applied to $n$ and $c$.

Let $n$ be a natural number. Let $c$ be an element of $\mathrm{optParam}$ applied to $\mathrm{Char}$ and $\operatorname{ofNat}$ applied to $32$. Let $s$ be an element of $\mathrm{String}$. Then $\operatorname{rightpad}$ applied to $n$, $c$ and $s$ is an element of $\mathrm{String}$ defined as $\operatorname{hAppend}$ applied to $s$ and $\operatorname{replicate}$ applied to $n - \operatorname{length} (s)$ and $c$.

the coinduction of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ of $x$, $p$ holds for $f$ applied to $a$. Let $x_{2}$ be an element of $x$. Then the coinduction of $f$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{p (x_{3})}$ defined as $f$ applied to $x_{2}$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ of $x$, if $p$ holds for $a$, then $q$ holds for $f$ applied to $a$. Let $x_{2}$ be an element of $\SubtypeSet {x_{4}}{p (x_{4})}$. Then the map of $f$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{q (x_{3})}$ defined as $f$ applied to $x_{2}$.

Let $p$ be a function from elements of $x$ to propositions. Let $f$ be a function from elements $x_{4}$ of $x$ to elements of $x_{1}$ applied to $x_{4}$. Let $x_{2}$ be an element of $\SubtypeSet {x_{3}}{p (x_{3})}$. Then $\operatorname{restrict}$ applied to $p$, $x_{4}$, $f$ and $x_{2}$ is an element of $x_{1}$ applied to $x_{2}$ defined as the function that maps $x_{2}$ to $x_{4}$ applied to $f$ and $x_{2}$.