Code

Pullback properties#449

Code

Merged

JacquesCarette merged 5 commits intoagda:masteragda/agda-categories:masterfrom frederikgebert:pullback-propertiesfrederikgebert/agda-categories:pullback-propertiesCopy head branch name to clipboardFeb 20, 2025

+93

Commits

Commits on Jan 31, 2025

• added pasting law for pullbacks

  

  Frederik Gebert

  committed
  2985e55

  Copy full SHA for 2985e55

Commits on Feb 6, 2025

• Fixed typo.

  

  Frederik Gebert

  committed
  496aed8

  Copy full SHA for 496aed8

• Omitted implicit arguments. Shortened proofs using push and pull.

  

  Frederik Gebert

  committed
  6fed915

  Copy full SHA for 6fed915

• Shortened proof by removing unnecessary definitions.

  

  Frederik Gebert

  committed
  7532da2

  Copy full SHA for 7532da2

• Move intermediate equations to definitions that use them.

  Show description for 7d87911
  

  Frederik Gebert

  committed
  7d87911

  Copy full SHA for 7d87911