\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*{concrete object}

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

\hypertarget{discrete_and_concrete_objects}{}\paragraph*{{Discrete and concrete objects}}\label{discrete_and_concrete_objects}

[[!include discrete and concrete objects - contents]]

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

[[!include category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{concretification_factorization}{Concretification factorization}\dotfill \pageref*{concretification_factorization} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

For $\Gamma : \mathcal{E} \to \mathcal{B}$ a [[functor]] we say that it \emph{has [[codiscrete object]]s} if it has a [[full and faithful functor|full and faithful]] [[right adjoint]] $coDisc : \mathcal{B} \hookrightarrow \mathcal{E}$.

This is for instance the case for the [[global section]] [[geometric morphism]] of a [[local topos]] $(Disc \dashv \Gamma \dashv coDisc) \;\colon\; \mathcal{E} \to \mathcal{B}$.

In this situation, we say that a \textbf{concrete object} $X \in \mathcal{E}$ is one for which the $(\Gamma \dashv coDisc)$-[[unit of an adjunction]] is a [[monomorphism]].

If $\mathcal{E}$ is a [[sheaf topos]], this is called a [[concrete sheaf]].

If $\mathcal{E}$ is a [[cohesive (∞,1)-topos]] then this is called a [[concrete (∞,1)-sheaf]] or the like.

The dual notion is that of a [[co-concrete object]].

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

$\Gamma$ is a [[faithful functor]] on [[morphisms]] whose [[codomain]] is concrete.

\hypertarget{concretification_factorization}{}\subsubsection*{{Concretification factorization}}\label{concretification_factorization}

\begin{prop}
\label{ConcretificationFactorization}\hypertarget{ConcretificationFactorization}{}
For $\mathbf{H}$ a [[local topos]], write

\begin{displaymath}
\mathbf{H}_{conc} 
  \overset{ \phantom{AAAA} }{\hookrightarrow}
  \mathbf{H}
\end{displaymath}
for its [[full subcategory]] of [[concrete objects]].

Then there is a sequence of [[reflective subcategory]]-inclusions that factor the $(\Gamma \dashv coDisc)$-adjunction as

\begin{displaymath}
\Gamma \;\dashv\; coDisc
  \;\;\colon\;\;
  \mathbf{H}
  \itexarray{
    \overset{\phantom{AA} conc \phantom{AA}}{\longrightarrow}
    \\
    \overset{\phantom{AA} \iota_{conc} \phantom{AA}}{\hookleftarrow}
  }
  \mathbf{H}_{conc}
  \itexarray{
    \overset{\phantom{AAA}}{\longrightarrow}
    \\
    \overset{\phantom{AAA}}{\hookleftarrow}
  }
  Set
\end{displaymath}
Here morphisms on top are left adjoint to morphisms below, hence

\begin{displaymath}
conc \dashv \iota_{conc}
\end{displaymath}
exhibits the concrete objects as a [[reflective subcategory]], the reflector $conc$ being ``[[concretification]]''.

\end{prop}
\begin{proof}
For the adjunction on the right, we just need to observe that for every [[set]] $S \in Set$, the [[codiscrete object]] $coDisc(S)$ is [[concrete object|concrete]], which is immediate by [[idempotent monad|idempotency]] of $\sharp$ and the fact that every [[isomorphism]] is also a [[monomorphism]].

For the adjunction on the left we claim that the [[left adjoint]] $conc$ ([[concretification]]), is given by sending each [[object]] to the [[image]] of its $(\Gamma \dashv coDisc)$ [[adjunction unit]] $\eta^\sharp$:

\begin{displaymath}
conc \;\colon\; X \mapsto im(\eta^\sharp_X)
\end{displaymath}
hence to the object which exhibits the [[(epi, mono) factorization system|epi/mono-factorization]] of $\eta^\sharp_X$

\begin{equation}
\eta^\sharp_X
  \;\colon\;
  X 
    \underoverset{epi}{ \eta^{conc}_X }{\longrightarrow}
  conc X
    \underoverset{mono}{}{\longrightarrow}
  \sharp X
  \,.
\label{ConcretificationUnitFromEpiMonoFactorization}\end{equation}
First we need to show that $conc X$, thus defined, is indeed concrete, hence that $\eta^\sharp_{im(\eta^\sharp_X)}$ is a monomorphism. For this, consider the following [[naturality square]] of the $\Gamma \dashv coDisc$-adjunction hom-isomorphism

\begin{equation}
\itexarray{
    Hom_{Set}( \Gamma im(\eta^\sharp_X), \Gamma im(\eta^\sharp_X) )
    &\simeq&
    Hom_{\mathbf{H}}( im(\eta^\sharp_X), \sharp im(\eta^\sharp_X) )
    \\
    {}^{ \mathllap{ (-) \circ \Gamma(\eta^{conc}_X) } }\big\downarrow      
      &&
    \big\downarrow^{
      \mathrlap{ (-) \circ \eta^{conc}_X }
    }
    \\
    Hom_{Set}( \Gamma X, \Gamma im(\eta^\sharp_X) )
    &\simeq&
    Hom_{\mathbf{H}}( X, \sharp im(\eta^\sharp_X) )    
  }
  \phantom{AAAA}
  \itexarray{
    \left\{ id_{\Gamma im(\eta^\sharp_X)} \right\}
      &\longrightarrow&
    \phantom{\sharp(\eta^{conc}_X) \circ \eta^\sharp_{ X }}
    \left\{ \eta^{\sharp}_{im(\eta^\sharp_X)} \right\}
    \\
    \big\downarrow 
      && 
    \phantom{\sharp(\eta^{conc}_X) \circ \eta^\sharp_{ X }}
    \big\downarrow
    \\
    \left\{ \Gamma(\eta^{conc}_X) \right\}
      &\longrightarrow& 
    \left\{
      \underset{
        iso
      }{ 
      \underbrace{
         \sharp(\eta^{conc}_X)
      }}
      \circ \eta^\sharp_{ X }
      \;=\;
    \eta^{\sharp}_{ im(\eta^\sharp_X) } \circ \eta^{conc}_X 
    \right\}
  }
\label{ConcNatur}\end{equation}
By chasing the [[identity morphism]] on $\Gamma im(\eta^\sharp_X)$ through this diagram, as shown by the diagram on the right, we obtain the equality displayed in the bottom right entry, where we used the general formula for [[adjuncts]] and the definition $\sharp \coloneqq coDisc \circ \Gamma$.

But observe that $\Gamma (\eta^{conc}_X)$, and hence also $\sharp(\eta^{conc}_X)$, is an [[isomorphism]], as indicated above: Since $\Gamma$ is both a [[left adjoint]] as well as a [[right adjoint]], it preserves both [[epimorphisms]] as well as [[monomorphisms]], hence it preserves [[image]] factorizations. This implies that $\Gamma \eta^{conc}_X$ is the epimorphism onto the image of $\Gamma( \eta^\sharp_X )$. But by [[idempotent monad|idempotency]] of $\sharp$, the latter is an [[isomorphism]], and hence so is the epimorphism in its image factorization.

Therefore the equality in \eqref{ConcNatur} says that

\begin{displaymath}
\begin{aligned}
    \eta^\sharp_{ X } 
      & =
    \left( 
      iso \circ \eta^{\sharp}_{ im(\eta^\sharp_X)} 
    \right)
      \circ 
    \eta^{conc}_X
    \\
    & =
    mono \circ \eta^{conc}_X 
    \,,
  \end{aligned}
\end{displaymath}
where in the second line we remembered that $\eta^{conc}_X$ is, by definition, the epimorphism in the epi/mono-factorization of $\eta^\sharp_X$.

Now the defining property of epimorphisms allows to cancel this commmon factor on both sides, which yields

\begin{displaymath}
\eta^{\sharp}_{ im(\eta^\sharp_X) }
  \;=\;
  iso \circ mono
  \;=\;
  mono.
\end{displaymath}
This shows that $conc X \coloneqq im(\eta^\sharp_X)$ is indeed concret.

It remains to show that this construction is [[left adjoint]] to the inclusion. We claim that the [[adjunction unit]] of $(conc \dashv \iota_{conc})$ is provided by $\eta^{conc}$ \eqref{ConcretificationUnitFromEpiMonoFactorization}.

To see this, first notice that, since the [[(epi, mono) factorization system|epi/mono-factorization]] is [[orthogonal factorization system|orthogonal]] and hence [[functorial factorization|functorial]], we have [[commuting diagrams]] of the form

\begin{equation}
\itexarray{
    X_1 
      &\underoverset{epi}{\eta^{conc}_{X_1}}{\longrightarrow}& 
    im(\eta^\sharp_{X_1})
      &\underset{mono}{\longrightarrow}&
    \sharp X_1
    \\
    \big\downarrow && \big\downarrow && \big\downarrow
    \\
    X_2 
      &\underoverset{epi}{\eta^{conc}_{X_2}}{\longrightarrow}& 
    im(\eta^\sharp_{X_2})
      &\underset{mono}{\longrightarrow}&
    \sharp X_2
  }
\label{NaturalitySquareForConcretificationUnit}\end{equation}
Now to demonstrate the adjunction, it is sufficient, to show that $\eta^{conc}$ is a [[universal morphism]] in the sense discussed at \emph{[[adjoint functors]]}. Hence consider any morphism $f \;\colon\; X_1 \to X_2$ with $X_2 \in \mathbf{H}_{conc} \hookrightarrow \mathbf{H}$. Then we need to show that there is a unique diagonal morphism as below, that makes the following \emph{top left triangle} [[commuting diagram|commute]]:

\begin{displaymath}
\itexarray{
    X_1 
      &\overset{\phantom{AA} f \phantom{AA}}{\longrightarrow}& 
    X_2
    \\
    {}^{\mathllap{epi}}\big\downarrow^{\mathrlap{\eta^{conc}_{X_1}}} 
      &{}^{\mathllap{\exists !}}\nearrow& 
    \big\downarrow^{\mathrlap{mono}}
    \\
    im(\eta^\sharp_{X_1}) 
      &\underset{}{\longrightarrow}& 
    \sharp X_2
  }
\end{displaymath}
Now, from \eqref{NaturalitySquareForConcretificationUnit}, we have a [[commuting square]] as shown. Here the left morphism is an [[epimorphism]] by construction, while the right morphism is a [[monomorphism]] by assumption on $X_2$. With this, the [[(epi, mono) factorization system|epi/mono-factorization]] says that there is a diagonal [[lift]] which makes \emph{both} triangles [[commuting diagram|commute]].

It remains to see that the lift is unique with just the property of making the top left triangle commute. But this is equivalently the statement that the left morphism is an [[epimorphism]].

\end{proof}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[concretification]]

\end{itemize}
[[!include cohesion - table]]

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

See also

\begin{itemize}%
\item [[Mike Shulman]], \emph{Discreteness, Concreteness, Fibrations, and Scones} (\href{http://golem.ph.utexas.edu/category/2011/11/discreteness_concreteness_fibr.html}{blog post})

\end{itemize}
[[!redirects concrete objects]]



\end{document}