Cómo representar Smullyan del "Ruiseñor" en los puzzles (Homotopy) Tipo de Teoría?

Question

(Si no estás familiarizado con los puzzles de Burlarse De un Ruiseñor, de tres páginas dirá todo lo que usted necesita.)

Es posible resolver los enigmas en Burlarse De un Ruiseñor en una "proposiciones como" tipos de estilo?

Como ejemplo, tomemos el segundo problema:

Un pájaro x se llama egocéntrico (a veces narcisista) si es aficionado a sí mismo-es decir, si x la respuesta de x es x. En símbolos, x es egocéntrico si xx = x. El problema es demostrar que en las condiciones dadas $\text{C}_1$ $\text{C}_2$ de la última problema, al menos una de las aves es egocéntrico.

En algo como de Orden Superior de la Lógica, que yo definiría como egocentrismo

definition egocentric :: "Bird => Bool" where
  "egocentric A == (call A A = A)"

(asumiendo call :: Bird => Bird => Bird)

Un ingenuo intento de codificación de egocentrismo como un tipo de ser $$ \text{egocéntrico} : \textbf{Aves} \rightarrow \operatorname{call}, (a, a)=A $$

However, an obvious problem is that $$ No está atado en el tipo de identidad $$ \operatorname{call}, (a, a)=A $$ (que, en HoTT es "de forma enjuiciadora de la igualdad" para el tipo de $\textbf{Id}_{\textbf{Bird}}(\operatorname{call}(A,A), A)$)
Por lo tanto, necesitamos un dependiente de la definición de la función, ¿verdad? $$ \text{egocéntrico} : \Pi A:\textbf{Aves}. llame al(a, a) =_\textbf{Aves} $$

But... that doesn't look like the type-theory equivalent of an unary predicate; it looks like the claim "Every bird's response to its own name is its name"!

If it's helpful to instead ask a very specific question:

Given the "composition" and "mockingbird" conditions (q.v. the book's first exercise), how would you construct a term of the following type? $$\Pi A:\textbf{Bird}. \Sigma x:\textbf{Bird}. \operatorname{call}(A, x) = x$$ (Sorta implícita: ¿cómo se codifican la "composición" y "mockingbird" givens?)

Answer 1

Vamos a tomar las cosas despacio. Lo primero es lo primero: $\mathsf{egocentric}$ es un predicado, por lo que es un $\mathsf{Type}$valores de la función de algún tipo. En este caso, es una función de $\mathsf{Bird} \to \mathsf{Type}$. Se define de la siguiente manera: $$\mathsf{egocentric} \equiv \lambda A : \mathsf{Bird} . \mathsf{call}(A, A) =_{\mathsf{Bird}} A$$ Por lo tanto: $$\mathop{\mathsf{egocentric}} A \equiv \mathsf{call}(A, A) =_{\mathsf{Bird}} A$$

Dicho esto, tengo que cuestionar sus motivos. No hay ningún beneficio en la forma de pensar sobre el problema de esta manera. Es más útil para trabajar directamente con el (escrito) $\lambda$-cálculo integrada en el tipo de teoría que intentar construir un modelo interno de la misma.