Double Functorial Representation of Indexed Monoidal Structures

Explore the double functorial representation of indexed monoidal structures in this Oxford Seminar presentation. Discover how Double Category Theory provides essential tools to capture the dual actions of substitution operations and quantification in logical doctrines, examining their concomitant relationship through double categories of spans where re-indexing and predicate actions are packaged as tight and loose arrows respectively. Learn how tight arrows possess conjoints that, when mapped into double categories of quintets, yield adjunctions internal to a 2-category, with the indexing category requiring only certain pullbacks through the notion of adequate triple. Investigate the addition of monoidal structures to fibers and double pseudofunctors to capture both Beck-Chevalley and Frobenius conditions, focusing on monoidal analogues of regular hyperdoctrines and similar structures where predicate objects exist within 2-categories rather than necessarily being posets. Understand the equivalence between these structures and lax symmetric monoidal double pseudofunctors operating between spans and quintet double categories, providing a comprehensive framework for understanding the categorical foundations of logical reasoning and predicate manipulation.