Definición de conjuntos finitos en Agda

Question

Soy nuevo en Agda. Estoy leyendo el documento "Tipos dependientes en el trabajo" de Ana Bove y Peter Dybjer. No entiendo la discusión de Conjuntos finitos (en la página 15 en mi copia).

El documento define un tipo Fin:

data Fin : Nat -> Set where 
    fzero : {n : Nat} -> Fin (succ n) 
    fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

Debo estar perdiendo algo obvio. No entiendo cómo funciona esta definición. ¿Podría alguien simplemente traducir la definición de Fin al inglés cotidiano? Eso podría ser todo lo que necesito para entender esta parte del documento.

Gracias por tomarse el tiempo para leer mi pregunta. Lo aprecio.

Answer 1

data Fin : Nat -> Set where 

Fin es un tipo de datos parametrizada por un número natural (o: Fin es una función de nivel tipo que toma un Nat y devuelve un (tipo básico Set), es decir, para cualquier número natural nFin n es una Set)

fzero : {n : Nat} -> Fin (succ n) 

Para todos los números naturales nfzero es un miembro del tipo/set Fin (succ n) (de la que se deduce que para todos los números positivos (es decir, todos los productos naturales excepto cero) nfzero es miembro de Fin n).

fsucc : {n : Nat} -> Fin n -> Fin (succ n) 

Para todos los números naturales n y todos los valores de m de tipo Fin n, fsucc m es un miembro de tipo Fin (succ n).

---

Así fzero es miembro de Fin n para todos n excepto cero y fsucc m es miembro de Fin n para todos n que representan un número mayor que fsucc m.

Básicamente Fin n representa el conjunto de todos los números naturales menores que n, es decir, de todos los índices válidos para las listas de tamaño n.