feat(CategoryTheory): effectiveness of descent #24434
+4,052
−66
Open
Annotations
11 errors and 10 warnings
|
Mathlib/CategoryTheory/Bicategory/Adjunction/BaseChange.lean#L23
@CategoryTheory.CommSq.toLoc is a def, should be lemma/theorem
|
|
Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean#L217
@CategoryTheory.IsPullback.exists_lift is a def, should be lemma/theorem
|
|
Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean#L445
@CategoryTheory.IsPushout.exists_desc is a def, should be lemma/theorem
|
|
Mathlib/CategoryTheory/Bicategory/Adjunction/Adj.lean#L376
@CategoryTheory.Bicategory.Adj.forget₂ definition missing documentation string
|
|
Mathlib/CategoryTheory/Bicategory/Adjunction/BaseChange.lean#L23
@CategoryTheory.CommSq.toLoc definition missing documentation string
|
|
Mathlib/CategoryTheory/Bicategory/Adjunction/BaseChange.lean#L233
@CategoryTheory.Pseudofunctor.baseChange definition missing documentation string
|
|
Mathlib/CategoryTheory/Bicategory/Opposite.lean#L37
@CategoryTheory.Bicategory.Opposite.associator definition missing documentation string
|
|
Mathlib/CategoryTheory/Bicategory/Opposite.lean#L43
@CategoryTheory.Bicategory.Opposite.leftUnitor definition missing documentation string
|
|
Mathlib/CategoryTheory/Bicategory/Opposite.lean#L48
@CategoryTheory.Bicategory.Opposite.rightUnitor definition missing documentation string
|
|
Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean#L217
@CategoryTheory.IsPullback.exists_lift definition missing documentation string
|
|
|
|
Mathlib/CategoryTheory/Sites/Descent/IsStack.lean#L159
declaration uses 'sorry'
|
|
|
|
Mathlib/CategoryTheory/Sites/Descent/ModuleCat.lean#L5
The module doc-string for a file should be the first command after the imports.
|
|
|
|
Mathlib/CategoryTheory/Sites/Descent/ModuleCat.lean#L5
The module doc-string for a file should be the first command after the imports.
|
|
|
|
Mathlib/CategoryTheory/Sites/Descent/ModuleCat.lean#L5
The module doc-string for a file should be the first command after the imports.
|
|
Mathlib/CategoryTheory/Sites/Descent/ModuleCat.lean#L13
declaration uses 'sorry'
|
|
|
|
Mathlib/CategoryTheory/Sites/Descent/ModuleCat.lean#L5
The module doc-string for a file should be the first command after the imports.
|
The logs for this run have expired and are no longer available.
Loading