capitals in Logic.Equiv.Defs file

Stream: mathlib4

[Kevin Buzzard]

We have Equiv.unique in mathlib4 and it's a def. Should it be Equiv.Unique? Same question for Equiv.symm, Equiv.trans, Equiv.decidableEq, Equiv.inhabited, Equiv.equivCongr, Equiv.permCongr, Equiv.plift... (all defs but have been decapitalised).

[Mario Carneiro]

I think so... some of them might be theorem-cased but none of them should be type-cased because they aren't types

[Mario Carneiro]

it sounds like they should all be def-cased though

[Kevin Buzzard]

There are tons of these, also in Logic.Equiv.Basic. The autoporter has called α × Empty ≃ Empty prodEmpty but it's a def so I'm changing it to ProdEmpty. In particular the conventions for Logic.Equiv.Basic (which I'm porting) are going to be different to those in Logic.Equiv.Defs (which is already ported) at this rate (unless I change Logic.Equiv.Devs too). @Scott Morrison do you have an opinion on this?

[Mario Carneiro]

no no, mathport is right here

[Mario Carneiro]

ProdEmpty would be if it was defining a type, i.e. something whose type is Type u or Prop

[Mario Carneiro]

for example:

def Equiv.Rel (e : A ~= B) (x : A) (y : B) : Prop := e x = y

[Kevin Buzzard]

Oh I'd misunderstood! Terms which are not types are lowerCamelCase!

[Mario Carneiro]

for something like Equiv.symm, it should be def-cased (lowerCamelCase) because it is constructing "data", i.e. something which is not a proposition:

def Equiv.symm (e : A ~= B) : B ~= A := sorry

[Mario Carneiro]

and for completeness: things which construct elements of a proposition are theorem-cased (snake_case), containing name components from the definitions it uses:

def Equiv.symm_symm (e : A ~= B) : e.symm.symm = e := sorry

[Yakov Pechersky]

Mario Carneiro said:

it sounds like they should all be def-cased though

I see, I was confused by Kevin calling it a lemma, while it's really an Equiv term.

[Kevin Buzzard]

def pemptyProd (α : Type _) : PEmpty × α ≃ PEmpty :=

So the rules are that this should be decapitalised because it's a term-not-a-type, and I think pEmpty looks weird so I'm going for this. Have I finally got it right?

[Kevin Buzzard]

def boolEquivPUnitSumPUnit : Bool ≃ Sum PUnit.{u + 1} PUnit.{v + 1} :=

The autoporter gave me boolEquivPunitSumPunit