Code

Rewrite rules for pushouts#1021

Code

Merged

VojtechStep merged 33 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:rewrite-pushoutfredrik-bakke/agda-unimath:rewrite-pushoutCopy head branch name to clipboardApr 19, 2024

+1,316-183

Commits

Commits on Feb 6, 2024

• add rewriting file

  fredrik-bakke

  committed
  8347f78

  Copy full SHA for 8347f78

• stop :(

  fredrik-bakke

  committed
  06950c7

  Copy full SHA for 06950c7

Commits on Apr 15, 2024

• The recursion principle of pushouts

  fredrik-bakke

  committed
  29a53f6

  Copy full SHA for 29a53f6

• Erasing equality primitive

  fredrik-bakke

  committed
  fc236be

  Copy full SHA for fc236be

• projections for htpy-eq-cocone

  fredrik-bakke

  committed
  ca671fe

  Copy full SHA for ca671fe

• Dependent cocones on constant type families

  fredrik-bakke

  committed
  81dfdfd

  Copy full SHA for 81dfdfd

• change pushout postulates

  fredrik-bakke

  committed
  aa13b23

  Copy full SHA for aa13b23

• add module rewriting-pushouts

  fredrik-bakke

  committed
  3e3b60b

  Copy full SHA for 3e3b60b

• Merge branch 'master' into rewrite-pushout

  fredrik-bakke

  authored
  de131c4

  Copy full SHA for de131c4

• computing with dependent cocones on constant type families

  fredrik-bakke

  committed
  2eb7ed0

  Copy full SHA for 2eb7ed0

• redefine cogap so it computes with rewrite rules

  fredrik-bakke

  committed
  f59f390

  Copy full SHA for f59f390

• Idea rewriting-pushouts

  fredrik-bakke

  committed
  8662b15

  Copy full SHA for 8662b15

• pre-commit

  fredrik-bakke

  committed
  72dc2e3

  Copy full SHA for 72dc2e3

Commits on Apr 16, 2024

• Naturality of transport in constant type families

  fredrik-bakke

  committed
  88686b0

  Copy full SHA for 88686b0

• nitpick dependent-identifications

  fredrik-bakke

  committed
  f2e276e

  Copy full SHA for f2e276e

• nitpick transport-along-identifications

  fredrik-bakke

  committed
  850a9f8

  Copy full SHA for 850a9f8

• Computing with the characterization of identifications of dependent cocones on constant type families

  fredrik-bakke

  committed
  b0044db

  Copy full SHA for b0044db

• Dependent homotopies of dependent cocones

  fredrik-bakke

  committed
  f88cb2a

  Copy full SHA for f88cb2a

• reflexive-htpy-cocone -> refl-htpy-cocone

  fredrik-bakke

  committed
  86b1582

  Copy full SHA for 86b1582

• is-retraction-ind-induction-principle-pushout

  fredrik-bakke

  committed
  ba8ae0b

  Copy full SHA for ba8ae0b

• compute-glue-cogap by hand

  fredrik-bakke

  committed
  fd189bf

  Copy full SHA for fd189bf

• elaborate

  fredrik-bakke

  committed
  7160b93

  Copy full SHA for 7160b93

• Merge branch 'master' into rewrite-pushout

  fredrik-bakke

  authored
  b335744

  Copy full SHA for b335744

• fixes

  fredrik-bakke

  committed
  c736c04

  Copy full SHA for c736c04

• refactoring definitions joins of types

  fredrik-bakke

  committed
  7450599

  Copy full SHA for 7450599

Commits on Apr 17, 2024

• idea rewriting

  fredrik-bakke

  committed
  6aaae16

  Copy full SHA for 6aaae16

• standard* identity relation

  fredrik-bakke

  committed
  ba8bed8

  Copy full SHA for ba8bed8

• headers dependent cocones

  fredrik-bakke

  committed
  b6e2b5c

  Copy full SHA for b6e2b5c

• explain computation rules for pushouts

  fredrik-bakke

  committed
  6fa81af

  Copy full SHA for 6fa81af

• Merge branch 'master' into rewrite-pushout

  fredrik-bakke

  authored
  9c051c6

  Copy full SHA for 9c051c6

Commits on Apr 19, 2024

• review comments

  fredrik-bakke

  committed
  f99e553

  Copy full SHA for f99e553

• assoc ap inv assoc business

  fredrik-bakke

  committed
  001ffc6

  Copy full SHA for 001ffc6

• Merge branch 'master' into rewrite-pushout

  fredrik-bakke

  authored
  7c48dab

  Copy full SHA for 7c48dab