Library HoTT.Spaces.Card
(* -*- mode: coq; mode: visual-line -*- *)
Representation of cardinals, see Chapter 10 of the HoTT book.
This speeds things up considerably
Definition Card := Trunc 0 HSet.
Definition card A `{IsHSet A} : Card
:= tr (Build_HSet A).
Definition sum_card (a b : Card) : Card.
Proof.
strip_truncations.
refine (tr (Build_HSet (a + b))).
Defined.
Definition prod_card (a b : Card) : Card.
Proof.
strip_truncations.
refine (tr (Build_HSet (a × b))).
Defined.
Definition exp_card `{Funext} (b a : Card) : Card.
Proof.
strip_truncations.
refine (tr (Build_HSet (b → a))).
Defined.
Definition leq_card `{Univalence} : Card → Card → HProp.
Proof.
refine (Trunc_rec (fun a ⇒ _)).
refine (Trunc_rec (fun b ⇒ _)).
exact (hexists (fun (i : a → b) ⇒ IsInjective i)).
Defined.
Section contents.
Context `{Univalence}.
Global Instance plus_card : Plus Card := sum_card.
Global Instance mult_card : Mult Card := prod_card.
Global Instance zero_card : Zero Card := tr (Build_HSet Empty).
Global Instance one_card : One Card := tr (Build_HSet Unit).
Global 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].
Context `{Univalence}.
Global Instance plus_card : Plus Card := sum_card.
Global Instance mult_card : Mult Card := prod_card.
Global Instance zero_card : Zero Card := tr (Build_HSet Empty).
Global Instance one_card : One Card := tr (Build_HSet Unit).
Global 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.
Proof. reduce. symmetry. apply equiv_sum_assoc. Defined.
Instance rightid_sum : RightIdentity plus_card zero_card.
Proof. reduce. apply sum_empty_r. Defined.
Instance commutative_sum : Commutative plus_card.
Proof. reduce. apply equiv_sum_symm. Defined.
Instance associative_prod : Associative mult_card.
Proof. reduce. apply equiv_prod_assoc. Defined.
Instance rightid_prod : RightIdentity mult_card one_card.
Proof. reduce. apply prod_unit_r. Defined.
Instance commutative_prod : Commutative mult_card.
Proof. reduce. apply equiv_prod_symm. Defined.
Instance leftdistributive_card : LeftDistribute mult_card plus_card.
Proof. reduce. apply sum_distrib_l. Defined.
Instance leftabsorb_card : LeftAbsorb mult_card zero_card.
Proof. reduce. apply prod_empty_l. Defined.
Global Instance issemiring_card : IsSemiCRing Card.
Proof.
repeat split; try apply _.
- repeat intro. simpl_ops.
rewrite (commutativity zero_card _).
apply rightid_sum.
- repeat intro. simpl_ops.
rewrite (commutativity one_card _).
apply rightid_prod.
Defined.
Proof. reduce. symmetry. apply equiv_sum_assoc. Defined.
Instance rightid_sum : RightIdentity plus_card zero_card.
Proof. reduce. apply sum_empty_r. Defined.
Instance commutative_sum : Commutative plus_card.
Proof. reduce. apply equiv_sum_symm. Defined.
Instance associative_prod : Associative mult_card.
Proof. reduce. apply equiv_prod_assoc. Defined.
Instance rightid_prod : RightIdentity mult_card one_card.
Proof. reduce. apply prod_unit_r. Defined.
Instance commutative_prod : Commutative mult_card.
Proof. reduce. apply equiv_prod_symm. Defined.
Instance leftdistributive_card : LeftDistribute mult_card plus_card.
Proof. reduce. apply sum_distrib_l. Defined.
Instance leftabsorb_card : LeftAbsorb mult_card zero_card.
Proof. reduce. apply prod_empty_l. Defined.
Global Instance issemiring_card : IsSemiCRing Card.
Proof.
repeat split; try apply _.
- repeat intro. simpl_ops.
rewrite (commutativity zero_card _).
apply rightid_sum.
- repeat intro. simpl_ops.
rewrite (commutativity one_card _).
apply rightid_prod.
Defined.
Lemma exp_zero_card (a : Card) : exp_card 0 a = 1.
Proof. simpl_ops. reduce. symmetry. apply equiv_empty_rec. Defined.
Lemma exp_card_one (a : Card) : exp_card a 1 = 1.
Proof. simpl_ops. reduce. symmetry. apply equiv_unit_coind. Defined.
Lemma exp_one_card (a : Card) : exp_card 1 a = a.
Proof. reduce. symmetry. 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).
Proof. reduce. symmetry. 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).
Proof.
rewrite (@commutativity _ _ (.*.) _ b c).
reduce. symmetry. 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).
Proof. reduce. symmetry. apply equiv_prod_coind. Defined.
Proof. simpl_ops. reduce. symmetry. apply equiv_empty_rec. Defined.
Lemma exp_card_one (a : Card) : exp_card a 1 = 1.
Proof. simpl_ops. reduce. symmetry. apply equiv_unit_coind. Defined.
Lemma exp_one_card (a : Card) : exp_card 1 a = a.
Proof. reduce. symmetry. 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).
Proof. reduce. symmetry. 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).
Proof.
rewrite (@commutativity _ _ (.*.) _ b c).
reduce. symmetry. 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).
Proof. reduce. symmetry. apply equiv_prod_coind. Defined.
Instance reflexive_card : Reflexive leq_card.
Proof.
intro x. strip_truncations.
apply tr. ∃ idmap. refine (fun _ _ ⇒ idmap).
Defined.
Instance transitive_card : Transitive leq_card.
Proof.
intros a b c. strip_truncations.
intros Hab Hbc. strip_truncations.
destruct Hab as [iab Hab].
destruct Hbc as [ibc Hbc].
apply tr. ∃ (ibc ∘ iab).
intros x y Hxy.
apply Hab. apply Hbc. apply Hxy.
Defined.
Global Instance preorder_card : PreOrder le_card.
Proof. split; apply _. Defined.
End contents.
Proof.
intro x. strip_truncations.
apply tr. ∃ idmap. refine (fun _ _ ⇒ idmap).
Defined.
Instance transitive_card : Transitive leq_card.
Proof.
intros a b c. strip_truncations.
intros Hab Hbc. strip_truncations.
destruct Hab as [iab Hab].
destruct Hbc as [ibc Hbc].
apply tr. ∃ (ibc ∘ iab).
intros x y Hxy.
apply Hab. apply Hbc. apply Hxy.
Defined.
Global Instance preorder_card : PreOrder le_card.
Proof. split; apply _. Defined.
End contents.
(* We also work with cardinality comparisons directly to avoid unnecessary type truncations via cardinals. *)
Definition Injection X Y :=
{ f : X → Y | IsInjective f }.
Global Instance Injection_refl :
Reflexive Injection.
Proof.
intros X. ∃ (fun x ⇒ x). intros x x'. easy.
Qed.
Lemma Injection_trans X Y Z :
Injection X Y → Injection Y Z → Injection X Z.
Proof.
intros [f Hf] [g Hg]. ∃ (fun x ⇒ g (f x)).
intros x x' H. now apply Hf, Hg.
Qed.
Definition InjectsInto X Y :=
merely (Injection X Y).
Global Instance InjectsInto_refl :
Reflexive InjectsInto.
Proof.
intros X. apply tr. reflexivity.
Qed.
Lemma InjectsInto_trans X Y Z :
InjectsInto X Y → InjectsInto Y Z → InjectsInto X Z.
Proof.
intros H1 H2.
eapply merely_destruct; try apply H1. intros [f Hf].
eapply merely_destruct; try apply H2. intros [g Hg].
apply tr. ∃ (fun x ⇒ g (f x)).
intros x x' H. now apply Hf, Hg.
Qed.