Supplementary notes

Projection computations and endpoint comparisons when substituting into the universal coherence laws.

The five derived whiskering laws and the middle interchange in horizontal composition.

Endpoint transport, equivalences of identification animae, and lifts with specified images.

Projection tests for pairing, naturality, and compatibility with successive and identity substitutions.

The decoding equivalence on identification animae and its full compatibility square with restriction.

From the mapping-anima universal property to restriction of identifications, with prescribed images on both summands.

Restriction comparisons, pasted matchings, and the factorization equation behind pullback pasting.

Recovering fiber cones from diagonal coordinates and deriving the specified diagonal representability square.

The cone comparisons and matching compatibility behind preservation of pullbacks by functor categories.

The full matching comparison needed to turn pushout pasting into pullback pasting on mapping animae.

Endpoint frames and the full pullback computation law for families of arrows with prescribed source and target.

Endpoint-preserving restriction, successive substitutions, and changes of parameters in chosen composite presentations.

Changing the order of pullback constraints while retaining the projection to a family of invertible arrows.

Naturality and exponential compatibility of constant diagrams, with the coproduct comparison used in recognizing animae.

Naturality and exponential compatibility of constant diagrams, with the coproduct comparison used in recognizing animae.

Normalization of endpoint cones and computation of the hom-category composition functors under restriction.

Gluing specified family lifts and recovering the arrows of a generated subcategory.

Endpoint computations turning a coherent object-family factorization into a family of functors through a full subcategory.

Lifting identifications with their prescribed restrictions and reflecting the matching equations of cocones.

Lifting identifications with their prescribed restrictions and reflecting the matching equations of cocones.

Evaluating the inversion data at the identity functor and identifying the localization of the interval.

Naming, decoding and comparing functors while retaining their specified triangle over the base.

Base-change comparisons, including the full pullback-cone and base-triangle computations for composition.

Computing relative uncurrying on named triangles and deriving the finite laws for the induced dependent-product action.

Normalizing the join span and retaining the full cocone comparison for its pushout-defined action.

Exponential restriction, constant families and cylinder coordinates in the specified absolute slice pullback.

Lifting identifications with their prescribed restrictions and reflecting the matching equations of cocones.

Computing relative uncurrying on named triangles and deriving the finite laws for the induced dependent-product action.