diff --git a/src/hott/01-paths.rzk.md b/src/hott/01-paths.rzk.md index b1c4ce42..1fd50a91 100644 --- a/src/hott/01-paths.rzk.md +++ b/src/hott/01-paths.rzk.md @@ -969,8 +969,92 @@ The following is the same as above but with alternating arguments. The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the -equivalence between the right side of the square and a particular zig-zag of -paths. +equivalence between the right side of the square (in blue) and a particular +zig-zag of paths, the red zig-zag. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ```rzk #def eq-top-cancel-commutative-square