Pullback properties#449

Merged

JacquesCarette merged 5 commits intoagda:masterfrom

frederikgebert:pullback-properties

Feb 20, 2025

Commits on Jan 31, 2025

added pasting law for pullbacks
Frederik Gebert
committed

Commits on Feb 6, 2025

Fixed typo.
Frederik Gebert
committed
Omitted implicit arguments. Shortened proofs using push and pull.
Frederik Gebert
committed
Shortened proof by removing unnecessary definitions.
Frederik Gebert
committed
Move intermediate equations to definitions that use them.
Frederik Gebert
committed