higher geometry / derived geometry
geometric little (∞,1)-toposes
geometric big (∞,1)-toposes
derived smooth geometry
Higher Cartan geometry is the generalization of Cartan geometry to higher geometry.
It is the globalized version of higher Klein geometry.
As Cartan geometry is a special case of the theory of principal connections, so higher Cartan geometry is a special case of the theory of ∞-connections on principal ∞-bundles.
Let $\mathfrak{h} \to \mathfrak{g}$ be a morphism of L-∞ algebras. Write $i : \mathbf{B}H \to \mathbf{B}G$ for a Lie integration to a morphism of smooth ∞-groups. Notice that this defines a higher Klein geometry
Let $X$ be a smooth ∞-groupoid. For $x : * \to X$ any point, write $T_x X$ for its tangent $L_\infty$-algebra.
An $\infty$-Cartan geometry over $X$ with respect to $i$ is
a $G$-principal ∞-bundle $P \to X$ whose structure group reduces to $H$, hence such that there is morphism $g : X \to \mathbf{B}H$ and a fiber sequence
equipped with an $\mathfrak{g}$ ∞-connection $\nabla$;
such that for every point $x : * \to X$ any any local trivialization, the canonical composite
(of the ∞-Lie algebra valued differential form of the connection at that point) with the quotient projection is an equivalence.
Notice that ordinary gravity can be understood as the theory of $(O(d,1) \hookrightarrow Iso(d,1))$-Cartan geometry, where $Iso(d,1)$ is the Poincare group and $O(d,1)$ the orthogonal group of Minkowski space. This is called the first order formulation of gravity.
One can read the D'Auria-Fre formulation of supergravity as saying that higher dimensional supergravity is analogously given by higher Cartan supergeometry. See there and see the examples at higher Klein geometry for more on this.