\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*{geometry of physics -- principal bundles}

\begin{quote}%
This entry contains one chapter of the material at \emph{[[geometry of physics]]}.

previous chapters: \emph{[[geometry of physics -- groups|groups]]}. \emph{[[geometry of physics -- smooth homotopy types|smooth homotopy type]]}

next chapter: \emph{[[geometry of physics -- manifolds and orbifolds|manifolds and orbifold]]}, \emph{[[geometry of physics -- representations and associated bundles|representations and associated bundles]]}


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

\hypertarget{physics}{}\paragraph*{{Physics}}\label{physics}

[[!include physicscontents]]

\hypertarget{differential_geometry}{}\paragraph*{{Differential geometry}}\label{differential_geometry}

[[!include synthetic differential geometry - contents]]

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

\noindent\hyperlink{PrincipalBundles}{\textbf{Principal bundles}}\dotfill \pageref*{PrincipalBundles} \linebreak
\noindent\hyperlink{model_layer}{Model Layer}\dotfill \pageref*{model_layer} \linebreak
\noindent\hyperlink{PrincipalBundlesViaSmoothGroupoids}{Smooth principal bundles via Smooth groupoids}\dotfill \pageref*{PrincipalBundlesViaSmoothGroupoids} \linebreak
\noindent\hyperlink{cech_1cocycles}{Cech 1-cocycles}\dotfill \pageref*{cech_1cocycles} \linebreak
\noindent\hyperlink{the_universal_smooth_principal_bundle}{The universal smooth $G$-principal bundle}\dotfill \pageref*{the_universal_smooth_principal_bundle} \linebreak
\noindent\hyperlink{principal_bundles_2}{$G$-Principal bundles}\dotfill \pageref*{principal_bundles_2} \linebreak
\noindent\hyperlink{fibration_categories_and_the_factorization_lemma}{Fibration categories and the Factorization lemma}\dotfill \pageref*{fibration_categories_and_the_factorization_lemma} \linebreak
\noindent\hyperlink{categories_of_fibrant_objects}{Categories of Fibrant objects}\dotfill \pageref*{categories_of_fibrant_objects} \linebreak
\noindent\hyperlink{factorization_lemma}{Factorization lemma}\dotfill \pageref*{factorization_lemma} \linebreak
\noindent\hyperlink{homotopy_and_homotopy_pullback}{Homotopy and Homotopy pullback}\dotfill \pageref*{homotopy_and_homotopy_pullback} \linebreak
\noindent\hyperlink{WeakyPrincipalSimplicialBundles}{Weakly principal simplicial bundles}\dotfill \pageref*{WeakyPrincipalSimplicialBundles} \linebreak
\noindent\hyperlink{universal_principal_bundle}{Universal principal bundle}\dotfill \pageref*{universal_principal_bundle} \linebreak
\noindent\hyperlink{weakly_principal_simplicial_bundles_2}{Weakly principal simplicial bundles}\dotfill \pageref*{weakly_principal_simplicial_bundles_2} \linebreak
\noindent\hyperlink{semantic_layer}{Semantic Layer}\dotfill \pageref*{semantic_layer} \linebreak
\noindent\hyperlink{principal_bundles_3}{Principal $\infty$-bundles}\dotfill \pageref*{principal_bundles_3} \linebreak
\noindent\hyperlink{syntactic_layer}{Syntactic Layer}\dotfill \pageref*{syntactic_layer} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{PrincipalBundles}{}\subsection*{{\textbf{Principal bundles}}}\label{PrincipalBundles}

\hypertarget{model_layer}{}\subsubsection*{{Model Layer}}\label{model_layer}

\hypertarget{PrincipalBundlesViaSmoothGroupoids}{}\paragraph*{{Smooth principal bundles via Smooth groupoids}}\label{PrincipalBundlesViaSmoothGroupoids}

For $G$ a [[Lie group]], we discuss $G$-[[principal bundles]] over a [[smooth manifold]] $X$ as a natural construction in the context of [[smooth groupoids]].

\hypertarget{cech_1cocycles}{}\paragraph*{{Cech 1-cocycles}}\label{cech_1cocycles}

Recall the discussion of [[Cech cohomology]] in degree 1 from \emph{[[geometry of physics -- smooth homotopy types]] -- \href{geometry%20of%20physics%20--%20smooth%20homotopy%20types#PreSmoothGroupoids}{Pre-smooth groupoids}}

\begin{defn}
\label{BGAsASmoothGroupoid}\hypertarget{BGAsASmoothGroupoid}{}
Let $G$ be a [[Lie group]]. Write $(\mathbf{B}G)_\bullet \in LieGrpd \hookrightarrow PreSmoothGrpd$ for the [[Lie groupoid]]

\begin{displaymath}
(\mathbf{B}G)_\bullet = (G \stackrel{\longrightarrow}{\longrightarrow} \bullet)
\end{displaymath}
with composition induced from the product in $G$.

\end{defn}
A useful schematic picture this groupoid is

\begin{displaymath}
(\mathbf{B}G)_\bullet = 
  \left\{
    \itexarray{
      && \bullet
      \\
      & {}^{\mathllap{g_1}}\nearrow 
      &=& 
      \searrow^{\mathrlap{g_2}}
      \\
      \bullet &&\stackrel{g_2 \cdot g_1 }{\longrightarrow}&& \bullet
    }
  \right\}
\end{displaymath}
where the $g_i \in G$ are elements in the group, and the bottom morphism is labeled by forming the product in the group. (The order of the factors here is a convention whose choice, once and for all, does not matter up to equivalence.)

\begin{remark}
\label{}\hypertarget{}{}
The [[nerve]] of $(\mathbf{B}G)_\bullet$, def. \ref{BGAsASmoothGroupoid}, is a [[simplicial object]] of the form

\begin{displaymath}
N(\mathbf{B}G)_k = G^{\times_k}
\end{displaymath}
with face maps of the form

\begin{displaymath}
N(\mathbf{B}G)_\bullet
 =
 \left(
   \cdots
   G \times G \times G
    \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}}
   G \times G
    \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}
   G \stackrel{\longrightarrow}{\longrightarrow} \bullet
 \right)
\end{displaymath}
where the outer face maps forget the corresponding outer copy in the Cartesian product of groups, and the inner face maps are given by group multiplication in two consecutive copies.

\end{remark}
\begin{defn}
\label{SmoothManifoldAsSmoothGroupoid}\hypertarget{SmoothManifoldAsSmoothGroupoid}{}
For $X$ a [[smooth manifold]], we may regard it as a [[Lie groupoid]] with only identity morphisms. Its schematic depiction is simply

\begin{displaymath}
X = \{x \stackrel{id}{\longrightarrow} x \}
  \,.
\end{displaymath}
\end{defn}
\begin{defn}
\label{CechGroupoidAsSmoothGroupoid}\hypertarget{CechGroupoidAsSmoothGroupoid}{}
Let $\{U_i \to X\}_{i \in I}$ be an [[open cover]] of a [[smooth manifold]] $X$. The corresponding \emph{[[Cech groupoid]]} $C(\{U_i\})_\bullet$ is

\begin{displaymath}
C(\{U_i\})_\bullet
  =
  \left(
    \coprod_{i,j} U_i \underset{X}{\times} U_j
    \stackrel{\overset{p_1}{\longrightarrow}}{\underset{p_2}{\longrightarrow}}
    \coprod_i U_i
  \right)
\end{displaymath}
with the uniquely defined composition. The schematic depiction is

\begin{displaymath}
C(\{U_i\})_\bullet
  = 
  \left\{
    \itexarray{
       && (x,j)
       \\
       & \nearrow &=& \searrow
       \\
      (x,i) && \longrightarrow&& (x,k)
    }
  \right\}
  \,.
\end{displaymath}
\end{defn}
This indicates that the objects of this groupoid are pairs $(x,i)$ consisting of a point $x \in X$ and a patch $U_i \subset X$ that contains $x$, and a morphism is a triple $(x,i,j)$ consisting of a point and \emph{two} patches, that both contain the point, in that $x \in U_i \cap U_j$. The triangle in the above cartoon symbolizes the evident way in which these morphisms compose. All this inherits a smooth structure from the fact that the $U_i$ are smooth manifolds and the inclusions $U_i \to X$ are [[smooth function]]s. hence also $C(U)$ becomes a [[Lie groupoid]].

\begin{remark}
\label{}\hypertarget{}{}
Given an [[open cover]] $\{U_i \to X\}$ there is a canonical morphism from its [[Cech groupoid]] to the manifold $X$ given by

\begin{displaymath}
C(\{U_i\})_\bullet \to X \;\; :\;\; (x,i) \mapsto x
  \,.
\end{displaymath}
\end{remark}
\begin{example}
\label{}\hypertarget{}{}
A morphism

\begin{displaymath}
g : C(\{U_i\})_\bullet \longrightarrow (\mathbf{B}G)_\bullet
\end{displaymath}
is given in components precisely by a collection of functions

\begin{displaymath}
\{g_{i j} : U_{i j} \to G \}_{i,j \in I}
\end{displaymath}
such that on each $U_i \underset{X}{\times} U_k \cap U_j$ the equality $g_{j k} g_{i j}  = g_{i k}$ of [[smooth functions]] holds:

\begin{displaymath}
\left(
    \itexarray{
       && (x,j)
       \\
       & \nearrow && \searrow
       \\
      (x,i) &&\to&& (x,k)
    }
  \right)
  \mapsto
  \left(
    \itexarray{
       && \bullet
       \\
       & {}^{\mathllap{g_{i j}(x)}}\nearrow
       && \searrow^{\mathrlap{g_{j k}(x)}}
       \\
      \bullet &&\stackrel{g_{i k}(x)}{\to}&& \bullet
    }
  \right)
  \,.
\end{displaymath}
This is precisely a [[cocycle]] in [[Cech cohomology]] on $X$ relative $\{U_i\}$ with coefficients in $G$.

\end{example}
\hypertarget{the_universal_smooth_principal_bundle}{}\paragraph*{{The universal smooth $G$-principal bundle}}\label{the_universal_smooth_principal_bundle}

For $G$ a [[Lie group]] (or any [[topological group]]), traditional literature highlights the [[universal principal bundle]] $E G \to B G$ over the [[classifying space]] of $G$, and the fact that under [[pullback]] of [[topological spaces]] this yields all [[isomorphism classes]] of smooth $G$-principal bundles. But an analogous construction exists in [[smooth groupoids]] which is both simpler as well as more powerful: it [[modulating morphism|modulates]] the full groupoid of smooth $G$-[[principal bundles]]. We now discuss this smooth incarnation $(\mathbf{E}G)_\bullet$ of $E G$.

\begin{defn}
\label{EGAsASmoothGroupoid}\hypertarget{EGAsASmoothGroupoid}{}
For $G$ a [[Lie group]], write $\mathbf{E}G$ for the [[action groupoid]] of $G$ acting on itself from the right, hence for the [[Lie groupoid]]

\begin{displaymath}
(\mathbf{E}G)_\bullet
  \coloneqq
  \left(
    G \times G \stackrel{\overset{(-)\cdot (-)}{\longrightarrow}}{\underset{p_1}{\longrightarrow}} G 
  \right)
\end{displaymath}
whose manifold of objects is $G$, whose manifold of morphisms is $G \times G$, whose source-map is projection on the first factor, whose target map is multiplication in the group, whose identity-map is $g\mapsto (g,e)$ and whose composition operation is

\begin{displaymath}
(g_1 g, h) \circ (g_1,g) \coloneqq (g_1, g h)
  \,.
\end{displaymath}
\end{defn}
\begin{remark}
\label{bfEGAsPairGroupoid}\hypertarget{bfEGAsPairGroupoid}{}
The groupoid $(\mathbf{E}G)_\bullet$ of def. \ref{EGAsASmoothGroupoid} has at most one morphism for every ordered pair of objects, hence the morphisms are uniquely identified by giving their source and target.

Schematically:

\begin{displaymath}
(\mathbf{E}G)_\bullet
  = 
  \left\{
     \itexarray{
        && g_2
        \\
        & {}^{\mathllap{g_1^{-1} g_2}}\nearrow &=& \searrow^{\mathrlap{g_2^{-1}g_3 }}
        \\
        g_1 &&\stackrel{ g_1^{-1}g_3}{\longrightarrow}&& g_3
     }
  \right\}
\end{displaymath}
or simply

\begin{displaymath}
(\mathbf{E}G)_\bullet
  = 
  \left\{
     \itexarray{
        && g_2
        \\
        & {}^{\mathllap{}}\nearrow &=& \searrow^{\mathrlap{}}
        \\
        g_1 &&\stackrel{ }{\longrightarrow}&& g_3
     }
  \right\}
  \,.
\end{displaymath}
This means that it is [[isomorphism|isomorphic]], as a pre-smooth groupoid, to the [[pair groupoid]] of $G$.

\end{remark}
While therefore $(\mathbf{E}G)_\bullet$ is a rather simplistic object, it is nevertheless worthwhile to make its following properties explicit.

\begin{prop}
\label{GActionOnEGForLieGroups}\hypertarget{GActionOnEGForLieGroups}{}
There is an evident morphism of smooth groupoids

\begin{displaymath}
p\colon (\mathbf{E}G)_\bullet \to (\mathbf{B}G)_\bullet
\end{displaymath}
given by

\begin{displaymath}
(g_1, g) \mapsto g
\end{displaymath}
hence

\begin{displaymath}
(g_1 \to g_2) \mapsto (\bullet \stackrel{g_1^{-1}g_2 }{\to} \bullet)
\end{displaymath}
There is an evident $G$-[[action]]

\begin{displaymath}
(\mathbf{E}G)_\bullet \times G \longrightarrow G
\end{displaymath}
given by

\begin{displaymath}
((g_1,g_2), h) \mapsto (g_1 h, g_2 h)
  \,.
\end{displaymath}
The projection $p$ is the [[quotient]] [[projection]] of this action.

\end{prop}
\begin{defn}
\label{NerveOfEGForLieGroup}\hypertarget{NerveOfEGForLieGroup}{}
The [[nerve]] of $(\mathbf{E}G)_\bullet$ is a [[simplicial object]] of the form

\begin{displaymath}
N((\mathbf{E}G)_\bullet)_k = G \times G^{\times_k}
\end{displaymath}
with face maps of the form

\begin{displaymath}
N((\mathbf{B}G)_\bullet)_\bullet
 =
 \left(
   \cdots
   G \times G \times G \times G
    \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}}
   G \times G\times G
    \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}
   G\times G \stackrel{\longrightarrow}{\longrightarrow} 
   G
 \right)
 \,.
\end{displaymath}
If here $(\mathbf{E}G)_\bullet$ is though of isomorphically as $(G//G)_\bullet$, then\newline these face maps are such that all except one outermost (say the topmost) in each degree are given by group multiplication in two consecutive copies of $G$, with the remaining outermost one given by projection.

If on the other hand $(\mathbf{E}G)_\bullet$ is thought of isomorphically as the [[pair groupoid]] of $G$, via remark \ref{bfEGAsPairGroupoid}, then the $k$th face map in each degree is given simply by projecting out the $k$th factor (starting counting at 0).

\end{defn}
\begin{defn}
\label{FibrationOfSmoothGroupoids}\hypertarget{FibrationOfSmoothGroupoids}{}
A morphism $p\colon E_\bullet \to B_\bullet$ of pre-smooth groupoids is called a \emph{[[fibration]]} if for each $n\in \mathbb{N}$ the [[functor]] $p(\mathbb{R}^n) \colon E(\mathbb{R}^n)_\bullet \to B(\mathbb{R}^n)_\bullet$ is an [[isofibration]], hence if for each object $e \in E(\mathbb{R}^n)$, each morphism $p(e) \to b$ in $B(\mathbb{R}^n)$ has a lift through $p$ to a morphism $e \to e'$ in $E$:

\begin{displaymath}
\itexarray{
    e &\stackrel{\exists \psi \in p^{-1}(\phi)}{\to} & \exists e'&&& E 
    \\
     &&&&&  \downarrow^p
    \\
    p(e) &\stackrel{\phi}{\to} & b &&& B
  }
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{EGForLieGroupIsFibrantReplacementOfPointInclusion}\hypertarget{EGForLieGroupIsFibrantReplacementOfPointInclusion}{}
The projection $p \colon (\mathbf{E}G)_\bullet \to (\mathbf{B}G)_\bullet$ of prop. \ref{GActionOnEGForLieGroups} is a fibration of smooth groupoids, def. \ref{FibrationOfSmoothGroupoids}. Moreover, any point inclusion $\ast \longrightarrow \mathbf{E}G$ is over each $\mathbb{R}^n$ an [[equivalence of groupoids]], hence is in particular a local weak equivalence of smooth groupoids (as defined \href{geometry+of+physics+--+smooth+homotopy+types#LocalWeakEquivalence}{here}).

In summary, the morphisms $\ast \to (\mathbf{E}G)_\bullet \stackrel{p}{\to} (\mathbf{B}G)_\bullet$ constitute a factorization of the canonical $\ast \to (\mathbf{B}G)_\bullet$ into a local weak equivalence followed by a fibration.

\end{prop}
\begin{prop}
\label{}\hypertarget{}{}
The smooth groupoid $(\mathbf{E}G)_\bullet$ of def. \ref{EGAsASmoothGroupoid} has the following equivalent incarnations as pre-smooth groupoids by [[isomorphism|isomorphic]] Lie groupoids

\begin{enumerate}%
\item $(\mathbf{E}G)_\bullet \simeq (G//G)_\bullet$ is the [[action groupoid]] of $G$ acting on itself by right multiplication;


\item $(\mathbf{E}G)_\bullet \simeq ((\mathbf{B}G)^{I})_\bullet \underset{(\mathbf{B}G)_\bullet}{\times} \ast$ is the [[pullback]] of the point inclusion $\ast \to (\mathbf{B}G)_\bullet$ along one of the projection map $d_1 \colon ((\mathbf{B}G)^I)_\bullet \longrightarrow (\mathbf{B}G)_\bullet$ out of the [[path space object]] of $(\mathbf{B}G)_\bullet$.



\end{enumerate}
\end{prop}
\begin{proof}
The first statement is immediate from the definitions. The second is also fairly immediate, but worth making more explicit: the Lie groupoid $((\mathbf{B}G)^I)_\bullet$ has as objects the morphisms in $(\mathbf{B}G)_\bullet$, hence elements of $G$, and as morphisms $g_1 \to g_2$ commuting squares between these, schematically:

\begin{displaymath}
((\mathbf{B}G)^I)_\bullet
  =
  \left\{
    \itexarray{
      \bullet &\stackrel{h_1}{\longrightarrow}& \bullet
      \\
      {}^{\mathllap{g_1}}\downarrow && \downarrow^{\mathrlap{g_2}}
      \\
      \bullet &\stackrel{h_2}{\longrightarrow}& \bullet
    }
  \right\}
  \,.
\end{displaymath}
The morphism $d_1$ projects out the top horizontal morophisms:

\begin{displaymath}
d_1
  \;\colon\;
   \left(
    \itexarray{
      \bullet &\stackrel{h_1}{\longrightarrow}& \bullet
      \\
      {}^{\mathllap{g_1}}\downarrow && \downarrow^{\mathrlap{g_2}}
      \\
      \bullet &\stackrel{h_2}{\longrightarrow}& \bullet
    }
  \right)
  \;\;
  \mapsto
  \;\;
   \left(
    \itexarray{
      \bullet &\stackrel{h_1}{\longrightarrow}& \bullet
    }
  \right)  
  \,.
\end{displaymath}
The pullback then restricts this image to be constant and hence produces the groupoid whose objects are still the morphisms in $\mathbf{B}G$, hence elements of $G$, but whose morphisms are no longer all commuting squares, but just all commuting triangles between these, schematically:

\begin{displaymath}
((\mathbf{B}G)^I)_\bullet \underset{(\mathbf{B}G)_\bullet}{\times} \ast
  =
  \left\{
    \itexarray{
      && \bullet
      \\
      & {}^{\mathllap{g_1}}\swarrow && \searrow^{\mathrlap{g_2}}
      \\
      \bullet && \stackrel{h}{\longrightarrow} && \bullet
    }
  \right\}
  \,.
\end{displaymath}
Such a triangle exists precisely if $g_2 = g_1 h$, which gives $\mathbf{E}G$ as in def. \ref{EGAsASmoothGroupoid}, thought of as:

\begin{itemize}%
\item objects = $\left\{
    \itexarray{
    && \bullet
    \\
    & {}^g\swarrow
    \\
    \bullet
    }
  \right\}$


\item morphisms = $\left\{
    \itexarray{
    && \bullet
    \\
    & {}^g\swarrow && \searrow^{g' = g h}
    \\
    \bullet &&\stackrel{h}{\longrightarrow}&& \bullet
    }
  \right\}
  \,.$



\end{itemize}
\end{proof}
\hypertarget{principal_bundles_2}{}\paragraph*{{$G$-Principal bundles}}\label{principal_bundles_2}

The traditional construction of the $G$-principal bundle associated to a [[Cech cohomology|Cech cocycle]] is the following.

\begin{defn}
\label{TraditionalConstructionOfGBundleFormCocycle}\hypertarget{TraditionalConstructionOfGBundleFormCocycle}{}
Let $X$ be a [[smooth manifold]], $\{U_i \to X\}_I$ an [[open cover]] and $(g_{i j})_{i,j \in I}$ a [[Cech cohomology|Cech cocycle]] of degree 1 with values in $G$. Then the [[bundle]] $P \to X$ associated with this data is the [[quotient]]

\begin{displaymath}
P \coloneqq \left( \coprod_{i} U_i \times G \right)/{\sim}
\end{displaymath}
of the [[Cartesian product]] of the [[cover]] (regarded as the [[disjoint union]] of its patches) with $G$, by the [[equivalence relation]] which identifies two elements in the product whenever they are related by the Cech cocycle:

\begin{displaymath}
((x,i),g) \sim ((x,j), g \cdot g_{i j}(x))
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{GBundleAsPullbackAlongCechCocycle}\hypertarget{GBundleAsPullbackAlongCechCocycle}{}
Let $X$ be a [[smooth manifold]], $\{U_i \to X\}_I$ an [[open cover]] and $(g_{i j})_{i,j \in I}$ a [[Cech cohomology|Cech cocycle]] of degree 1 with values in $G$. Then the associated $G$-bundle $P$, def. \ref{TraditionalConstructionOfGBundleFormCocycle}, is equivalent, regarded as a [[smooth groupoid]] with only identity morphisms, to the [[pullback]] of the morphism $(\mathbf{E}G)_\bullet \to (\mathbf{B}G)_\bullet$ of def. \ref{EGAsASmoothGroupoid} along the cocycle regarded as a homomorphism of [[smooth groupoids]] $C(\{U_i\})_\bullet \stackrel{g}{\longrightarrow} (\mathbf{B}G)_\bullet$.

\begin{displaymath}
\itexarray{
     P &\overset{\simeq}{\longleftarrow}& C(\{U_i\})_\bullet \underset{(\mathbf{B}G)_\bullet}{\times} (\mathbf{E}G)_\bullet &\longrightarrow& (\mathbf{E}G)_\bullet
     \\
     \downarrow && \downarrow && \downarrow
     \\
     && C(\{U_i\})_\bullet &\stackrel{g}{\longrightarrow}& (\mathbf{B}G)_\bullet
     \\
     &\searrow & \downarrow^{\mathrlap{\simeq}}
     \\
     && X
  }
\end{displaymath}
\end{prop}
\begin{proof}
Pullbacks of pre-smooth groupoids are computed componentwise. Hence a morphism in $C(\{U_i\})_\bullet\underset{(\mathbf{B}G)_\bullet}{\times} (\mathbf{E}G)_\bullet$ is a pair consisting of a morphism $(x,i,j)$ in $C(\{U_i\})_\bullet$ and a morphism $(g_1, h)$ in $(\mathbf{E}G)_\bullet$ such that $h$ is the value of the cocycle on $(x,i,j)$.

With $(\mathbf{E}G)_\bullet$ thought of as in remark \ref{bfEGAsPairGroupoid}, then the pullback looks like:

\begin{itemize}%
\item objects =

\begin{displaymath}
\left\{
 \itexarray{
   && \bullet
   \\
   & {}^{g}\swarrow
   \\
   \bullet
   \\
   (x,i)
 }
 \right\}
\end{displaymath}

\item morphisms =

\begin{displaymath}
\left\{
 \itexarray{
   && \bullet
   \\
   & {}^{g}\swarrow && \searrow^{g'}
   \\
   \bullet &&\stackrel{g_{i j }(x)}{\to}&& \bullet
   \\
   (x,i) &&\stackrel{}{\to}&& (x,j)
 }
 \right\}
\end{displaymath}


\end{itemize}
This means that the morphisms in the pullback are of the form

\begin{displaymath}
\itexarray{
     ((x,i),g_1) &&\stackrel{\simeq}{\to}&& ((x,j), g_1 g_{i j}(x) )
  }
\end{displaymath}
and there is at most one for any ordered pair of objects. But this means that these morphisms represent precisely the [[equivalence relation]] of def. \ref{TraditionalConstructionOfGBundleFormCocycle}: the evident projection map from this pullback to $P$ (with $P$ regarded as a groupoid with only identity morphisms) is evidently [[essentially surjective functor|essentially surjective]] and [[fully faithful functor|fully faithful]], hence an equivalence.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
By the pullback construction in prop. \ref{GBundleAsPullbackAlongCechCocycle}, $P$ inherits a $G$-action from that on $(\mathbf{E}G)_\bullet$ of def. \ref{GActionOnEGForLieGroups}:

via the [[pasting]] diagram of pullbacks

\begin{displaymath}
\itexarray{
     \tilde P \times G &\to& (\mathbf{E}G)_\bullet \times G
     \\
     \downarrow && \downarrow
     \\
     \tilde P &\to& (\mathbf{E}G)_\bullet
     \\
     \downarrow && \downarrow
     \\
     C(\{U_i\})_\bullet &\stackrel{g}{\to}& (\mathbf{B}G)_\bullet
     \\
     \downarrow^{\mathrlap{\simeq}}
     \\
     X
  }
  \,.
\end{displaymath}
The morphism $\tilde P \times G \to \tilde P$ exhibits the principal $G$-[[action]] of $G$ on $\tilde P$.

\end{remark}
\hypertarget{fibration_categories_and_the_factorization_lemma}{}\paragraph*{{Fibration categories and the Factorization lemma}}\label{fibration_categories_and_the_factorization_lemma}

We saw \hyperlink{PrincipalBundlesViaSmoothGroupoids}{above} that smooth $G$-[[principal bundles]] for $G$ a [[Lie group]] may naturally be understood in terms of pullbacks of the fibrant replacement $\mathbf{E}G\to \mathbf{B}G$ of the point inclusion $\ast \to \mathbf{B}G$ along a Cech cocycle, regarded as a homomorphism of smooth groupoids.

This is a special case of a very general construction of [[homotopy pullbacks]] which will also apply, below, to \hyperlink{WeakyPrincipalSimplicialBundles}{weakly principal simplicial bundles} and then generally to [[principal infinity-bundles]]. We now discuss the general axiomatization of this construction via [[categories of fibrant objects]].

\hypertarget{categories_of_fibrant_objects}{}\paragraph*{{Categories of Fibrant objects}}\label{categories_of_fibrant_objects}

\begin{defn}
\label{CategoryOfFibrantObjects}\hypertarget{CategoryOfFibrantObjects}{}
A \textbf{[[category of fibrant objects]]} $\mathcal{C}$ is

\begin{itemize}%
\item a [[category with weak equivalences]], i.e equipped with a subcategory $W$ that contains all [[isomorphisms]]

\begin{displaymath}
Core(\mathcal{C}) \hookrightarrow W \hookrightarrow \mathcal{C}
  \,,
\end{displaymath}
where $f \in Mor(W)$ is called a \textbf{weak equivalence};


\item equipped with a further subcategory

\begin{displaymath}
Core(\mathcal{C}) \hookrightarrow F \hookrightarrow \mathcal{C}
  \,,
\end{displaymath}
where $f \in Mor(F)$ is called a \textbf{fibration}

Those morphisms which are both weak equivalences and fibrations are called \textbf{acyclic fibrations} .



\end{itemize}
This data has to satisfy the following properties:

\begin{itemize}%
\item $\mathcal{C}$ has [[finite products]], and in particular a [[terminal object]] ${\ast}$;


\item the [[pullback]] of a fibration along an arbitrary morphism exists, and is again a fibration;


\item acyclic fibrations are preserved under [[pullback]];


\item weak equivalences satisfy [[category with weak equivalences|2-out-of-3]];


\item for every object there exists a [[path object]]

\begin{itemize}%
\item this means: for every object $B$ there exists at least one object denoted $B^I$ (not necessarily but possibly the [[internal hom]] with an [[interval object]]) that fits into a diagram

\end{itemize}
\begin{displaymath}
(B \stackrel{Id \times Id}{\to} B \times B)
  =
  (B \stackrel{\sigma}{\to} B^I \stackrel{d_0 \times d_1}{\to} B \times B)
\end{displaymath}
where $\sigma$ is a weak equivalence and $d_0 \times d_1$ is a fibration;


\item all objects are \emph{fibrant}, i.e. all morphisms $B \to {\ast}$ to the terminal object are fibrations.



\end{itemize}
\end{defn}
\begin{prop}
\label{PreSmoothGroupoidsFormCategoryOfFibrantObjects}\hypertarget{PreSmoothGroupoidsFormCategoryOfFibrantObjects}{}
The category of pre-smooth groupoids (\href{geometry%20of%20physics%20--%20smooth%20homotopy%20types#PreSmoothGroupoids}{here}) becomes a category of fibrant objects, def. \ref{CategoryOfFibrantObjects} with fibrations as in def. \ref{FibrationOfSmoothGroupoids} and weak equivalences the local weak equivalences (as defined \href{geometry+of+physics+--+smooth+homotopy+types#LocalWeakEquivalence}{here}).

\end{prop}
\hypertarget{factorization_lemma}{}\paragraph*{{Factorization lemma}}\label{factorization_lemma}

Let $C$ be a [[category of fibrant objects]]. The \emph{[[factorization lemma]]} says the following.

\begin{lemma}
\label{FactorizationLemma}\hypertarget{FactorizationLemma}{}
Every [[morphism]] $f : X \to Y$ in $C$ factors as

\begin{displaymath}
f : X \underoverset{\simeq}{i}{\longrightarrow} \hat X \stackrel{p}{\longrightarrow} Y
  \,,
\end{displaymath}
where

\begin{enumerate}%
\item $i$ is a weak equivalence (even a [[right inverse]] to an acyclic fibration);


\item $p$ is a [[fibration]].



\end{enumerate}
\end{lemma}
\begin{proof}
Let $Y^I$ with factorization $Y \stackrel{\simeq}{\to} Y^I \stackrel{(d_0,d_1)}{\longrightarrow} Y \times Y$ be a [[path space object]] for $Y$. Let $\hat X \coloneqq Y^I \times_Y X$ be the [[pullback]] of $f$ along one of its legs, to get the diagram

\begin{displaymath}
\itexarray{
     \hat X &\to& X
     \\
     \downarrow && \downarrow^{\mathrlap{f}}
     \\
     Y^I &\stackrel{d_1}{\to}& Y
     \\
     \downarrow^{\mathrlap{d_0}}
     \\
     Y
  }
  \,.
\end{displaymath}
Take $p$ to be the composite vertical morphism in the above diagram, hence

\begin{displaymath}
p \;\colon\; \hat X \to Y^I \stackrel{d_0}{\to} Y
  \,.
\end{displaymath}
To see that this is indeed a fibration, notice that, by the [[pasting law]], the above pullback diagram can be refined to a double pullback diagram as follows

\begin{displaymath}
\itexarray{
    \hat X
     &\stackrel{}{\to}& 
     X \times Y 
     &\stackrel{p_1}{\to}& 
     X
     \\
     \downarrow && \downarrow^{\mathrlap{(f, Id)}} && \downarrow^\mathrlap{f}
     \\
     Y^I &\stackrel{(d_1 , d_0) }{\to}&
     Y \times Y &\stackrel{p_1}{\to}&
     Y
     \\
     \downarrow^{\mathrlap{d_0}} & \swarrow_{p_2}
     \\
     Y
  }
  \,.
\end{displaymath}
Both squares are pullback squares. Since pullbacks of fibrations are fibrations, the morphism $\hat X  \to X \times Y$ is a fibration. Similarly, since $X$ is assumed to be fibrant (as all objects in a [[category of fibrant objects]]), also the [[projection]] map $X \times Y \to Y$ is a fibration (see \href{category+of+fibrant+objects#SimpleConsequences}{here}).

Since $p$ is thereby exhibited as the composite of two fibrations

\begin{displaymath}
\begin{aligned}
    p &: \hat X \to X \times Y
    \stackrel{(f ,Id)}{\to}
    Y \times Y
    \stackrel{p_2}{\to}
    Y
  \end{aligned}
  \,,
\end{displaymath}
(the first map being a pullback of a fibration as above, the composite of the second and the third map being the projection just menioned) it is itself a fibration.

Next, by the [[axioms]] of [[path space objects]] in a [[category of fibrant objects]] we have that $d_1 \;\colon\; Y^I \to Y$ is an acyclic fibration. Since these are stable under pullback, also $\hat X \to X$ is an acyclic fibration.

But, by the axioms, $Y^I \to Y$ has a right inverse $Y \to Y^I$. By the [[pullback]] property this induces a right inverse of $\hat X \to X$ fitting into a [[pasting]] diagram

\begin{displaymath}
\itexarray{
     X &\to& \hat X &\to& X
     \\
     {}^{\mathrlap{f}}\downarrow && \downarrow && \downarrow^{\mathrlap{f}}
     \\
     Y &\to& Y^I &\stackrel{d_1}{\to}& Y
     \\
     & {}_{\mathllap{Id}}\searrow& \downarrow^{\mathrlap{d_0}} 
     \\
     && Y
  }
  \,.
\end{displaymath}
This establishes the claim.

\end{proof}
\hypertarget{homotopy_and_homotopy_pullback}{}\paragraph*{{Homotopy and Homotopy pullback}}\label{homotopy_and_homotopy_pullback}

Let $\mathcal{C}$ be a [[category of fibrant objects]].

\begin{defn}
\label{}\hypertarget{}{}
Two morphism $f,g : A \to B$ in $\mathcal{C}(A,B)$ are

\begin{itemize}%
\item \textbf{right [[homotopy|homotopic]]}, denoted $f \simeq g$, precisely if they fit into a diagram of the form

\begin{displaymath}
\itexarray{
    && B
    \\
    & {}^f\nearrow & \uparrow^{d_0}
    \\
    A &\stackrel{\eta}{\to}&
    B^I
    \\
    & {}_g\searrow & \downarrow^{\mathrlap{d_1}}
    \\
    && B
  }
\end{displaymath}
for some [[path object|path space object]] $B^I$;


\item \textbf{[[homotopy|homotopic]]}, denoted $f \sim g$, if they become right homotopic after pulled back to a weakly equivalent domain, i.e. precisely if they fit into a diagram of the form



\end{itemize}
\begin{displaymath}
\itexarray{
    &&
    A 
    &\stackrel{f}{\to}& B
    \\
    &{}^{w \in W}\nearrow&&& \uparrow^{d_0}
    \\
    \hat A 
    &&
    \stackrel{\eta}{\to}
    &&
    B^I
    \\
    &{}_{w\in W}\searrow & &&
    \downarrow^{d_1}
    \\
    &&
    A
    &\stackrel{g}{\to}& 
    B
  }
\end{displaymath}
for some object $\hat A$ and for some [[path object|path space object]] $B^I$ of $I$

\end{defn}
In view of this the following definition is natural.

\begin{defn}
\label{HomotopyFiberProducts}\hypertarget{HomotopyFiberProducts}{}
A \textbf{homotopy fiber product} or \textbf{homotopy pullback} of two morphisms

\begin{displaymath}
A \stackrel{u}{\to} C \stackrel{v}{\leftarrow} B
\end{displaymath}
in a category of fibrant objects is the object $A \times_C C^I \times_C B$ defined as the (ordinary) [[nLab:limit|limit]]

\begin{displaymath}
\itexarray{
    A \times_C C^I \times_C B &\longrightarrow& &\longrightarrow & B
    \\
    \downarrow &&&& \downarrow^v
    \\
    & &C^I & \stackrel{d_0}{\to}& C
    \\
    \downarrow &&
    \downarrow^{\mathrlap{d_1}}
    \\
    A &\stackrel{u}{\to} & C    
  }
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{}\hypertarget{}{}
The homotopy fiber product in def. \ref{HomotopyFiberProducts} is [[isomorphism|isomorphic]] to the ordinary [[fiber product]] of either of the two morphisms with the fibration replacement of the other as given by the factorization lemma, def. \ref{FactorizationLemma}.

\end{prop}
\begin{proof}
By basic properties of [[limits]] the defining limit in def. \ref{HomotopyFiberProducts} may be computed by two consecutive pullbacks.

\begin{displaymath}
\itexarray{
    A \times_C C^I \times_C B \simeq & A \underset{C}{\times} \left(C^I \underset{C}{\times} B\right)  &\to& C^I \underset{C}{\times} B &\to 
    & B
    \\
    & \downarrow && \downarrow && \downarrow^{\mathrlap{v}}
    \\
    & & &C^I & \stackrel{d_0}{\to}& C
    \\
    & \downarrow &&
    \downarrow^{\mathrlap{d_1}}
    \\
    & A &\stackrel{u}{\to}& C    
  }
  \,.
\end{displaymath}
Here the intermediate pullback is precisely the one appearing in the proof of the factorization lemma.

\end{proof}
\begin{example}
\label{}\hypertarget{}{}
With $\mathcal{C}$ the category of fibrant objects given by pre-smooth groupoids, prop. \ref{PreSmoothGroupoidsFormCategoryOfFibrantObjects}, then for $G$ a Lie group, the factorization $\ast \to \mathbf{E}G \stackrel{p}{\to} \mathbf{B}G$ of prop. \ref{EGForLieGroupIsFibrantReplacementOfPointInclusion} is the one given by the [[factorization lemma]]. Hence a pullback of $p \colon \mathbf{E}G\to \mathbf{B}G$ as in prop. \ref{GBundleAsPullbackAlongCechCocycle} is equivalently the homotopy pullback of $\ast \to \mathbf{B}G$.

\end{example}
\hypertarget{WeakyPrincipalSimplicialBundles}{}\paragraph*{{Weakly principal simplicial bundles}}\label{WeakyPrincipalSimplicialBundles}

(\ldots{} under construction \ldots{})

It is no coincidence that the above statement looks akin to the maybe more familiar statement which says that \emph{equivalence classes} of $G$-principal bundles are classified by [[homotopy]]-classes of morphisms of [[topological space]]s

\begin{displaymath}
\pi_0 Top(X, \mathbf{B}G)
  \simeq
  \pi_0 G Bund(X)
  \,,
\end{displaymath}
where $\mathbf{B}G \in$ [[Top]] is the topological [[classifying space]] of $G$. The category [[Top]] of topological spaces, regarded as an [[(∞,1)-category]], is the archetypical [[(∞,1)-topos]] the way that [[Set]] is the archetypical [[topos]]. And it is equivalent to [[∞Grpd]], the $(\infty,1)$-category of bare [[∞-groupoid]]s. What we are seeing above is a first indication of how [[cohomology]] of bare $\infty$-groupoids is lifted to a richer $(\infty,1)$-topos to cohomology of $\infty$-groupoids with extra structure.

In fact, all of the statements that we have considered so far become conceptually \emph{simpler} in the $(\infty,1)$-topos. We had already remarked that the [[anafunctor]] span $X \stackrel{\simeq}{\leftarrow} C(U) \stackrel{g}{\to} \mathbf{B}G$ is really a model for what is simply a direct morphism $X \to \mathbf{B}G$ in the $(\infty,1)$-topos. But more is true: that pullback of $\mathbf{E}G$ which we considered is just a model for the [[homotopy pullback]] of just the \emph{point}

\begin{displaymath}
\itexarray{
     \vdots && \vdots
     \\
     \tilde P \times G &\to& \mathbf{E}G \times G
     \\
     \downarrow && \downarrow
     \\
     \tilde P &\to& \mathbf{E}G
     \\
     \downarrow && \downarrow
     \\
     C(U) &\stackrel{g}{\to}& \mathbf{B}G
     \\
     \downarrow^{\mathrlap{\simeq}}
     \\
     X
     \\
     {}
     \\
     {}
     \\
     & in\;the\;model\;category &
  }
  \;\;\;\;\;\;\;
  \;\;\;\;\;\;\;
  \;\;\;\;\;\;\;
  \itexarray{
     \vdots && \vdots
     \\
     P \times G &\to& G
     \\
     \downarrow &\swArrow_{\simeq}& \downarrow
     \\
     P &\to& * 
     \\
     \downarrow &\swArrow_{\simeq}& \downarrow 
     \\
     X &\stackrel{}{\to}& \mathbf{B}G
     \\
     .
     \\
     .
     \\
     \\
     \\
     & in\;the\;(\infty,1)-topos
  }
  \,.
\end{displaymath}
\hypertarget{universal_principal_bundle}{}\paragraph*{{Universal principal bundle}}\label{universal_principal_bundle}

\begin{itemize}%
\item [[groupal model for universal principal infinity-bundles]]

\end{itemize}
\hypertarget{weakly_principal_simplicial_bundles_2}{}\paragraph*{{Weakly principal simplicial bundles}}\label{weakly_principal_simplicial_bundles_2}

The [[principal ∞-bundles]] that we wish to model are already the main and simplest example of the application of these three items:

Consider an object $\mathbf{B}G \in [C^{op}, sSet]$ which is an $\infty$-groupoid with a single object, so that we may think of it as the [[delooping]] of an [[∞-group]] $G$, let $*$ be the point and $* \to \mathbf{B}G$ the unique inclusion map. The \emph{good replacement} of this inclusion morphism is the $G$-[[universal principal ∞-bundle]] $\mathbf{E}G \to \mathbf{B}G$ given by the pullback diagram

\begin{displaymath}
\itexarray{ 
    \mathbf{E}G &\to& *
    \\
    \downarrow && \downarrow
    \\
    \mathbf{B}G^{\Delta[1]} &\to& \mathbf{B}G
    \\
    \downarrow
    \\
     \mathbf{B}G
   }
\end{displaymath}
An [[∞-anafunctor]] $X \stackrel{\simeq}{\leftarrow} \hat X \to \mathbf{B}G$ we call a [[cocycle]] on $X$ with coefficients in $G$, and the [[(∞,1)-pullback]] $P$ of the point along this cocycle, which by the above discussion is the ordinary [[limit]]

\begin{displaymath}
\itexarray{ 
    P &\to& \mathbf{E}G &\to& *
    \\
    \downarrow && \downarrow && \downarrow
    \\
    && \mathbf{B}G^I &\to& \mathbf{B}G
    \\
    \downarrow && \downarrow
    \\
    \hat X &\stackrel{g}{\to}& \mathbf{B}G
    \\
    \downarrow^{\mathrlap{\simeq}}
    \\
    X
  }
\end{displaymath}
we call the [[principal ∞-bundle]] $P \to X$ classified by the cocycle.

It is now evident that our discussion of ordinary smooth principal bundles \hyperlink{PrincipalBundles}{above} is the special case of this for $\mathbf{B}G$ the [[nerve]] of the one-object groupoid associated with the ordinary [[Lie group]] $G$.

So we find the complete generalization of the situation that we already indicated there, which is summarized in the following diagram:

\begin{displaymath}
\itexarray{
     \vdots && \vdots
     \\
     \tilde P \times G &\to& \mathbf{E}G \times G
     \\
     \downarrow && \downarrow
     \\
     \tilde P &\to& \mathbf{E}G
     \\
     \downarrow && \downarrow
     \\
     C(U) &\stackrel{g}{\to}& \mathbf{B}G
     \\
     \downarrow^{\mathrlap{\simeq}}
     \\
     X
     \\
     {}
     \\
     {}
     \\
     & in\;the\;model\;category &
  }
  \;\;\;\;\;\;\;
  \;\;\;\;\;\;\;
  \;\;\;\;\;\;\;
  \itexarray{
     \vdots && \vdots
     \\
     P \times G &\to& G
     \\
     \downarrow && \downarrow
     \\
     P &\to& * 
     \\
     \downarrow &\swArrow_{\simeq}& \downarrow 
     \\
     X &\stackrel{}{\to}& \mathbf{B}G
     \\
     .
     \\
     .
     \\
     \\
     \\
     & in\;the\;(\infty,1)-topos
  }
  \,.
\end{displaymath}
\begin{itemize}%
\item [[simplicial principal bundle]]

\end{itemize}
\hypertarget{semantic_layer}{}\subsubsection*{{Semantic Layer}}\label{semantic_layer}

\hypertarget{principal_bundles_3}{}\paragraph*{{Principal $\infty$-bundles}}\label{principal_bundles_3}

\begin{itemize}%
\item [[homotopy fiber]]


\item [[homotopy colimit]]


\item [[principal infinity-bundle]]



\end{itemize}
\hypertarget{syntactic_layer}{}\subsubsection*{{Syntactic Layer}}\label{syntactic_layer}

\begin{itemize}%
\item [[connected type]]

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

\begin{itemize}%
\item [[Thomas Nikolaus]], [[Urs Schreiber]], [[Danny Stevenson]], \emph{[[schreiber:Principal ∞-bundles -- theory, presentations and applications]]}

\end{itemize}


\end{document}