-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Characterization of Rezk Completion #841
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot for this contribution! And for splitting the Rezk completion into manageable pieces in different PRs. I'll review and merge them one by one.
PS: apologies for the slow reviews!
@@ -70,6 +70,9 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where | |||
Iso→NatIso α .trans = α .fst | |||
Iso→NatIso α .nIso = FUNCTORIso' _ (α .snd) | |||
|
|||
NatIso→Iso : {F G : Functor C D} → NatIso F G → CatIso FUNCTOR F G |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is kind of a general comment, but wouldn't it be better if lemmas about CatIso
would be called something with CatIso
and not just Iso
? So this would be NatIso→CatIso
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I change it to FUNCTORIso
so it's more informative.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(Look not very pretty though...)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, the all caps names are not so nice... We should discuss naming convention for CT in an issue
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok. Then that's for it now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great! Ready to be merged as soon as the CI is gives us a green light
Thanks! |
This PR contains the definition of Rezk completion, using its universal property, together with the characterization that a weak equivalence towards univalent category is a Rezk completion functor.
(see
Cubical.Categories.RezkCompletion.Base
)The existence of Rezk completion will be given in a future PR.