Left/Right Vertical Adjoints are (Op)Fibred, Optimize Diagram Fibration#223

Open

TOTBWF wants to merge 10 commits intomainfrom displayed-adjuncts

+669-170

Commits on Aug 2, 2023

def: avoid transports in diagram fibration

TOTBWF
authored and
plt-amy
committed
def: restriction of vertical functors/natural transformations

TOTBWF
authored and
plt-amy
committed
chore: rexport Displayed from Displayed.Reasoning

TOTBWF
authored and
plt-amy
committed
wip: some random junk about vertical functors

TOTBWF
authored and
plt-amy
committed
def: vertical adjuncts, all right vertical adjoints are fibred

TOTBWF
authored and
plt-amy
committed
def: vertical left adjoints are opfibred

TOTBWF
authored and
plt-amy
committed
chore: tiny bit of prose

TOTBWF
authored and
plt-amy
committed
refactor: move around files, update index

TOTBWF
authored and
plt-amy
committed
fix: fix link

TOTBWF
authored and
plt-amy
committed
minor spelling mistake
plt-amy
committed