Yoneda lemma using 0-groupoids #1527
Annotations
10 warnings
|
theories/Basics/Equivalences.v#L104
adj is declared opaque (Qed) but this is not fully respected inside
|
|
theories/Colimits/Pushout.v#L281
esp1_beta_pglue is declared opaque (Qed) but this is not fully
|
|
theories/Colimits/Pushout.v#L300
esp2_beta_pglue is declared opaque (Qed) but this is not fully
|
|
theories/Categories/LaxComma/Core.v#L178
This inductive will be minimized to Set even though Universe
|
|
theories/Categories/LaxComma/Core.v#L213
This inductive will be minimized to Set even though Universe
|
|
theories/Classes/implementations/peano_naturals.v#L22
natpaths_symm is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L586
f_preserves_0 is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L589
f_preserves_1 is declared opaque (Qed) but this is not fully
|
|
theories/Classes/implementations/peano_naturals.v#L596
f_S is declared opaque (Qed) but this is not fully respected inside
|
|
theories/Classes/implementations/peano_naturals.v#L606
f_preserves_plus is declared opaque (Qed) but this is not fully
|
The logs for this run have expired and are no longer available.
Loading