* [HoTT] Definitional equality of types as strict bijection
@ 2023-02-04 13:56 Madeleine Birchfield
0 siblings, 0 replies; only message in thread
From: Madeleine Birchfield @ 2023-02-04 13:56 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 3789 bytes --]
In this thread, I follow the approach in Egbert Rijke's textbook in having
a separate type judgment, rather than the HoTT book's judgment in having an
infinite tower of universes and no separate type judgment, and I follow
Agda in using the bare equals sign for definitional equality.
In structural set theories like William Lawvere's ETCS or Mike Shulman's
SEAR it is quite common to have equality only for the sorts of elements,
functions, and relations, and not have any primitive equality relation for
the sort of sets. This means that the only way to compare sets for
"equality" is through a bijection of sets.
In addition, Mike Shulman's talks on Higher Observational Type Theory back
in May of 2022 includes a section where he talks about the right notion of
"definitional univalence" is not using the usual notion of definitional
equality of types, but rather strict bijection, where there are functions
idtoequiv(a, b):Id_U(a, b) -> Equiv_U(a, b)
equivtoid(a, b):Equiv_U(a, b) -> Id_U(a, b)
between the identity types Id_U(a, b) and the type of equivalences
Equiv_U(a, b) of elements a:U and b:U of a universe U, and definitional
equalities of elements
equivtoid(a, b)(idtoequiv(a, b)(p)) = p:Id_U(a, b)
idtoequiv(a, b)(equivtoid(a, b)(R)) = R:Equiv_U(a, b)
Using insights from structural set theory, one could go beyond definitional
univalence in Mike Shulman's Higher Observational Type Theory and directly
modify the structural rules for definitional equality of types so that it
behaves not as an equivalence relation a la first order logic with
equality, but rather strict bijection of types a la structural set theory,
using the following rules:
Gamma |- A = B type
---------------------------------
Gamma, x:A |- f(x):B
Gamma |- A = B type
---------------------------------
Gamma, y:B |- g(y):A
Gamma |- A = B type
---------------------------------
Gamma, x:A |- g(f(x)) = x:A
Gamma |- A = B type
---------------------------------
Gamma, y:B |- f(g(y)) = y:B
The variable conversion rule in dependent type theory then becomes
substitution of g(y) for x,
Gamma |- A = A' type Gamma, x:A, Delta(x) |- J(x)
------------------------------------------------------------------------------------
Gamma, y:A', Delta(g(y)) |- J(g(y))
The first congruence rule for substitution is the following rule
Gamma |- a = a':A Gamma, x:A, Delta(x) |- B(x) type
------------------------------------------------------------------------------------
Gamma, Delta(a) |- B(a) = B(a') type
and the strict bijection rules for definitional equality of types implies
that f and g for the definitional equality B(a) = B(a') type are judgmental
versions of transport. The second congruence rule for substitution becomes
merely a judgmental version of application to paths:
Gamma |- a = a':A Gamma, x:A, Delta(x) |- b(x):B(x) type
------------------------------------------------------------------------------------------
Gamma, Delta(a) |- b(a) = g(b(a')):B(a)
Definitional univalence then becomes under this collection of structural
rules the following rule
Gamma |- U type Gamma |- A:U Gamma |- B:U
------------------------------------------------------------------------------------------
Gamma |- Id_U(A, B) = Eq_U(A, B) type
from which one could derive Mike Shulman's original 4 rules for
definitionally univalent universes.
Madeleine Birchfield
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/45bf6ae5-b73b-4df2-a8bc-9aca972797e1n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 4668 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-02-04 13:59 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-02-04 13:56 [HoTT] Definitional equality of types as strict bijection Madeleine Birchfield
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).