(** Representation of cardinals, see Chapter 10 of the HoTT book. *)
Require Import HoTT.Universes.TruncType.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Classes.interfaces.abstract_algebra.

(** This speeds things up considerably *)
Local Opaque equiv_isequiv istrunc_isequiv_istrunc.

(** ** Definitions and operations *)

Definition Card := Trunc 0 HSet.

Definition card A `{IsHSet A} : Card
  := tr (Build_HSet A).

Definition sum_card (a b : Card) : Card.
a, b: Card
Card
Proof.
a, b: Card
Card
  strip_truncations.
b, a: HSet
Card
  exact (tr (Build_HSet (a + b))).
Defined.

Definition prod_card (a b : Card) : Card.
a, b: Card
Card
Proof.
a, b: Card
Card
  strip_truncations.
b, a: HSet
Card
  exact (tr (Build_HSet (a * b))).
Defined.

Definition exp_card `{Funext} (b a : Card) : Card.
H: Funext
b, a: Card
Card
Proof.
H: Funext
b, a: Card
Card
  strip_truncations.
H: Funext
a, b: HSet
Card
  exact (tr (Build_HSet (b -> a))).
Defined.

Definition leq_card `{Univalence} : Card -> Card -> HProp.
H: Univalence
Card -> Card -> HProp
Proof.
H: Univalence
Card -> Card -> HProp
  refine (Trunc_rec (fun a => _)).
H: Univalence
a: HSet
Card -> HProp
  refine (Trunc_rec (fun b => _)).
H: Univalence
a, b: HSet
HProp
  exact (hexists (fun (i : a -> b) => IsInjective i)).
Defined.

(** ** Properties *)
Section contents.
  Context `{Univalence}.

  #[export] Instance plus_card : Plus Card := sum_card.
  #[export] Instance mult_card : Mult Card := prod_card.
  #[export] Instance zero_card : Zero Card := tr (Build_HSet Empty).
  #[export] Instance one_card : One Card := tr (Build_HSet Unit).
  #[export] Instance le_card : Le Card := leq_card.

  (* Reduce an algebraic equation to an equivalence *)
  Local Ltac reduce :=
    repeat (intros ?); strip_truncations; cbn; f_ap; apply path_hset.

  (* Simplify an equation by unfolding all the definitions apart from
  the actual operations. *)
  (* Note that this is an expensive thing to do, and will be very slow unless we tell it not to unfold the following. *)
  Local Ltac simpl_ops :=
    cbv-[plus_card mult_card zero_card one_card exp_card].

  (** We only make the instances of upper classes global, since the
  other instances will be project anyway. *)

  (** *** [Card] is a semi-ring *)
  Instance associative_sum : Associative plus_card.
H: Univalence
Associative plus_card
  Proof.
H: Univalence
Associative plus_card reduce.
H: Univalence
z, y, x: HSet
Build_HSet (x + (y + z)) <~> Build_HSet (x + y + z) symmetry.
H: Univalence
z, y, x: HSet
Build_HSet (x + y + z) <~> Build_HSet (x + (y + z)) apply equiv_sum_assoc. Defined.

  Instance rightid_sum : RightIdentity plus_card zero_card.
H: Univalence
RightIdentity plus_card zero_card
  Proof.
H: Univalence
RightIdentity plus_card zero_card reduce.
H: Univalence
x: HSet
Build_HSet (x + Empty) <~> x apply sum_empty_r. Defined.

  Instance commutative_sum : Commutative plus_card.
H: Univalence
Commutative plus_card
  Proof.
H: Univalence
Commutative plus_card reduce.
H: Univalence
y, x: HSet
Build_HSet (x + y) <~> Build_HSet (y + x) apply equiv_sum_symm. Defined.

  Instance associative_prod : Associative mult_card.
H: Univalence
Associative mult_card
  Proof.
H: Univalence
Associative mult_card reduce.
H: Univalence
z, y, x: HSet
Build_HSet (x * (y * z)) <~> Build_HSet (x * y * z) apply equiv_prod_assoc. Defined.

  Instance rightid_prod : RightIdentity mult_card one_card.
H: Univalence
RightIdentity mult_card one_card
  Proof.
H: Univalence
RightIdentity mult_card one_card reduce.
H: Univalence
x: HSet
Build_HSet (x * Unit) <~> x apply prod_unit_r. Defined.

  Instance commutative_prod : Commutative mult_card.
H: Univalence
Commutative mult_card
  Proof.
H: Univalence
Commutative mult_card reduce.
H: Univalence
y, x: HSet
Build_HSet (x * y) <~> Build_HSet (y * x) apply equiv_prod_symm. Defined.

  Instance leftdistributive_card : LeftDistribute mult_card plus_card.
H: Univalence
LeftDistribute mult_card plus_card
  Proof.
H: Univalence
LeftDistribute mult_card plus_card reduce.
H: Univalence
c, b, a: HSet
Build_HSet (a * (b + c)) <~>
Build_HSet (a * b + a * c) apply sum_distrib_l. Defined.

  Instance leftabsorb_card : LeftAbsorb mult_card zero_card.
H: Univalence
LeftAbsorb mult_card zero_card
  Proof.
H: Univalence
LeftAbsorb mult_card zero_card reduce.
H: Univalence
y: HSet
Build_HSet (Empty * y) <~> Build_HSet Empty apply prod_empty_l. Defined.

  #[export] Instance issemiring_card : IsSemiCRing Card.
H: Univalence
IsSemiCRing Card
  Proof.
H: Univalence
IsSemiCRing Card
    repeat split; try exact _.
H: Univalence
LeftIdentity sg_op mon_unit
H: Univalence
LeftIdentity sg_op mon_unit
    -
H: Univalence
LeftIdentity sg_op mon_unit repeat intro.
H: Univalence
y: Card
sg_op mon_unit y = y simpl_ops.
H: Univalence
y: Card
plus_card zero_card y = y
      rewrite (commutativity zero_card _).
H: Univalence
y: Card
plus_card y zero_card = y
      apply rightid_sum.
    -
H: Univalence
LeftIdentity sg_op mon_unit repeat intro.
H: Univalence
y: Card
sg_op mon_unit y = y simpl_ops.
H: Univalence
y: Card
mult_card one_card y = y
      rewrite (commutativity one_card _).
H: Univalence
y: Card
mult_card y one_card = y
      apply rightid_prod.
  Defined.

  (** *** Properties of exponentiation *)
  Lemma exp_zero_card (a : Card) : exp_card 0 a = 1.
H: Univalence
a: Card
exp_card 0 a = 1
  Proof.
H: Univalence
a: Card
exp_card 0 a = 1 simpl_ops.
H: Univalence
a: Card
exp_card zero_card a = one_card reduce.
H: Univalence
a: HSet
Build_HSet (Empty -> a) <~> Build_HSet Unit symmetry.
H: Univalence
a: HSet
Build_HSet Unit <~> Build_HSet (Empty -> a) apply equiv_empty_rec. Defined.

  Lemma exp_card_one (a : Card) : exp_card a 1 = 1.
H: Univalence
a: Card
exp_card a 1 = 1
  Proof.
H: Univalence
a: Card
exp_card a 1 = 1 simpl_ops.
H: Univalence
a: Card
exp_card a one_card = one_card reduce.
H: Univalence
a: HSet
Build_HSet (a -> Unit) <~> Build_HSet Unit symmetry.
H: Univalence
a: HSet
Build_HSet Unit <~> Build_HSet (a -> Unit) apply equiv_unit_coind. Defined.

  Lemma exp_one_card (a : Card) : exp_card 1 a = a.
H: Univalence
a: Card
exp_card 1 a = a
  Proof.
H: Univalence
a: Card
exp_card 1 a = a reduce.
H: Univalence
a: HSet
Build_HSet (Unit -> a) <~> a symmetry.
H: Univalence
a: HSet
a <~> Build_HSet (Unit -> a) apply equiv_unit_rec. Defined.

  Lemma exp_card_sum_mult (a b c : Card) :
    exp_card (b + c) a = (exp_card b a) * (exp_card c a).
H: Univalence
a, b, c: Card
exp_card (b + c) a = exp_card b a * exp_card c a
  Proof.
H: Univalence
a, b, c: Card
exp_card (b + c) a = exp_card b a * exp_card c a reduce.
H: Univalence
c, b, a: HSet
Build_HSet (b + c -> a) <~>
Build_HSet ((b -> a) * (c -> a)) symmetry.
H: Univalence
c, b, a: HSet
Build_HSet ((b -> a) * (c -> a)) <~>
Build_HSet (b + c -> a) apply equiv_sum_distributive. Defined.

  Lemma exp_mult_card_exp (a b c : Card) :
    exp_card (b * c) a = exp_card c (exp_card b a).
H: Univalence
a, b, c: Card
exp_card (b * c) a = exp_card c (exp_card b a)
  Proof.
H: Univalence
a, b, c: Card
exp_card (b * c) a = exp_card c (exp_card b a)
    rewrite (@commutativity _ _ (.*.) _ b c).
H: Univalence
a, b, c: Card
exp_card (c * b) a = exp_card c (exp_card b a)
    reduce.
H: Univalence
c, b, a: HSet
Build_HSet (c * b -> a) <~> Build_HSet (c -> b -> a) symmetry.
H: Univalence
c, b, a: HSet
Build_HSet (c -> b -> a) <~> Build_HSet (c * b -> a) apply equiv_uncurry.
  Defined.

  Lemma exp_card_mult_mult (a b c : Card) :
    exp_card c (a * b) = (exp_card c a) * (exp_card c b).
H: Univalence
a, b, c: Card
exp_card c (a * b) = exp_card c a * exp_card c b
  Proof.
H: Univalence
a, b, c: Card
exp_card c (a * b) = exp_card c a * exp_card c b reduce.
H: Univalence
c, b, a: HSet
Build_HSet (c -> a * b) <~>
Build_HSet ((c -> a) * (c -> b)) symmetry.
H: Univalence
c, b, a: HSet
Build_HSet ((c -> a) * (c -> b)) <~>
Build_HSet (c -> a * b) apply equiv_prod_coind. Defined.

  (** *** Properties of ≤ *)
  Instance reflexive_card : Reflexive leq_card.
H: Univalence
Reflexive (fun x x0 : Card => leq_card x x0)
  Proof.
H: Univalence
Reflexive (fun x x0 : Card => leq_card x x0)
    intro x.
H: Univalence
x: Card
leq_card x x strip_truncations.
H: Univalence
x: HSet
leq_card (tr x) (tr x)
    apply tr.
H: Univalence
x: HSet
{i : x -> x & IsInjective i} exists idmap.
H: Univalence
x: HSet
IsInjective idmap exact (fun _ _ => idmap).
  Defined.

  Instance transitive_card : Transitive leq_card.
H: Univalence
Transitive (fun x x0 : Card => leq_card x x0)
  Proof.
H: Univalence
Transitive (fun x x0 : Card => leq_card x x0)
    intros a b c.
H: Univalence
a, b, c: Card
leq_card a b -> leq_card b c -> leq_card a c strip_truncations.
H: Univalence
c, b, a: HSet
leq_card (tr a) (tr b) ->
leq_card (tr b) (tr c) -> leq_card (tr a) (tr c)
    intros Hab Hbc.
H: Univalence
c, b, a: HSet
Hab: leq_card (tr a) (tr b)
Hbc: leq_card (tr b) (tr c)
leq_card (tr a) (tr c) strip_truncations.
H: Univalence
c, b, a: HSet
Hbc: {i : b -> c & IsInjective i}
Hab: {i : a -> b & IsInjective i}
leq_card (tr a) (tr c)
    destruct Hab as [iab Hab].
H: Univalence
c, b, a: HSet
Hbc: {i : b -> c & IsInjective i}
iab: a -> b
Hab: IsInjective iab
leq_card (tr a) (tr c)
    destruct Hbc as [ibc Hbc].
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
leq_card (tr a) (tr c)
    apply tr.
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
{i : a -> c & IsInjective i} exists (ibc ∘ iab).
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
IsInjective (ibc ∘ iab)
    intros x y Hxy.
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
x, y: a
Hxy: (ibc ∘ iab) x = (ibc ∘ iab) y
x = y
    apply Hab.
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
x, y: a
Hxy: (ibc ∘ iab) x = (ibc ∘ iab) y
iab x = iab y apply Hbc.
H: Univalence
c, b, a: HSet
ibc: b -> c
Hbc: IsInjective ibc
iab: a -> b
Hab: IsInjective iab
x, y: a
Hxy: (ibc ∘ iab) x = (ibc ∘ iab) y
ibc (iab x) = ibc (iab y) exact Hxy.
  Defined.

  #[export] Instance preorder_card : PreOrder le_card.
H: Univalence
PreOrder le_card
  Proof.
H: Univalence
PreOrder le_card split; exact _. Defined.

End contents.


(** * Cardinality comparisons *)

(* We also work with cardinality comparisons directly to avoid unnecessary type truncations via cardinals. *)

Definition Injection X Y :=
  { f : X -> Y | IsInjective f }.

Instance Injection_refl :
  Reflexive Injection.
Reflexive Injection
Proof.
Reflexive Injection
  intros X.
X: Type
Injection X X exists (fun x => x).
X: Type
IsInjective idmap intros x x'.
X: Type
x, x': X
x = x' -> x = x' done.
Qed.

Lemma Injection_trans X Y Z :
  Injection X Y -> Injection Y Z -> Injection X Z.
X, Y, Z: Type
Injection X Y -> Injection Y Z -> Injection X Z
Proof.
X, Y, Z: Type
Injection X Y -> Injection Y Z -> Injection X Z
  intros [f Hf] [g Hg].
X, Y, Z: Type
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
Injection X Z exists (fun x => g (f x)).
X, Y, Z: Type
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
IsInjective (fun x : X => g (f x))
  intros x x' H.
X, Y, Z: Type
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
x, x': X
H: g (f x) = g (f x')
x = x' by apply Hf, Hg.
Qed.

Definition InjectsInto X Y :=
  merely (Injection X Y).

Instance InjectsInto_refl :
  Reflexive InjectsInto.
Reflexive (fun X Y : Type => InjectsInto X Y)
Proof.
Reflexive (fun X Y : Type => InjectsInto X Y)
  intros X.
X: Type
InjectsInto X X apply tr.
X: Type
Injection X X reflexivity.
Qed.

Lemma InjectsInto_trans X Y Z :
  InjectsInto X Y -> InjectsInto Y Z -> InjectsInto X Z.
X, Y, Z: Type
InjectsInto X Y -> InjectsInto Y Z -> InjectsInto X Z
Proof.
X, Y, Z: Type
InjectsInto X Y -> InjectsInto Y Z -> InjectsInto X Z
  intros H1 H2.
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
InjectsInto X Z
  eapply merely_destruct; try exact H1.
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
Injection X Y -> InjectsInto X Z intros [f Hf].
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
InjectsInto X Z
  eapply merely_destruct; try exact H2.
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
Injection Y Z -> InjectsInto X Z intros [g Hg].
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
InjectsInto X Z
  apply tr.
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
Injection X Z exists (fun x => g (f x)).
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
IsInjective (fun x : X => g (f x))
  intros x x' H.
X, Y, Z: Type
H1: InjectsInto X Y
H2: InjectsInto Y Z
f: X -> Y
Hf: IsInjective f
g: Y -> Z
Hg: IsInjective g
x, x': X
H: g (f x) = g (f x')
x = x' by apply Hf, Hg.
Qed.



(** * Infinity *)

(* We call a set infinite if nat embeds into it. *)

Definition infinite X :=
  Injection nat X.