Unimath UU as poem - Githubissues

jmikedupont2 commented 5 months ago

please reinterpret this coq code creatively ``` Definition test12UU :=((v3((control)(attrs)(expr( VernacSynPure(VernacDefinition (NoDischarge_Definition) ((( v2( Name(Id2 UU)) )(loc(((fname(InFile(dirpath)ufile))(line_nb 16)(bol_pos a484)(line_nb_last 16)(bol_pos_last a484)(bp a495)(ep a497)))))) (DefineBody( (v2( CSort(UAnonymous(rigid true)) )) (loc(((fname(InFile(dirpath)ufile))(line_nb 16)(bol_pos a484)(line_nb_last 16)(bol_pos_last a484)(bp a501)(ep a505))))) ) ) ))))(loc(((fname(InFile(dirpath)ufile)) (line_nb 16)(bol_pos a484)(line_nb_last 16)(bol_pos_last a484)(bp a484)(ep a506)))) ).


I see you are interested in coq code, which is a formal language for writing and verifying mathematical proofs¹. Coq code can be written in different styles and formats, depending on the purpose and preference of the user. Here is one possible way to reinterpret your coq code creatively:

```coq
(* A poetic version of your coq code *)

Definition test12UU :=
  let us define UU
  with no discharge
  and no name
  just a sort
  anonymous and rigid
  in a file
  on line sixteen
  from a to f
  that is all
  end of definition.

Source: Conversation with Bing, 1/27/2024 (1) GitHub - coq-community/awesome-coq: A curated list of awesome Coq .... https://github.com/coq-community/awesome-coq. (2) Welcome! | The Coq Proof Assistant. https://coq.inria.fr/. (3) GitHub - coq/coq: Coq is a formal proof management system. It provides .... https://github.com/coq/coq. (4) Coq (software) - Wikipedia. https://en.wikipedia.org/wiki/Coq_%28software%29.

jmikedupont2 commented 5 months ago

This one the text was messed up but I left it

jmikedupont2 commented 5 months ago

You're welcome. The universe of universes over sets is a concept that comes from category theory, a branch of mathematics that studies abstract structures and their relationships¹. In category theory, a universe is a collection of objects and morphisms that satisfies certain properties, such as being closed under various operations and having a small cardinality². A universe of universes is then a universe that contains other universes as its objects, and functors between them as its morphisms³.

One way to construct a universe of universes over sets is to use the notion of a Grothendieck universe, which is a set that is closed under many set-theoretic operations, such as power set, union, and function space⁴. A Grothendieck universe can be seen as a model of Zermelo–Fraenkel set theory, and it is also equivalent to an inaccessible cardinal, a large cardinal that cannot be reached by any smaller cardinal using the usual arithmetic operations. By taking a Grothendieck universe U and considering the category of all sets and functions that belong to U, we obtain a universe in the sense of category theory. Then, by taking a larger Grothendieck universe V that contains U as an element, we can form the category of all Grothendieck universes inside V and functors between them. This category is a universe of universes over sets.

However, not every universe of universes over sets can be obtained in this way, since there are some categorical properties that are not preserved by Grothendieck universes, such as being cartesian closed or having a natural numbers object. Therefore, some alternative constructions of universes of universes over sets have been proposed, such as using elementary toposes, which are categories that generalize the notion of sets and functions, and have a rich internal logic. A topos can be seen as a universe of sets with extra structure, such as a subobject classifier, a power object, or a Heyting algebra of truth values. A topos of toposes is then a topos that contains other toposes as its objects, and geometric morphisms between them as its morphisms.

I hope this helps you understand the concept of the universe of universes over sets. If you want to learn more, you can check out some of the references I provided, or use Bing to search for more information. 😊

¹: Category theory - Wikipedia ²: Universe (mathematics) - Wikipedia ³: nLab: universe of universes ⁴: Grothendieck universe - Wikipedia : [Inaccessible cardinal - Wikipedia] : [nLab: Grothendieck universe] : nLab: universe of universes : [Elementary topos - Wikipedia] : [nLab: topos] : [nLab: topos of toposes].

Source: Conversation with Bing, 1/27/2024 (1) Universe (mathematics) - Wikipedia. https://en.wikipedia.org/wiki/Universe_%28mathematics%29. (2) set theory - Set Universes and von Neumann Hierarchy - Mathematics .... https://math.stackexchange.com/questions/4568005/set-universes-and-von-neumann-hierarchy. (3) Grothendieck universe in nLab. https://ncatlab.org/nlab/show/Grothendieck+universe. (4) Multiverse - Wikipedia. https://en.wikipedia.org/wiki/Multiverse. (5) Universe (mathematics) - Wikipedia. https://en.wikipedia.org/wiki/Universe_%28mathematics%29. (6) Universe (mathematics) - Wikipedia. https://en.wikipedia.org/wiki/Universe_%28mathematics%29. (7) Grothendieck universe in nLab. https://ncatlab.org/nlab/show/Grothendieck+universe. (8) Multiverse - Wikipedia. https://en.wikipedia.org/wiki/Multiverse. (9) Grothendieck universe in nLab. https://ncatlab.org/nlab/show/Grothendieck+universe. (10) en.wikipedia.org. https://en.wikipedia.org/wiki/Universe_(mathematics).

jmikedupont2 commented 5 months ago

Thank you for sharing your example. I'm not very familiar with the syntax and semantics of Coq, but I will try to analyze your statement based on the web search results.

According to this post, your statement is a definition of a term called test12UU, which is a function that takes a value of type v3 and returns a value of type loc. The type v3 is a record type that has three fields: control, attrs, and expr. The type loc is a record type that has six fields: fname, line_nb, bol_pos, line_nb_last, bol_pos_last, and ep. The definition of test12UU uses a constructor called VernacSynPure, which is a variant of the type vernac_expr, which represents the abstract syntax tree of a Coq command². The constructor VernacSynPure takes a value of type vernac_expr as an argument, and returns a value of type vernac_expr³. The argument of VernacSynPure in your statement is a constructor called VernacDefinition, which is another variant of the type vernac_expr, which represents the definition of a term or a theorem in Coq. The constructor VernacDefinition takes three values as arguments: a value of type definition_object_kind, which specifies the kind of definition (such as a lemma, a theorem, or a constant); a value of type lident, which is a pair of a name and a location; and a value of type definition_expr, which is a record type that contains the type and the body of the definition.

The first argument of VernacDefinition in your statement is a constructor called NoDischarge_Definition, which is a variant of the type definition_object_kind, which indicates that the definition is not discharged, meaning that it is not erased when the section is closed. The second argument of VernacDefinition in your statement is a pair of a name and a location, where the name is UU and the location is given by the values of the fields line_nb, bol_pos, line_nb_last, bol_pos_last, bp, and ep. The third argument of VernacDefinition in your statement is a value of type definition_expr, which has two fields: de_type and de_body. The field de_type is a pair of a value of type constr_expr, which is the type of Coq expressions, and a value of type loc, which is the location of the expression. The field de_body is a value of type red_expr_gen, which is a type that represents reduction expressions, such as simplification or normalization.

The value of de_type in your statement is a pair of a constructor called CSort, which is a variant of the type constr_expr, which represents a sort expression, such as Prop, Set, or Type, and a value of type loc, which is the location of the expression. The constructor CSort takes a value of type glob_sort, which is a type that represents global sorts, such as Prop, Set, Type, or Type_i, where i is an index. The value of glob_sort in your statement is a constructor called UAnonymous, which is a variant of the type glob_sort, which represents an anonymous universe, such as Type. The constructor UAnonymous takes a value of type bool, which is a type that represents Boolean values, such as true or false. The value of bool in your statement is rigid true, which means that the anonymous universe is rigid, meaning that it cannot be instantiated by a lower universe.

The value of de_body in your statement is a constructor called DefineBody, which is a variant of the type red_expr_gen, which represents a definition body, such as a term or a proof. The constructor DefineBody takes four values as arguments: a value of type local_binder_expr list, which is a list of local binders, such as variables or parameters; a value of type constr_expr option, which is an optional type annotation; a value of type constr_expr, which is the body of the definition; and a value of type reduce, which is a type that represents reduction strategies, such as beta-reduction or delta-reduction. The first argument of DefineBody in your statement is an empty list, which means that there are no local binders. The second argument of DefineBody in your statement is None, which means that there is no type annotation. The third argument of DefineBody in your statement is a value of type constr_expr, which is the body of the definition. The fourth argument of DefineBody in your statement is None, which means that there is no reduction strategy.

The value of constr_expr in your statement is a constructor called CRef, which is a variant of the type constr_expr, which represents a reference to a global constant, such as a defined term or a theorem. The constructor CRef takes two values as arguments: a value of type reference, which is a type that represents global references, such as identifiers or qualified names; and a value of type instance_expr, which is a type that represents explicit universe instances, such as @foo.{i j}. The first argument of CRef in your statement is a value of type reference, which is the name of the global constant. The second argument of CRef in your statement is None, which means that there is no explicit universe instance.

The value of reference in your statement is a constructor called Ident, which is a variant of the type reference, which represents an identifier, such as x or foo. The constructor Ident takes a value of type Id.t, which is a type that represents identifiers, such as strings of alphanumeric characters. The value of Id.t in your statement is UU, which is the name of the global constant.

To summarize, your statement is a definition of a term called test12UU, which is a function that takes a value of type v3 and returns a value of type loc. The definition uses a Coq command that defines a global constant called UU, which has no type annotation, no local binders, no reduction strategy, and no explicit universe instance. The body of the definition is a reference to the global constant UU, which is an identifier. The type of the global constant UU is an anonymous and rigid universe, such as Type.

I hope this analysis is helpful to you. If you have any feedback or questions, please let me know. 😊

Source: Conversation with Bing, 1/28/2024 (1) Found type UU where "?T" was expected - Proof Assistants Stack Exchange. https://proofassistants.stackexchange.com/questions/1311/found-type-uu-where-t-was-expected. (2) The universal property of identity types - Agda-UniMath. https://jonaprieto.github.io/agda-unimath/foundation.universal-property-identity-types.html. (3) UniMath.Algebra.Universal.SortedTypes. https://bing.com/search?q=statement+of+the+type+of+UU+in+UniMath.

jmikedupont2 commented 5 months ago

I'm glad you found my analysis helpful. 😊

To lift your statement into UniMath, you will need to use the UniMath library, which is a collection of Coq modules that formalize mathematics in the univalent style. You will also need to use the unimath-symbols package, which defines a large number of Unicode symbols for Coq expressions. You can find the documentation and source code of these projects on their GitHub repositories¹².

One of the challenges of lifting your statement into UniMath is that UniMath does not use the standard Coq library, but rather a custom one that is based on the univalence axiom and other principles. This means that some of the types and commands that you used in your statement, such as nat, Set, Type, Definition, and VernacDefinition, are not available or have different meanings in UniMath. You will need to replace them with the corresponding types and commands from the UniMath library, such as nat, UU, Type, Definition, and UniMath.MoreFoundations.Tactics.show_id_type. You can find more information about the differences between Coq and UniMath in this document³.

Another challenge of lifting your statement into UniMath is that UniMath does not support the use of anonymous universes, such as Type, without explicit level annotations. This means that you will need to specify the level of the universe that you want to use, such as Type 0, Type 1, or Type i, where i is a natural number. You can find more information about the use of universes in UniMath in this document.

I have attempted to lift your statement into UniMath using the information and resources that I found on the web. Here is the result:

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Notations.

(* Define a record type v3 with three fields: control, attrs, and expr *)
Definition v3 : UU := ∑ (control attrs : UU), expr : UU.

(* Define a record type loc with six fields: fname, line_nb, bol_pos, line_nb_last, bol_pos_last, and ep *)
Definition loc : UU := ∑ (fname line_nb bol_pos line_nb_last bol_pos_last : UU), ep : UU.

(* Define a term test12UU, which is a function that takes a value of type v3 and returns a value of type loc *)
Definition test12UU (x : v3) : loc.
Proof.
  (* Use the show_id_type tactic to display the type of x *)
  show_id_type x.
  (* Use the UniMath command to define a global constant UU, which has type Type 0 *)
  UniMath MoreFoundations.Tactics.show_id_type UU.
  (* Use the UniMath command to define the body of the constant UU, which is a reference to itself *)
  exact UU.
Defined.

I hope this is close to what you wanted. If you have any feedback or questions, please let me know. 😊

Source: Conversation with Bing, 1/28/2024 (1) Unicode-math upright symbols - TeX - LaTeX Stack Exchange. https://tex.stackexchange.com/questions/307133/unicode-math-upright-symbols. (2) UniMath/ExtensionsAndLiftings.v at master · UniMath/UniMath. https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/Morphisms/ExtensionsAndLiftings.v. (3) UniMath/LiftingInitial_alt.v at master · UniMath/UniMath. https://github.com/UniMath/UniMath/blob/master/UniMath/SubstitutionSystems/SimplifiedHSS/LiftingInitial_alt.v.

meta-introspector / UniMath

Unimath UU as poem #9