(*|
有限型
======
|*)

Require Import function.

Inductive fin : nat -> Type :=
  | zero {n} : fin (S n)
  | suc  {n} : fin n -> fin (S n).

Lemma no_fin0 : fin 0 -> False.
Proof.
  intro p.
  inversion p.
Qed.

Definition fin_S_case {n}
  (p : fin (S n)) :
  forall P : fin (S n) -> Type,
  P zero ->
  (forall q, P (suc q)) ->
  P p
  :=
  match p with
  | zero  => fun P Pz _ => Pz
  | suc q => fun P _ Ps => Ps q
  end.

Lemma zero_or_suc {n} (p : fin (S n))
  : p = zero \/ (exists q, p = suc q).
Proof.
  destruct p using fin_S_case.
  -
    left.
    reflexivity.
  -
    right.
    exists p.
    reflexivity.
Qed.

Definition bishop_finite (A : Type) : Prop :=
  exists n, inhabited (A ≅ fin n).

Definition subfinite (A : Type) : Prop :=
  exists n (f : A -> fin n), injective f.

Definition finitely_indexed (A : Type) : Prop :=
  exists n (f : fin n -> A), surjective f.