For a functor F : C → D, we write C ↓ c --[F ↓ c]-> D ↓ F(c) for the action of F on the slice over c ∈ C. Lemma {pullback-terminal-object}. Consider a pullback of categories E₁ --[G]-> E₀ |P₁ pb |P₀ B₁ --[F]-> B₀. Assume one of: (a) F is an isofibration and has a fully faithful right adjoint, (b) P₀ is a cartesian fibration and F has a right adjoint. If E₀ has a terminal object, then so does E₁. Proof. A direct verification. ∎ Proposition {pullback-left-adjoint}. Consider a pullback of categories E₁ --[G]-> E₀ |P₁ pb |P₀ B₁ --[F]-> B₀. Assume one of: (a) F is a cartesian fibration, (b) P₀ is a cartesian fibration and F has left adjoint actions on slices. If P₀ is has a right adjoint, then so does P₁. Proof. Given b₁ ∈ B₁, we want a terminal object in P₁ ↓ b₁. We have an induced pullback of categories P₁ ↓ b₁ -----------> P₀ ↓ F(b₁) |P₁ pb |P₀ B₁ ↓ b₁ --[F ↓ b₁]-> B₀ ↓ F(b₁). Since P₀ has a right adjoint, we have a terminal object in P₀ ↓ F(b₁). We obtain a terminal object in P₁ ↓ b₁ using Lemma {pullback-terminal-object}: (a) Since F is an isofibration, so is F ↓ b₁. Since F is a cartesian fibration, F ↓ b₁ has a fully faithful right adjoint (given by cartesian lifting). (b) The right map in the above square in a cartesian fibration as well and the bottom map has a right adjoint. ∎ Recall that a right fibration is *locally representable* if it has a right adjoint. Remark. Recall the usual notion of (locally) representable map in presheaves as follows. Consider a pseudonatural transformation Y → X of groupoid-valued pseudo-presheaves Y → X over a category C. We have an induced right fibration ∫ Y ---> ∫ X between categories of elements. The map Y → X is (locally) representable exactly if ∫ Y → ∫ X is locally representable. Note that this no longer depends on C. This simplifies the notion and makes it easier to establish. ∎ Essentially from the definition, locally (representable) maps in groupoid-valued pseudo-presheaves are closed under pullback. On categories of elements, this is a pullback along a right fibration. The next corollary can be understood as a generalization of this fact. Corollary {pullback-locally-representable}. Locally representable right fibrations are closed under pullback along: (a) cartesian fibrations, (b) functors with left adjoint action on slices. ∎ Recall that adjunctions descend to slices (assuming the necessary pullbacks). So a special case of (b) is the following: (b') left adjoints whose source has pullbacks along the components of the unit map. Write C^[1]_cart for the restriction of the arrow category of C to: * objects that admit base change, * morphisms that are cartesian squares. Example {dom-action-on-slices-left-adjoint}. For the domain projection C^[1]_cart --[dom]-> C and a map f : Y → X, the induced functor C^[1]_cart ↓ f ---> C ↓ Y is equivalent to pullback f^* : C ↓ X → C ↓ Y. Thus, a right adjoint would be given by pushforward along f. ∎ A *notion of fibred structure* is a right fibration S ---> C^[1]_cart. Our (locally representable) notions of fibred structures agree with Shulman's [arxiv:1904.07004v2]. Remark. We decompose Shulman's observation [arxiv:1904.07004v2, Example 3.12] that locally representable notions of fibred structure are created by pullback-preserving left adjoints L : D → C. Consider a notion of fibred structure S ---> C^[1]_cart where C has pullbacks. Ppreservation of pullbacks means that L lifts to a left adjoint D^[1]_cart --[L']-> C^[1]_cart. Then Corollary {pullback-locally-representable} allows us to create in representability in the pullback T ----------------> S | pb | D^[1]_cart --[L']-> C^[1]_cart. ∎ Remark. The corollary also modularizes [arxiv:2406.18497v1, Lemma 2.1.16 (ii)], which we now review. Consider categories C and D with pullbacks. Consider pullback-preserving functors L, K : D → C with a natural transformation α : D → C. Assume that the induced functor D ↓ d ---> C ↓ L(d) has a right adjoint for d ∈ D. Consider a notion of fibred structure S on C. Define a notion of fibred structure T on D as follows. Create T via pullback application of α: T -------------------------> S | pb | D^[1]_cart --[(app)(α, -)]-> C^[1]_cart, so that a T-structure on Y → X is an S-structure on LY → LX ×_KX KY. If S is locally representable, then so is T. We give a modular proof of this claim. By Corollary {pullback-locally-representable}, it suffices to show that (app)(α, -) has left adjoint action on slices. We decompose this as D^[1]_cart ---> C^[2]_cart ---> C^[1]_cart where the first functor sends Y → X to the sequence LY ---> LX ×_KX KY ---> LX and the second functor sends a sequence to its first factor. It suffices to separately show that the actions of each factor on slices have right adjoints. We examine the first factor. The composition functor C^[2]_cart ---> C^[1]_cart has invertible action on slices. Therefore, it suffices to show that the composite D^[1]_cart ---> C^[2]_cart ---> C^[1]_cart has left adjoint action on slices. But this is just the lift of L' as in the previous remark, a left adjoint. We examine the second factor. Its actions on slices are equivalent to the actions on slices of C^[1]_cart --[dom]-> C. These are left adjoint by Example {dom-action-on-slices-left-adjoint}. ∎ Example. Consider notion of fibred structure S and T in a category C. The *stacking* T • S is the notion of fibred structure given by composites of a map in T and a map in S. Formally, this is defined by the pullback T • S ----> T | |cod S --[dom]-> C. Note that this forms a monoidal structure on notions of fibred structures. Suppose cod : S → C and T : S → C are locally representable. Assume pushforward along S-types. Then cod : T • S → C is locally representable. To see this, consider the cocell complex T • S ----> T | pb |cod S --[dom]-> C |cod C. The bottom map is locally representable by assumption. For the top map, we use above Corollary and Example. Note that the nullary stacking is trivially locally representable. So the stacking monoidal structure lifts to locally representable notions of fibred structure whose underlying maps admit pushforward. ∎ Example. The above example appears in splitting constructions ("coherence methods") for models of type theory. For example, in the global universe coherence method, one builds universal contexts in which it suffices to interpret certain rules. Categorically, these correspond to representations of certain right fibrations. This starts with a representation ty_p ∈ Ty(p : Ũ → U) of cod : Ty → C. We asume: * C has a terminal object 1, * U → 1 admits base change, * Ũ → U admits base change, * Ũ → U admits pushforward. Because of the first three conditions, products with U and Ũ exist, so cod : Ty → C is locally representable. Then so is cod : Ty^(n) → C by the above example. For example, for the Σ-type formation rule, one has A ∈ Ty(Γ) and B ∈ Ty(Γ.A), that is, (A, B) ∈ Ty^(2)(Γ). The universal context is given by the representation of cod : Ty^(2) → Γ. This is local representation at 1, computing as expected to exp_U(p, U^* U) ---> exp_U(p, U^* Ũ). Note that we did not assume C to be a presheaf category. ∎