Blake Shaw schreef op wo 15-06-2022 om 21:40 [+0000]: > On the contrary, lets say I'm writing an intro book on CT. If I'm > demonstrating something trivial, say the initial object, I'm not > going to refer to it as "an initial-like object" for the sake of > generality. Neither does Guix? If you're in a context where only the basic object (in this case, your demonstration the initial object) is used, just talk about the basic object. But in a later section where you generalize things to ‘initial-like objects’ (whatever that would be in CT, I don't know any CT), you talk about ‘initial-like objects’, not ‘initial object and initial-like objects’. For an example from another domain, consider groups in algebra. In group theory, we have e.g. the fundamental theorem on homomorphisms. Wikipedia formulates this as: Given two groups G and H and a group homomorphism f : G → H, let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K (where G/K is the quotient group of G by K). If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ. An equivalent statement could be made by replacing ‘given a group’ by ‘given an Abelian group or a group’: Given two Abelian groups or groups G and H and a group homomorphism f : G → H, let K be an Abelian normal subgroup or normal subgroup in G and φ the natural surjective homomorphism G → G/K (where G/K is the quotient group of G by K). If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.’ But why do such a pointless thing, wouldn't just talking about groups instead of ‘Abelian groups or groups’ be much simpler? TBC: here ‘file-like object’ ≃ ‘group’ and ‘file’ = ‘Abelian group’. Greetings, Maxime.