OAI/Algebra/FinitisticAsymmetry/Derived/DerivedSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.DerivedSupport.derivedHomotopyCofanIsColimit line 16
2. def OAI.LittleFinitistic.DerivedSupport.derivedCofanIsColimit line 23
3. def OAI.LittleFinitistic.DerivedSupport.derivedSumIsColimit line 60
4. lemma OAI.LittleFinitistic.DerivedSupport.prop_derived_sum line 63
5. instance OAI.LittleFinitistic.DerivedSupport.derivedHasCoproducts line 68