\section{Implementation in Agda}

\begin{frame}[t, fragile]{Goals}
  \begin{itemize}[<+->]
    \item Formalize the delay monad categorically and show that it is..
    \begin{itemize}
      \item strong
      \item commutative
    \end{itemize}
    \item Formalize K and show that it is..
    \begin{itemize}
      \item strong
      \item commutative
      \item an equational lifting monad
    \end{itemize}
    \item Take the category of setoids and show that $K$ instantiates to $D_\approx$
  \end{itemize}
\end{frame}

\begin{frame}[t, fragile, blank]{Category Theory in Agda}{Setoid-enriched Categories}
  \begin{minted}{agda}
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    Obj : Set o
    _⇒_ : Obj → Obj → Set ℓ
    _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} 
      → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
  \end{minted}
\end{frame}