Hello, this is Copilot. It seems that you are working on a proof in homotopy type theory using the UniMath proof assistant. I can try to help you with some information and suggestions, but I cannot guarantee the correctness or completeness of my responses.
From your goal and debug output, I can see that you are trying to apply the hsubtype_univalence lemma, which states that for any two hsubtypes of a given hSet, there is an equivalence between the propositions that they are equal and that they are equivalent. This lemma is a special case of the univalence axiom, which is one of the main features of homotopy type theory. The univalence axiom asserts that for any two types, there is an equivalence between the propositions that they are equal and that they are equivalent. ¹
The univalence axiom is incompatible with the uniqueness of identity proofs (UIP), which is the assumption that all types are h-sets, i.e., that any two proofs of equality between two elements
Source: Conversation with Bing, 2/4/2024
(1) [2005.00260] Partial Univalence in n-truncated Type Theory - arXiv.org. https://arxiv.org/abs/2005.00260.
Sure, I'll try to explain it with some analogies and metaphors. Please note that these are not exact, but only meant to illustrate some aspects of the concepts.
The univalence axiom is like saying that two books are the same if they have the same content, regardless of their covers, titles, or editions. The equivalence between the books is like a translation that preserves the meaning of the text. The identity between the books is like a copy that preserves the physical appearance of the book. The univalence axiom asserts that these two notions of sameness are interchangeable, and that any translation can be turned into a copy and vice versa.
UIP is like saying that two books are the same only if they are identical copies, and that there is only one way to copy a book. This means that any two books with different covers, titles, or editions are different, even if they have the same content. UIP also means that any translation between books is trivial, and that it does not change anything about the books.
Partial univalence is like saying that two books are the same if they have the same content, but only for certain kinds of books. For example, one might say that two books are the same if they are both dictionaries, or if they are both novels, but not if they are of different genres. Partial univalence also means that there are different ways to translate between books of the same kind, but not between books of different kinds.
The hsubtype_univalence lemma is like saying that two books are the same if they have the same content, but only for books that have a fixed number of pages. For example, one might say that two books are the same if they are both 100-page books, or if they are both 200-page books, but not if they have different numbers of pages. The hsubtype_univalence lemma also means that there are different ways to translate between books of the same size, but not between books of different sizes.
Goal:
X : hSet g : pr1hSet (choice_fun X) lem : hProptoType LEM C : WOSubset X gC : hProptoType (is_guided_WOSubset g C) D : WOSubset X gD : hProptoType (is_guided_WOSubset g D) W := max_common_initial (WOSubset_to_TOSubset C) (WOSubset_to_TOSubset D) : hsubtype (pr1hSet X) WC : hProptoType (W ⊆ TOSubset_to_subtype (WOSubset_to_TOSubset C)) WD : hProptoType (W ⊆ TOSubset_to_subtype (WOSubset_to_TOSubset D)) WCi : hProptoType (sub_initial WC) WDi : hProptoType (sub_initial WD) WCD : hProptoType (same_induced_ordering WC WD) eWC : hProptoType (W ≡ TOSubset_to_subtype (WOSubset_to_TOSubset C))
(W = TOSubset_to_subtype (WOSubset_to_TOSubset C))%type
DEBUG:Going to execute: PTRDEBUGTACapply hsubtype_univalence DEBUG LTAC Evaluated term: hinhpr DEBUG LTAC Evaluated term: E DEBUG LTAC Evaluated term: inl DEBUG LTAC Evaluated term: (W = TOSubset_to_subtype (WOSubset_to_TOSubset C))%type
TcDebug (0) > /mnt/data1/2024/01/05/UniMath/UniMath/Combinatorics/WellOrderedSets.v:1148
Hello, this is Copilot. It seems that you are working on a proof in homotopy type theory using the UniMath proof assistant. I can try to help you with some information and suggestions, but I cannot guarantee the correctness or completeness of my responses.
From your goal and debug output, I can see that you are trying to apply the
hsubtype_univalencelemma, which states that for any two hsubtypes of a given hSet, there is an equivalence between the propositions that they are equal and that they are equivalent. This lemma is a special case of the univalence axiom, which is one of the main features of homotopy type theory. The univalence axiom asserts that for any two types, there is an equivalence between the propositions that they are equal and that they are equivalent. ¹The univalence axiom is incompatible with the uniqueness of identity proofs (UIP), which is the assumption that all types are h-sets, i.e., that any two proofs of equality between two elements
Source: Conversation with Bing, 2/4/2024 (1) [2005.00260] Partial Univalence in n-truncated Type Theory - arXiv.org. https://arxiv.org/abs/2005.00260.
Sure, I'll try to explain it with some analogies and metaphors. Please note that these are not exact, but only meant to illustrate some aspects of the concepts.
hsubtype_univalencelemma is like saying that two books are the same if they have the same content, but only for books that have a fixed number of pages. For example, one might say that two books are the same if they are both 100-page books, or if they are both 200-page books, but not if they have different numbers of pages. Thehsubtype_univalencelemma also means that there are different ways to translate between books of the same size, but not between books of different sizes.