有限型

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.fin 0 -> False
Proof.fin 0 -> False
  intro p.p: fin 0
False
  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).n: nat
p: fin (S n)
p = zero \/ exists q : fin n, p = suc q
Proof.n: nat
p: fin (S n)
p = zero \/ exists q : fin n, p = suc q
  destruct p using fin_S_case.n: nat
zero = zero \/ exists q : fin n, zero = suc q
n: nat
p: fin n
suc p = zero \/ exists q : fin n, suc p = suc q
  -n: nat
zero = zero \/ exists q : fin n, zero = suc q
    left.n: nat
zero = zero
    reflexivity.
  -n: nat
p: fin n
suc p = zero \/ exists q : fin n, suc p = suc q
    right.n: nat
p: fin n
exists q : fin n, suc p = suc q
    exists p.n: nat
p: fin n
suc p = suc 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.