[Merged by Bors] - style: CoeFun for PFunctor.Obj & MvPFunctor.Obj
#7526
Conversation
Komyyy
commented
Oct 5, 2023
Komyyy
commented
Komyyy
added
awaiting-review
Komyyy
changed the title
CoeFun for PFunctor.Obj & MvPFunctor.ObjCoeFun for PFunctor.Obj & MvPFunctor.Obj
leanprover-community-mathlib4-bot
added
the
merge-conflict
Komyyy
removed
the
merge-conflict
| @@ -38,122 +38,125 @@ open MvFunctor (LiftP LiftR) | |||
| variable {n m : ℕ} (P : MvPFunctor.{u} n) | |||
|
|
|||
| /-- Applying `P` to an object of `Type` -/ | |||
| @[coe] | |||
There was a problem hiding this comment.
What does the coe attribute do? Since we also have the explicit CoeFun instance a few lines lower
There was a problem hiding this comment.
The function with a coe attribute is printed as ↑.
| id_map := @id_map _ P | ||
| comp_map := @comp_map _ P | ||
|
|
||
| /-- Constant functor where the input object does not affect the output -/ | ||
| def const (n : ℕ) (A : Type u) : MvPFunctor n := | ||
| def Const (n : ℕ) (A : Type u) : MvPFunctor n := |
There was a problem hiding this comment.
Technically, MvPFunctor is a structure, so the naming convention calls for this definition to be lowerCamelCase.
Then again, the point of this PR is to pretend that MvPFunctor is a Type-valued function, in which case we do UpperCamelCase.
I support this change, since it improves consistency between MvPFunctor and MvFunctor, but still I think we should discuss on a Zulip thread whether we want to treat structures with a CoeFun instance as if they were function types, and if so, to document this exception in the naming convention document.
There was a problem hiding this comment.
From this discussion, I decided to use lowerCamelCase.
| @@ -39,37 +39,41 @@ namespace PFunctor | |||
| instance : Inhabited PFunctor := | |||
| ⟨⟨default, default⟩⟩ | |||
|
|
|||
| variable (P : PFunctor) {α β : Type u} | |||
| variable (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} | |||
There was a problem hiding this comment.
| variable (P : PFunctor.{u}) {α : Type v₁} {β : Type v₂} | |
| variable (P : PFunctor.{u}) {α β : Type*} |
I think this should have the same effect, but is a bit more succinct
There was a problem hiding this comment.
I want to fix the order of universe variables as u, v₁, v₂.
With Type*, the order of universe variables becomes v₁, v₂, u.
| def Obj (α : Type*) := | ||
| Σx : P.A, P.B x → α | ||
| @[coe] | ||
| def Obj (α : Type v) := |
There was a problem hiding this comment.
I'm curious, what is your motivation for changing Type* to explicitly giving the universe variable?
There was a problem hiding this comment.
I want to fix the order of universe variables as u, v.
With Type*, the order of universe variables becomes v, u.
leanprover-community-mathlib4-bot
added
the
merge-conflict
Komyyy
removed
the
merge-conflict
There was a problem hiding this comment.
bors d=@digama0
As this is largely stylistic, I'll let Mario decide since they were involved in the initial development.
|
✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
CoeFun for PFunctor.Obj & MvPFunctor.ObjCoeFun for PFunctor.Obj & MvPFunctor.Obj
