\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{duploid}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability}

[[!include constructivism - contents]]

\hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{duploid}{}\section*{{Duploid}}\label{duploid}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{linear_and_thunkable_morphisms}{Linear and Thunkable Morphisms}\dotfill \pageref*{linear_and_thunkable_morphisms} \linebreak
\noindent\hyperlink{relation_to_adjunctions}{Relation to Adjunctions}\dotfill \pageref*{relation_to_adjunctions} \linebreak
\noindent\hyperlink{a_duploid_from_an_adjunction}{A Duploid from an Adjunction}\dotfill \pageref*{a_duploid_from_an_adjunction} \linebreak
\noindent\hyperlink{adjunction_from_a_duploid}{Adjunction from a Duploid}\dotfill \pageref*{adjunction_from_a_duploid} \linebreak
\noindent\hyperlink{related_concepts}{Related Concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \textbf{duploid} is a [[category]]-like [[structure]] where [[objects]] have a specific [[polarity in type theory|polarity]] and [[composition]] is not necessarily [[associative]].

Duploids are models of [[programming languages]] with [[side effects]] and explicitly polarized [[positive type|positive]] and [[negative type|negative]] [[types]], accomodating both [[call-by-value]] and [[call-by-name]] programming paradigms. Duploids axiomatize the algebraic structure of effectful morphisms, and to a certain extent ``pure'' morphisms (those with no side effects) can be characterized by equational properties as thunkable and linear morphisms. Contrast with [[call-by-push-value]] which directly provides a syntax for the pure morphisms (as values and stacks).

A duploid can be constructed from an [[adjunction]] and the category of duploids is [[reflective subcategory|coreflective]] in the category of adjunctions, equivalent to the [[subcategory]] of adjunctions satisfying an equalizing requirement. The intuition is that a duploid is what is left of an adjunction if we only consider (co)Kleisli morphisms and duploids can be identified with adjunctions whose categories can be recovered from the Kleisli morphisms.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

A \textbf{pre-duploid} $\mathcal{D}$ consists of

\begin{enumerate}%
\item a set $|\mathcal{D}|$ of objects with a polarity map $\varpi : |\mathcal{D}| \to \{+,-\}$. If $\varpi(A) = +$, we say $A$ is positive and otherwise negative.
\item for every pair $A,B \in |\mathcal{D}|$ a set of morphisms $\mathcal{D}(A,B)$.
\item for every compatible pair of morphisms $f \in \mathcal{D}(A,B), g\in \mathcal{D}(B,C)$ a composite $g \odot f \in \mathcal{D}(A,C)$.
\item for every object $A$ an morphism $id_A \in \mathcal{D}(A,A)$ that is the identity with respect to composition.
\item For every $f \in \mathcal{D}(A,B), g \in \mathcal{D}(B,C), h \in \mathcal{D}(C,D)$, an associative law $h \odot (g \odot f) = (h \odot g) \odot f$ when $B$ is negative or $C$ is positive.

\end{enumerate}
Note that when restricted to positive objects or negative objects, composition and identities form a category, written $\mathcal{P}$ and $\mathcal{N}$. When the polarity is known we write positive objects as $P,Q,R$ and negative objects as $L,M,N$. We call composition where the middle object is positive ``positive composition'' or ``by-value composition'' and notate it as $g \bullet f$ and when the middle object is negative we call it ``negative composition'' or ``by-name composition'' and notate it as $g \circ f$. Then the associativity laws can be restated as:

\begin{enumerate}%
\item $\bullet\bullet$: $f \bullet (g \bullet h)  = (f \bullet g) \bullet h$
\item $\circ\circ$: $f \circ (g \circ h)  = (f \circ g) \circ h$
\item $\bullet\circ$: $f \bullet (g \circ h)  = (f \bullet g) \circ h$

\end{enumerate}
and we can see that the only obstacle to associativity is that $f \circ (g \bullet h)$ is not necessarily equal to $(f \circ g) \bullet h$.

A \textbf{duploid} is a pre-duploid $\mathcal{D}$ plus two \textbf{polarity shifts} $\Downarrow : |\mathcal{N}| \to |\mathcal{P}| and \Uparrow : |\mathcal{P}| \to |\mathcal{N}|$, and for each $P \in |\mathcal{P}|, N \in |\mathcal{N}|$, morphisms:

\begin{enumerate}%
\item $delay_P : P \to \Uparrow P$
\item $force_P : \Uparrow P \to P$
\item $wrap_N : N \to \Downarrow N$
\item $unwrap_N : \Downarrow N \to N$

\end{enumerate}
such that

\begin{enumerate}%
\item $\forall f : A \to P, force_P \circ (delay_P \bullet f) = f$
\item $\forall f : N \to A, (f \circ unwrap_N) \bullet wrap_N = f$
\item $delay_P \bullet force_P = id_{\Uparrow P}$
\item $wrap_N \circ unwrap_N = id_{\Downarrow N}$

\end{enumerate}
In light of the definition of linear and thunkable morphisms, these identities are equivalent to saying

\begin{enumerate}%
\item $wrap_N$ is thunkable.
\item $wrap_N, unwrap_N$ is an isomorphism.
\item $force_P$ is linear.
\item $force_P, thunk_P$ is an isomorphism.

\end{enumerate}
\hypertarget{linear_and_thunkable_morphisms}{}\subsection*{{Linear and Thunkable Morphisms}}\label{linear_and_thunkable_morphisms}

Just as thunkable morphisms can be defined in a [[thunk-force category]] and linear morphisms can be defined in a category with a [[runnable monad]], they can be defined in a duploid in a similar way using $delay_P$ in place of the thunk and $unwrap_N$ in place of the run morphism. However, thunkable and linear morphisms can also be defined in a \emph{pre-duploid}, giving a simple characterization just in terms of associativity of composition.

A morphism $f$ is \textbf{thunkable} if for all compatible $g,h$,

\begin{displaymath}
h \odot (g \odot f) = (h \odot g) \odot f.
\end{displaymath}
and a morphism $f$ is \textbf{linear} if for all compatible $g,h$,

\begin{displaymath}
f \odot (g \odot h) = (f \odot g) \odot h.
\end{displaymath}
Observe that all $f : P \to B$ are trivially linear and $g : A \to N$ are trivially thunkable. Further thunkable and linear morphisms form (non-full) subcategories $\mathcal{D}_t, \mathcal{D}_l$.

To understand these concepts, consider the non-trivial situation where $f : A \to P$ is thunkable:

\begin{displaymath}
h \circ (g \bullet f) = (h \circ g) \bullet f.
\end{displaymath}
on the left side, since we have a by-name composition, $h$ is ``evaluated first'', whereas on the right side we have a by-value composition, so $f$ is evaluated first. Thus these two morphisms being equal implies in many semantics $f$ cannot perform any [[side-effect]]. For instance if $f$ prints to the screen and so does $h$, then each composite will print in a different order. Furthermore, if $f$ can manipulate its [[continuation]] explicitly, it has to treat it linearly otherwise $h$ may be evaluated twice or not at all.

In the dual, if $f : N \to B$ and $f$ is linear:

\begin{displaymath}
f \circ (g \bullet h) = (f \circ g) \bullet h
\end{displaymath}
holds and similarly $f$ is evaluated first in the left morphism and $h$ is evaluated first in the right. Then as above it cannot perform any effects and has to treat its \emph{input} linearly, as duplicating or dropping $h$ would make the equation fail to hold.

\hypertarget{relation_to_adjunctions}{}\subsection*{{Relation to Adjunctions}}\label{relation_to_adjunctions}

Briefly, the category of duploids and duploid functors is a [[reflective subcategory]] of the category of adjunctions and morphisms of adjunctions.

\hypertarget{a_duploid_from_an_adjunction}{}\subsubsection*{{A Duploid from an Adjunction}}\label{a_duploid_from_an_adjunction}

First, we construct a duploid from an adjunction, which we think of as a [[forgetful functor]] that only remembers the Kleisli morphisms of the adjunction. To keep the proof unbiased, we start with a [[profunctor]] $O : C_- &#8696; C_+$ that the adjunction [[representable functor|represents]]. This gives us a notion of ``oblique-'' or [[heteromorphism|hetero-]]morphism from a positive object $P \in C_+$ to a negative object $N \in C-$ as $O(P,N)$ and can be used to define the Kleisli and coKleisli categories. In programming applications these are the ``possibly effectful'' morphisms. Then let $F \dashv G$ be adjoint functors representing $O$, i.e. there is a natural equivalence:

\begin{displaymath}
C_+(F P, N) \cong O(P,N) \cong C_-(P, G N).
\end{displaymath}
The pre-duploid $\mathcal{D}$ has as objects $|\mathcal{D}| = |C_+| + |C_-|$ with $\varpi(P) = +, \varpi(N) = -$. The morphisms are defined as:

\begin{displaymath}
\mathcal{D}(A,B) = O(A^+,B^-)
\end{displaymath}
where

\begin{displaymath}
P^+ = P
\end{displaymath}
\begin{displaymath}
N^+ = G N
\end{displaymath}
\begin{displaymath}
P^- = F P
\end{displaymath}
\begin{displaymath}
N^- = N
\end{displaymath}
and identities are given by the identities/unit and counit of the adjunction:

\begin{displaymath}
\id_P : O(P, F P) \equiv C_-(F P,F P)
\end{displaymath}
\begin{displaymath}
\id_N : O(G N, N) \equiv C_+(G N,G N)
\end{displaymath}
To define composition of $f \in \mathcal{D}(A,B), g \in \mathcal{D}(B,C)$, we inspect $B$. If $B = P$ is positive, composition is interpreted as composition in $C_-$, or equivalently in the [[Kleisli category]] of $GF$, using

\begin{displaymath}
f \in O(A^+,F P) \cong C_-(F A^+, F P)
\end{displaymath}
\begin{displaymath}
g \in O(P, C^-) \cong C_-(F P, C^-)
\end{displaymath}
and similarly if $B = N$ is negative, composition is interpreted as composition in $C_+$, or equivalently in the [[Kleisli category]] of $FG$, using

\begin{displaymath}
f \in O(A^+,N) \cong C_+(A^+, G N)
\end{displaymath}
\begin{displaymath}
g \in O(G N, C^-) \cong C_+(G N, G C^-)
\end{displaymath}
This definition makes it clear that the identities are identity and the $\bullet\bullet$ and $\circ\circ$ laws hold from identity and associativity of $C_+,C_-$.

\hypertarget{adjunction_from_a_duploid}{}\subsubsection*{{Adjunction from a Duploid}}\label{adjunction_from_a_duploid}

From a duploid, we can construct the ``cofree'' adjunction: i.e., a right adjoint to the forgetful functor just defined. Intuitively, we want to recover the homomorphisms just from the heteromorphisms. The maximal choice is to consider all thunkable morphisms between positive types and linear morphisms between negative types to be homomorphisms.

Furthermore, this functor is fully faithful, making the category of duploids a [[reflective subcategory]] of adjunctions: they can be identified with exactly those adjunctions in which the unit and counit are mono and epi respectively and in which all thunkable heteromorphisms are the image under $F$ of some homomorphism and vice-versa all linear heteromorphisms are in the image of $G$. This is equivalent to saying that the unit $\eta$ is the [[equalizer]] of $GF\eta$ and $\eta GF$ and dually that the counit $\epsilon$ is the [[coequalizer]] of $FG\epsilon$ and $\epsilon FG$

\hypertarget{related_concepts}{}\subsection*{{Related Concepts}}\label{related_concepts}

\begin{itemize}%
\item [[polarity in type theory]]
\item [[thunk-force category]]
\item [[runnable monad]]

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

Duploids were introduced in chapter II of

\begin{itemize}%
\item Guillaume Munch-Maccagoni, \emph{Syntax and Models of a Non-Associative Composition of Programs and Proofs}, PhD thesis University of Paris Diderot, 2013 \href{https://hal.inria.fr/tel-00918642}{link}

\end{itemize}


\end{document}