Przemebra/praca-magisterska/agda-tex/Kern.tex

\begin{code}
\>[2]\AgdaFunction{Kern$_h$}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[11]\AgdaFunction{Pred}\AgdaSpace{}%
\AgdaFunction{Carrier$_h$}\AgdaSpace{}%
\AgdaBound{ℓ₂}\<%
\\
%
\>[2]\AgdaFunction{Kern$_h$}\AgdaSpace{}%
\AgdaBound{a}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{fn}\AgdaSpace{}%
\AgdaBound{a}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaField{≈$_h$}}\AgdaSpace{}%
\AgdaField{\ensuremath{\epsilon}$_h$}\<%
\end{code}