Lifting Refactor#555

Merged

plt-amy merged 27 commits intomainfrom

lifting-refactor

Sep 1, 2025

Commits on Sep 1, 2025

def: classes of morphisms

TOTBWF
and
plt-amy
committed
chore: rework arrow category

TOTBWF
and
plt-amy
committed
def: general lifting machinery

TOTBWF
authored and
plt-amy
committed
refactor: use a class-based approach for orthogonality

TOTBWF
authored and
plt-amy
committed
refactor: move OFS's out of Cat.Morphism.Factorisation

TOTBWF
authored and
plt-amy
committed
refactor: live with the consequences of our refactors

TOTBWF
authored and
plt-amy
committed
def: some useful factorisation lemmas

TOTBWF
authored and
plt-amy
committed
refactor: refactor Regular categories a bit

TOTBWF
authored and
plt-amy
committed
refactor: move Monos/Epis/Isos to Cat.Morphism

TOTBWF
authored and
plt-amy
committed
refactor: projectivity via Lifts

TOTBWF
authored and
plt-amy
committed
refactor: more refactor fallout

TOTBWF
authored and
plt-amy
committed
refactor: injective objects via Lifts

TOTBWF
authored and
plt-amy
committed
fix: sort imports

TOTBWF
authored and
plt-amy
committed
prose: indentation fixes

TOTBWF
authored and
plt-amy
committed
prose: hide Lifts-against class from the innocent reader

TOTBWF
authored and
plt-amy
committed
fix: Orthogonal is now exported by Lifts

TOTBWF
authored and
plt-amy
committed
fixup katex
plt-amy
committed
fixup
plt-amy
committed
prose: fix typo

authored and
plt-amy
committed
prose: tidy up ofs prose

TOTBWF
authored and
plt-amy
committed
chore: more consistent names for composites of strong monos/epis

TOTBWF
authored and
plt-amy
committed
prose: redo prose for OFSs, rename to use left/right instead E/M

TOTBWF
authored and
plt-amy
committed
defn: factorisation in a regular category is an ofs

TOTBWF
authored and
plt-amy
committed
prose: fix diagrams/prose for lifts

TOTBWF
authored and
plt-amy
committed
prose: diagram transpositions, standardize midpoint of factorisation

TOTBWF
authored and
plt-amy
committed
prose: missed some m's, flip arrow

TOTBWF
authored and
plt-amy
committed
chore: styling
plt-amy
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lifting Refactor#555

Lifting Refactor#555
plt-amy merged 27 commits intomainfrom
lifting-refactor

Commits on Sep 1, 2025

def: classes of morphisms

chore: rework arrow category

def: general lifting machinery

refactor: use a class-based approach for orthogonality

refactor: move OFS's out of Cat.Morphism.Factorisation

refactor: live with the consequences of our refactors

def: some useful factorisation lemmas

refactor: refactor Regular categories a bit

refactor: move Monos/Epis/Isos to Cat.Morphism

refactor: projectivity via Lifts

refactor: more refactor fallout

refactor: injective objects via Lifts

fix: sort imports

prose: indentation fixes

prose: hide Lifts-against class from the innocent reader

fix: Orthogonal is now exported by Lifts

fixup katex

fixup

prose: fix typo

prose: tidy up ofs prose

chore: more consistent names for composites of strong monos/epis

prose: redo prose for OFSs, rename to use left/right instead E/M

defn: factorisation in a regular category is an ofs

prose: fix diagrams/prose for lifts

prose: diagram transpositions, standardize midpoint of factorisation

prose: missed some m's, flip arrow

chore: styling