pasting lemmas for cartesian squares

[TashiWalde]

1) right cancellation of equivalence property (gf, g equiv => f equiv)

2.1) defined homotopy cartesian squares 2.2) pasting of homotopy cartesian squares 2.3) right cancellation of homotopy cartesian squares

[fizruk]

Looks good to me!