Skip to content

defn: final functors induce equivalence of cocone categories#639

Merged
plt-amy merged 3 commits into
the1lab:mainfrom
ncfavier:final-functor-cocones
Jul 15, 2026
Merged

defn: final functors induce equivalence of cocone categories#639
plt-amy merged 3 commits into
the1lab:mainfrom
ncfavier:final-functor-cocones

Conversation

@ncfavier

@ncfavier ncfavier commented Jun 29, 2026

Copy link
Copy Markdown
Member

Also closes #78 and #81.

@Lavenza

Lavenza commented Jun 29, 2026

Copy link
Copy Markdown
Member

@ncfavier ncfavier force-pushed the final-functor-cocones branch from cb49a4c to 0ff27d9 Compare June 30, 2026 13:52
@ncfavier ncfavier marked this pull request as ready for review June 30, 2026 13:52
Comment thread src/Cat/Diagram/Colimit/Cocone.lagda.md Outdated
@ncfavier ncfavier force-pushed the final-functor-cocones branch from 0ff27d9 to 3f8842e Compare June 30, 2026 14:10
ncfavier added 3 commits July 15, 2026 09:24
Strengthen the results about final functors a bit: a final functor induces
an equivalence between categories of cocones, which automatically
preserves initial objects (i.e. colimits).
@plt-amy plt-amy force-pushed the final-functor-cocones branch from 3f8842e to 89d30e5 Compare July 15, 2026 12:24
@plt-amy plt-amy enabled auto-merge (rebase) July 15, 2026 12:31
@plt-amy plt-amy merged commit 484a970 into the1lab:main Jul 15, 2026
3 checks passed
@ncfavier ncfavier deleted the final-functor-cocones branch July 15, 2026 12:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Prove that all of our colimit diagrams are actually colimits

3 participants