Duskin's Monadicity Theorem #76
Conversation
| @@ -0,0 +1,203 @@ | |||
| ```agda | |||
There was a problem hiding this comment.
At the risk of being a terrible person, do these two pages need a description: frontmatter field?
| Reflects-colimit K = is-colimit (F F∘ Dia) (F-map-cocone K) → is-colimit Dia K | ||
| ``` | ||
|
|
||
| # Uniqueness |
There was a problem hiding this comment.
We should finish fleshing this section out to line up with the proofs for limits. However, I just need this one result for right now, so I'll circle back around at the end of this PR.
| ``` | ||
| --> | ||
|
|
||
| If the universal map $L \to K$ between coapexes of some colimit is |
There was a problem hiding this comment.
either "coapices" or "nadirs" (if you want to change the field name), but definitely not coapexes
There was a problem hiding this comment.
We should change the wording in Limits.Base as well then!
There was a problem hiding this comment.
You are correct. That's a bit embarrassing
| We also have a dual theorem for colimits. | ||
|
|
||
| ```agda | ||
| conservative-reflects-colimits |
There was a problem hiding this comment.
I've done this proof directly to avoid the subst; we should probably do the same for the reflection of limits.
There was a problem hiding this comment.
If you open an issue and assign it to me I'll take care of it when I'm done with work today
plt-amy
added
enhancement
Description
This PR proves Duskin's Monadicity Theorem, and also provides the associated machinery. This closes #74.
I'm also proving the version found in the Handbook of Categorical Algebra
Checklist