CoproductHomotopy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.coproductHomotopyHom line 17
theorem OAI.DerivedBar.ι_coproductHomotopyHom line 21
def OAI.DerivedBar.coproductHomotopy line 27
Source documentation
Homotopies out of the summands assemble through the actual degreewise coproduct, so equality after the homotopy quotient is still detected summandwise.
```
def coproductHomotopy : Homotopy f g where
…
```
def OAI.DerivedBar.homotopyCoconeLift line 53
def OAI.DerivedBar.homotopyCoproductIsColimit line 59
Source documentation
The actual coproduct survives the homotopy quotient. Both existence and uniqueness are proved; the latter assembles the component homotopies.
```
def homotopyCoproductIsColimit : IsColimit ((Q).mapCocone s) where
…
```