capitalization of morphism properties?

Stream: Infinity-Cosmos

[Emily Riehl]

@Nima Rasekh and @Matej Penciak just sent us a pull request which includes a definition of the morphism property of being an isofibration:

https://github.com/emilyriehl/infinity-cosmos/pull/36

I'll leave a few comments there but I had a question for @Jack McKoen and others: should morphism properties be capitalized?

In our current repository (under SimplicialSet/MorphismProperty) we have:

/-- an inductive type defining boundary inclusions as a class of morphisms. Used to take advantage
  of the `MorphismProperty` API. -/
inductive BoundaryInclusion : {X Y : SSet} → (X ⟶ Y) → Prop
  | mk n : BoundaryInclusion (boundaryInclusion n)

/-- The class of all boundary inclusions. -/
def BoundaryInclusions : MorphismProperty SSet := fun _ _ p ↦ BoundaryInclusion p

/-- a morphism of simplicial sets is a trivial fibration if it has the right lifting property wrt
  every boundary inclusion  `∂Δ[n] ⟶ Δ[n]`. -/
def trivialFibration : MorphismProperty SSet := fun _ _ p ↦ BoundaryInclusions.rlp p

The first term is an inductively defined type family, so definitely should be capitalized. What about the other terms?

[Nima Rasekh]

Emily Riehl said:

Nima Rasekh and Matej Penciak just sent us a pull request which includes a definition of the morphism property of being an isofibration:

https://github.com/emilyriehl/infinity-cosmos/pull/36

I'll leave a few comments there but I had a question for Jack McKoen and others: should morphism properties be capitalized?

In our current repository (under SimplicialSet/MorphismProperty) we have:

/-- an inductive type defining boundary inclusions as a class of morphisms. Used to take advantage
  of the `MorphismProperty` API. -/
inductive BoundaryInclusion : {X Y : SSet} → (X ⟶ Y) → Prop
  | mk n : BoundaryInclusion (boundaryInclusion n)

/-- The class of all boundary inclusions. -/
def BoundaryInclusions : MorphismProperty SSet := fun _ _ p ↦ BoundaryInclusion p

/-- a morphism of simplicial sets is a trivial fibration if it has the right lifting property wrt
  every boundary inclusion  `∂Δ[n] ⟶ Δ[n]`. -/
def trivialFibration : MorphismProperty SSet := fun _ _ p ↦ BoundaryInclusions.rlp p

The first term is an inductively defined type family, so definitely should be capitalized. What about the other terms?

This is a good point. We were also not absolutely sure about the capitalization and just tried to follow what @Jack McKoen had already done.

[Jack McKoen]

I think morphism properties should not be capitalised (based on some examples I just checked in mathlib). Maybe it should be lowerCamelCase based on https://leanprover-community.github.io/contribute/naming.html

[Jack McKoen]

@Adam Topaz might be a better person to ask about naming conventions

[Kevin Buzzard]

Although the finer points of the naming convention are still a mystery to me, one thing which has finally sunk in is that the first letter is capital for types and small for terms.

[Adam Topaz]

Since morphisms properties are essentially parameterized props, they should probably be UpperCamelCase, similarly to named props like docs#IsOpen

[Jack McKoen]

The first example I thought of was docs#CategoryTheory.MorphismProperty.monomorphisms

[Jack McKoen]

I guess the naming conventions will remain a mystery to me as well

[Adam Topaz]

Jack McKoen said:

I guess the naming conventions will remain a mystery to me as well

Same here :-/

[Adam Topaz]

Note that terms of docs#CategoryTheory.MorphismProperty are props, and thus should be UpperCamelCase with my understanding of the naming rules

[Adam Topaz]

But then again, you can think of IsOpen as the set of open sets, so that would be lowerCamelCase. Ok. Now I’m confused again

[Mario Carneiro]

I believe the rule we ended on was that if the type is Prop or a bunch of arrows ending in Prop then it should be capitalized, but not if the type is something which definitionally unfolds to such (the main example at the time of this was Set A), these should be lowercase like other data values

[Emily Riehl]

For now we've decided that terms of type MorphismProperty are in UpperCamelCase, but this can be changed if our interpretation of the convention is incorrect.

I now have a separate question: should the morphism property that defines, e.g., trivial fibrations be called IsTrivialFibration?

[Emily Riehl]

I noticed this because we currently have

def IsoFibration : MorphismProperty QCat := fun _ _ p ↦ InnerHornIsoInclusions.rlp p

but also

/-- A `PreInfinityCosmos` is a simplicially enriched category whose hom-spaces are quasi-categories
and whose morphisms come equipped with a special class of isofibrations.-/
class PreInfinityCosmos extends SimplicialCategory K where
  [has_qcat_homs : ∀ {X Y : K}, SSet.Quasicategory (EnrichedCategory.Hom X Y)]
  IsIsoFibration : MorphismProperty K

where IsIsoFibration is the name originally suggested by @Mario Carneiro.

[Jack McKoen]

Since a MorphismProperty is meant to be a class of morphisms, I think their names should not include verbs (e.g. Monomorphisms vs IsMonomorphism). I think this is just a matter of preference though.

[Mario Carneiro]

I believe this is normally used like φ.IsIsoFibration which is why I gave it that kind of naming