Library subobjects.b_finite
Require Import HoTT HitTactics.
Require Import FSets interfaces.lattice_interface.
From subobjects Require Import sub k_finite.
Section finite_hott.
Variable (A : Type).
Context `{Univalence}.
Definition Bfin (X : Sub A) : hProp := BuildhProp (Finite {a : A & a ∈ X}).
Global Instance singleton_contr a `{IsHSet A} : Contr {b : A & b ∈ {|a|}}.
Proof.
∃ (a; tr idpath).
intros [b p].
simple refine (Trunc_ind (fun p ⇒ (a; tr 1%path) = (b; p)) _ p).
clear p; intro p ; simpl.
apply path_sigma_hprop; simpl.
apply p^.
Defined.
Definition singleton_fin_equiv' a : Fin 1 → {b : A & b ∈ {|a|}}.
Proof.
intros _. apply (a; tr idpath).
Defined.
Global Instance singleton_fin_equiv a `{IsHSet A} : IsEquiv (singleton_fin_equiv' a).
Proof. apply _. Defined.
Definition singleton `{IsHSet A} : closedSingleton Bfin.
Proof.
intros a.
simple refine (Build_Finite _ 1 _).
apply tr.
symmetry.
refine (BuildEquiv _ _ (singleton_fin_equiv' a) _).
Defined.
Definition empty_finite : closedEmpty Bfin.
Proof.
simple refine (Build_Finite _ 0 _).
apply tr.
simple refine (BuildEquiv _ _ _ _).
intros [a p]; apply p.
Defined.
Definition decidable_empty_finite : hasDecidableEmpty Bfin.
Proof.
intros X [n f].
strip_truncations.
destruct n.
- refine (tr(inl _)).
apply path_forall. intro z.
apply path_iff_hprop.
× intros p.
contradiction (f (z;p)).
× contradiction.
- refine (tr(inr _)).
apply (tr(f^-1(inr tt))).
Defined.
Lemma no_union `{IsHSet A}
(U : ∀ (X Y : Sub A),
Bfin X → Bfin Y → Bfin (X ∪ Y))
: DecidablePaths A.
Proof.
intros a b.
destruct (U {|a|} {|b|} (singleton a) (singleton b)) as [n pn].
strip_truncations.
unfold Sect in ×.
destruct pn as [f [g fg gf _]], n as [ | [ | n]].
- contradiction f.
∃ a.
apply (tr(inl(tr idpath))).
- refine (inl _).
pose (s1 := (a;tr(inl(tr idpath)))
: {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
pose (s2 := (b;tr(inr(tr idpath)))
: {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
refine (ap (fun x ⇒ x.1) (gf s1)^ @ _ @ (ap (fun x ⇒ x.1) (gf s2))).
assert (fs_eq : f s1 = f s2).
{ by apply path_ishprop. }
refine (ap (fun x ⇒ (g x).1) fs_eq).
-
refine (inr (fun p ⇒ _)).
pose (s1 := inl (inr tt) : Fin n + Unit + Unit).
pose (s2 := inr tt : Fin n + Unit + Unit).
pose (gs1 := g s1).
pose (c := gs1).
pose (gs2 := g s2).
pose (d := gs2).
assert (Hgs1 : gs1 = c) by reflexivity.
assert (Hgs2 : gs2 = d) by reflexivity.
destruct c as [x px'], d as [y py'].
simple refine (Trunc_ind _ _ px') ; intros px
; simple refine (Trunc_ind _ _ py') ; intros py ; simpl.
enough (s1 = s2) as X.
{
unfold s1, s2 in X.
contradiction (inl_ne_inr _ _ X).
}
refine ((fg s1)^ @ ap f (Hgs1 @ _ @ Hgs2^) @ fg s2).
simple refine (path_sigma _ _ _ _ _); [ | apply path_ishprop ]; simpl.
destruct px as [px | px] ; destruct py as [py | py]
; refine (Trunc_rec _ px) ; clear px ; intro px
; refine (Trunc_rec _ py) ; clear py ; intro py.
× apply (px @ py^).
× refine (px @ p @ py^).
× refine (px @ p^ @ py^).
× apply (px @ py^).
Defined.
End finite_hott.
Section singleton_set.
Variable (A : Type).
Context `{Univalence}.
Variable (HA : ∀ a, {b : A & b ∈ {|a|}} <~> Fin 1).
Definition el x : {b : A & b ∈ {|x|}} := (x;tr idpath).
Theorem single_bfin_set : ∀ (x : A) (p : x = x), p = idpath.
Proof.
intros x p.
specialize (HA x).
pose (el x) as X.
pose (ap HA^-1 (ap HA (path_sigma _ X X p (path_ishprop _ _)))) as q.
assert (p = ap (fun z ⇒ z.1) ((eissect HA X)^ @ q @ eissect HA X)) as H1.
{
unfold q.
rewrite <- ap_compose.
enough(∀ r,
(eissect HA X)^
@ ap (fun x0 : {b : A & b ∈ {|x|}} ⇒ HA^-1 (HA x0)) r
@ eissect HA X = r
) as H2.
{
rewrite H2.
refine (@pr1_path_sigma _ _ X X p _)^.
}
induction r.
hott_simpl.
}
assert (idpath = ap (fun z ⇒ z.1) ((eissect HA X)^ @ idpath @ eissect HA X)) as H2.
{ hott_simpl. }
rewrite H1, H2.
repeat f_ap.
unfold q.
enough (ap HA (path_sigma (fun b : A ⇒ b ∈ {|x|}) X X p (path_ishprop _ _)) = idpath) as H3.
{
rewrite H3.
reflexivity.
}
apply path_ishprop.
Defined.
Global Instance set_singleton : IsHSet A.
Proof.
refine hset_axiomK.
unfold axiomK.
apply single_bfin_set.
Defined.
End singleton_set.
Section empty.
Variable (A : Type).
Variable (X : A → hProp)
(Xequiv : {a : A & a ∈ X} <~> Fin 0).
Context `{Univalence}.
Lemma X_empty : X = ∅.
Proof.
apply path_forall.
intro z.
apply path_iff_hprop ; try contradiction.
intro x.
destruct Xequiv as [f fequiv].
contradiction (f(z;x)).
Defined.
End empty.
Section split.
Context `{Univalence}.
Variable (A : Type).
Variable (P : A → hProp)
(n : nat)
(f : {a : A & P a } <~> Fin n + Unit).
Definition split : ∃ P' : Sub A, ∃ b : A,
({a : A & P' a} <~> Fin n) × (∀ x, P x = (P' x ∨ merely (x = b))).
Proof.
pose (fun x : A ⇒ sig (fun y : Fin n ⇒ x = (f^-1 (inl y)).1)) as P'.
assert (∀ x, IsHProp (P' x)).
{
intros a. unfold P'.
apply hprop_allpath.
intros [x px] [y py].
pose (p := px^ @ py).
assert (p2 : p # (f^-1 (inl x)).2 = (f^-1 (inl y)).2).
{ apply path_ishprop. }
simple refine (path_sigma' _ _ _).
- apply path_sum_inl with Unit.
refine (transport (fun z ⇒ z = inl y) (eisretr f (inl x)) _).
refine (transport (fun z ⇒ _ = z) (eisretr f (inl y)) _).
apply (ap f).
apply path_sigma_hprop. apply p.
- rewrite transport_paths_FlFr.
hott_simpl; cbn.
rewrite ap_compose, (ap_compose inl f^-1).
rewrite ap_inl_path_sum_inl.
repeat (rewrite transport_paths_FlFr; hott_simpl).
rewrite !ap_pp.
rewrite ap_V.
rewrite <- !other_adj.
rewrite <- (ap_compose f (f^-1)).
rewrite ap_equiv.
rewrite !ap_pp.
rewrite ap_pr1_path_sigma_hprop.
rewrite !concat_pp_p.
rewrite !ap_V.
rewrite concat_Vp.
rewrite (concat_p_pp (ap pr1 (eissect f (f^-1 (inl x))))^).
rewrite concat_Vp.
hott_simpl.
}
∃ (fun a ⇒ BuildhProp (P' a)).
∃ (f^-1 (inr tt)).1.
split.
{ unshelve eapply BuildEquiv.
{ refine (fun x ⇒ x.2.1). }
apply isequiv_biinv.
unshelve esplit;
∃ (fun x ⇒ (((f^-1 (inl x)).1; (x; idpath)))).
- intros [a [y p]]; cbn.
eapply path_sigma with p^.
apply path_ishprop.
- intros x.
reflexivity.
}
{ intros a.
unfold P'.
apply path_iff_hprop.
- intros Ha.
pose (y := f (a;Ha)).
assert (Hy : y = f (a; Ha)) by reflexivity.
destruct y as [y | []].
+ refine (tr (inl _)).
∃ y.
rewrite Hy.
by rewrite eissect.
+ refine (tr (inr (tr _))).
rewrite Hy.
by rewrite eissect.
- intros Hstuff.
strip_truncations.
destruct Hstuff as [[y Hy] | Ha].
+ rewrite Hy.
apply (f^-1 (inl y)).2.
+ strip_truncations.
rewrite Ha.
apply (f^-1 (inr tt)).2. }
Defined.
End split.
Arguments Bfin {_} _.
Arguments split {_} {_} _ _ _.
Section Bfin_no_singletons.
Definition S1toSig (x : S1) : {x : S1 & merely(x = base)}.
Proof.
∃ x.
simple refine (S1_ind (fun z ⇒ merely(z = base)) (tr idpath) _ x).
apply path_ishprop.
Defined.
Instance S1toSig_equiv : IsEquiv S1toSig.
Proof.
apply isequiv_biinv.
split.
- ∃ (fun x ⇒ x.1).
simple refine (S1_ind _ idpath _) ; simpl.
rewrite transport_paths_FlFr.
hott_simpl.
- ∃ (fun x ⇒ x.1).
intros [z x].
simple refine (path_sigma _ _ _ _ _) ; simpl.
× reflexivity.
× apply path_ishprop.
Defined.
Theorem no_singleton `{Univalence} (Hsing : Bfin {|base|}) : Empty.
Proof.
destruct Hsing as [n equiv].
strip_truncations.
assert (S1 <~> Fin n) as X.
{ apply (equiv_compose equiv S1toSig). }
assert (IsHSet S1) as X1.
{
rewrite (path_universe X).
apply _.
}
enough (idpath = loop).
- assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap.
rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'.
apply (pos_neq_zero H').
- apply set_path2.
Defined.
End Bfin_no_singletons.
Section dec_membership.
Variable (A : Type).
Context `{MerelyDecidablePaths A} `{Univalence}.
Global Instance DecidableMembership (P : Sub A) (Hfin : Bfin P) (a : A) :
Decidable (a ∈ P).
Proof.
destruct Hfin as [n Hequiv].
strip_truncations.
revert Hequiv.
revert P.
induction n.
- intros.
pose (X_empty _ P Hequiv) as p.
rewrite p.
apply _.
- intros.
destruct (split P n Hequiv) as
(P' & b & HP' & HP).
unfold member, sub_membership.
rewrite (HP a).
destruct (IHn P' HP') as [IH | IH].
× apply (inl (tr (inl IH))).
× destruct (m_dec_path a b) as [Hab | Hab].
+ apply (inl (tr (inr Hab))).
+ refine (inr(fun a ⇒ _)).
strip_truncations.
destruct a as [? | t] ; [ | strip_truncations] ; try contradiction.
contradiction (Hab (tr t)).
Defined.
End dec_membership.
Section bfin_kfin.
Context `{Univalence}.
Lemma bfin_to_kfin : ∀ (B : Type), Finite B → Kf B.
Proof.
apply finite_ind_hprop.
- apply _.
- apply Kf_unfold.
∃ ∅. intros [].
- intros B [n f] IH.
apply Kf_sum ; try assumption.
apply Kf_Unit.
Defined.
Definition bfin_to_kfin_sub A : ∀ (P : Sub A), Bfin P → Kf_sub _ P.
Proof.
intros P [n f].
strip_truncations.
revert f. revert P.
induction n; intros P f.
- ∃ ∅.
apply path_forall; intro a; simpl.
apply path_iff_hprop; [ | contradiction ].
intros p.
apply (f (a;p)).
- destruct (split P n f) as
(P' & b & HP' & HP).
destruct (IHn P' HP') as [Y HY].
∃ (Y ∪ {|b|}).
apply path_forall; intro a. simpl.
rewrite <- HY.
apply HP.
Defined.
End bfin_kfin.
Section kfin_bfin.
Variable (A : Type).
Context `{DecidablePaths A} `{Univalence}.
Lemma notIn_ext_union_singleton (b : A) (Y : Sub A) :
¬ (b ∈ Y) →
{a : A & a ∈ ({|b|} ∪ Y)} <~> {a : A & a ∈ Y} + Unit.
Proof.
intros HYb.
unshelve eapply BuildEquiv.
- intros [a Ha]. cbn in Ha.
destruct (dec (BuildhProp (a = b))) as [Hab | Hab].
+ apply (inr tt).
+ refine (inl(a;_)).
strip_truncations.
destruct Ha as [HXa | HYa].
× refine (Empty_rec _).
strip_truncations.
by apply Hab.
× apply HYa.
- apply isequiv_biinv.
unshelve esplit ; (unshelve eexists
; [intros [[a Ha] | []]
; [apply (a;(tr(inr Ha))) | apply (b;(tr(inl (tr idpath))))]
| ]).
+ intros [a Ha]; cbn.
strip_truncations.
simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
destruct (H a b); cbn.
× apply p^.
× reflexivity.
+ intros [[a Ha] | []]; cbn.
destruct (dec (a = b)) as [Hb | Hb]; cbn.
× refine (Empty_rec _).
rewrite Hb in Ha.
contradiction.
× reflexivity.
× destruct (dec (b = b)); [ reflexivity | contradiction ].
Defined.
Theorem bfin_union : @closedUnion A Bfin.
Proof.
intros X Y [n fX] HY.
strip_truncations.
revert fX. revert X.
induction n; intros X fX.
- rewrite (X_empty _ X fX), (neutralL_max (Sub A)).
apply HY.
- destruct (split X n fX) as
(X' & b & HX' & HX).
assert (Bfin (X'∪ Y)) by (by apply IHn).
destruct (dec (b ∈ (X' ∪ Y))) as [HX'Yb | HX'Yb].
+ cut (X ∪ Y = X' ∪ Y).
{ intros HXY. rewrite HXY. assumption. }
apply path_forall. intro a.
unfold union, sub_union, max_fun.
rewrite HX.
rewrite (commutativity (X' a)).
rewrite (associativity _ (X' a)).
apply path_iff_hprop.
× intros Ha.
strip_truncations.
destruct Ha as [HXa | HYa]; [ | assumption ].
strip_truncations.
rewrite HXa.
by apply tr.
× intros Ha.
apply (tr (inr Ha)).
+ destruct (IHn X' HX') as [n' fw].
strip_truncations.
∃ (n'.+1).
apply tr.
transitivity ({a : A & a ∈ (fun a ⇒ merely (a = b)) ∪ (X' ∪ Y)}).
× apply equiv_functor_sigma_id.
intro a.
rewrite <- (associative_max (Sub A)).
assert (X = X' ∪ (fun a ⇒ merely (a = b))) as HX_.
** apply path_forall. intros ?.
unfold union, sub_union, max_fun.
apply HX.
** rewrite HX_, <- (commutative_max (Sub A) X').
reflexivity.
× etransitivity.
{ apply (notIn_ext_union_singleton b _ HX'Yb). }
by rewrite ((equiv_path _ _)^-1 fw).
Defined.
Definition FSet_to_Bfin : ∀ (X : FSet A), Bfin (map X).
Proof.
hinduction; try (intros; apply path_ishprop).
- ∃ 0.
apply tr.
simple refine (BuildEquiv _ _ _ _).
destruct 1 as [? []].
- apply _.
- intros.
apply bfin_union ; assumption.
Defined.
End kfin_bfin.
Global Instance Kf_to_Bf (X : Type) `{Univalence} `{DecidablePaths X} (Hfin : Kf X) : Finite X.
Proof.
destruct (Kf_unfold _ Hfin) as [Y HY].
simple refine (finite_equiv' _ _ (FSet_to_Bfin _ Y)).
unshelve esplit.
- apply (fun z ⇒ z.1).
- apply isequiv_biinv.
split.
× ∃ (fun a ⇒ (a;HY a)).
intros [b Hb].
apply path_sigma' with idpath.
apply path_ishprop.
× refine (fun a ⇒ (a;HY a);fun _ ⇒ _).
reflexivity.
Defined.
Require Import FSets interfaces.lattice_interface.
From subobjects Require Import sub k_finite.
Section finite_hott.
Variable (A : Type).
Context `{Univalence}.
Definition Bfin (X : Sub A) : hProp := BuildhProp (Finite {a : A & a ∈ X}).
Global Instance singleton_contr a `{IsHSet A} : Contr {b : A & b ∈ {|a|}}.
Proof.
∃ (a; tr idpath).
intros [b p].
simple refine (Trunc_ind (fun p ⇒ (a; tr 1%path) = (b; p)) _ p).
clear p; intro p ; simpl.
apply path_sigma_hprop; simpl.
apply p^.
Defined.
Definition singleton_fin_equiv' a : Fin 1 → {b : A & b ∈ {|a|}}.
Proof.
intros _. apply (a; tr idpath).
Defined.
Global Instance singleton_fin_equiv a `{IsHSet A} : IsEquiv (singleton_fin_equiv' a).
Proof. apply _. Defined.
Definition singleton `{IsHSet A} : closedSingleton Bfin.
Proof.
intros a.
simple refine (Build_Finite _ 1 _).
apply tr.
symmetry.
refine (BuildEquiv _ _ (singleton_fin_equiv' a) _).
Defined.
Definition empty_finite : closedEmpty Bfin.
Proof.
simple refine (Build_Finite _ 0 _).
apply tr.
simple refine (BuildEquiv _ _ _ _).
intros [a p]; apply p.
Defined.
Definition decidable_empty_finite : hasDecidableEmpty Bfin.
Proof.
intros X [n f].
strip_truncations.
destruct n.
- refine (tr(inl _)).
apply path_forall. intro z.
apply path_iff_hprop.
× intros p.
contradiction (f (z;p)).
× contradiction.
- refine (tr(inr _)).
apply (tr(f^-1(inr tt))).
Defined.
Lemma no_union `{IsHSet A}
(U : ∀ (X Y : Sub A),
Bfin X → Bfin Y → Bfin (X ∪ Y))
: DecidablePaths A.
Proof.
intros a b.
destruct (U {|a|} {|b|} (singleton a) (singleton b)) as [n pn].
strip_truncations.
unfold Sect in ×.
destruct pn as [f [g fg gf _]], n as [ | [ | n]].
- contradiction f.
∃ a.
apply (tr(inl(tr idpath))).
- refine (inl _).
pose (s1 := (a;tr(inl(tr idpath)))
: {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
pose (s2 := (b;tr(inr(tr idpath)))
: {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
refine (ap (fun x ⇒ x.1) (gf s1)^ @ _ @ (ap (fun x ⇒ x.1) (gf s2))).
assert (fs_eq : f s1 = f s2).
{ by apply path_ishprop. }
refine (ap (fun x ⇒ (g x).1) fs_eq).
-
refine (inr (fun p ⇒ _)).
pose (s1 := inl (inr tt) : Fin n + Unit + Unit).
pose (s2 := inr tt : Fin n + Unit + Unit).
pose (gs1 := g s1).
pose (c := gs1).
pose (gs2 := g s2).
pose (d := gs2).
assert (Hgs1 : gs1 = c) by reflexivity.
assert (Hgs2 : gs2 = d) by reflexivity.
destruct c as [x px'], d as [y py'].
simple refine (Trunc_ind _ _ px') ; intros px
; simple refine (Trunc_ind _ _ py') ; intros py ; simpl.
enough (s1 = s2) as X.
{
unfold s1, s2 in X.
contradiction (inl_ne_inr _ _ X).
}
refine ((fg s1)^ @ ap f (Hgs1 @ _ @ Hgs2^) @ fg s2).
simple refine (path_sigma _ _ _ _ _); [ | apply path_ishprop ]; simpl.
destruct px as [px | px] ; destruct py as [py | py]
; refine (Trunc_rec _ px) ; clear px ; intro px
; refine (Trunc_rec _ py) ; clear py ; intro py.
× apply (px @ py^).
× refine (px @ p @ py^).
× refine (px @ p^ @ py^).
× apply (px @ py^).
Defined.
End finite_hott.
Section singleton_set.
Variable (A : Type).
Context `{Univalence}.
Variable (HA : ∀ a, {b : A & b ∈ {|a|}} <~> Fin 1).
Definition el x : {b : A & b ∈ {|x|}} := (x;tr idpath).
Theorem single_bfin_set : ∀ (x : A) (p : x = x), p = idpath.
Proof.
intros x p.
specialize (HA x).
pose (el x) as X.
pose (ap HA^-1 (ap HA (path_sigma _ X X p (path_ishprop _ _)))) as q.
assert (p = ap (fun z ⇒ z.1) ((eissect HA X)^ @ q @ eissect HA X)) as H1.
{
unfold q.
rewrite <- ap_compose.
enough(∀ r,
(eissect HA X)^
@ ap (fun x0 : {b : A & b ∈ {|x|}} ⇒ HA^-1 (HA x0)) r
@ eissect HA X = r
) as H2.
{
rewrite H2.
refine (@pr1_path_sigma _ _ X X p _)^.
}
induction r.
hott_simpl.
}
assert (idpath = ap (fun z ⇒ z.1) ((eissect HA X)^ @ idpath @ eissect HA X)) as H2.
{ hott_simpl. }
rewrite H1, H2.
repeat f_ap.
unfold q.
enough (ap HA (path_sigma (fun b : A ⇒ b ∈ {|x|}) X X p (path_ishprop _ _)) = idpath) as H3.
{
rewrite H3.
reflexivity.
}
apply path_ishprop.
Defined.
Global Instance set_singleton : IsHSet A.
Proof.
refine hset_axiomK.
unfold axiomK.
apply single_bfin_set.
Defined.
End singleton_set.
Section empty.
Variable (A : Type).
Variable (X : A → hProp)
(Xequiv : {a : A & a ∈ X} <~> Fin 0).
Context `{Univalence}.
Lemma X_empty : X = ∅.
Proof.
apply path_forall.
intro z.
apply path_iff_hprop ; try contradiction.
intro x.
destruct Xequiv as [f fequiv].
contradiction (f(z;x)).
Defined.
End empty.
Section split.
Context `{Univalence}.
Variable (A : Type).
Variable (P : A → hProp)
(n : nat)
(f : {a : A & P a } <~> Fin n + Unit).
Definition split : ∃ P' : Sub A, ∃ b : A,
({a : A & P' a} <~> Fin n) × (∀ x, P x = (P' x ∨ merely (x = b))).
Proof.
pose (fun x : A ⇒ sig (fun y : Fin n ⇒ x = (f^-1 (inl y)).1)) as P'.
assert (∀ x, IsHProp (P' x)).
{
intros a. unfold P'.
apply hprop_allpath.
intros [x px] [y py].
pose (p := px^ @ py).
assert (p2 : p # (f^-1 (inl x)).2 = (f^-1 (inl y)).2).
{ apply path_ishprop. }
simple refine (path_sigma' _ _ _).
- apply path_sum_inl with Unit.
refine (transport (fun z ⇒ z = inl y) (eisretr f (inl x)) _).
refine (transport (fun z ⇒ _ = z) (eisretr f (inl y)) _).
apply (ap f).
apply path_sigma_hprop. apply p.
- rewrite transport_paths_FlFr.
hott_simpl; cbn.
rewrite ap_compose, (ap_compose inl f^-1).
rewrite ap_inl_path_sum_inl.
repeat (rewrite transport_paths_FlFr; hott_simpl).
rewrite !ap_pp.
rewrite ap_V.
rewrite <- !other_adj.
rewrite <- (ap_compose f (f^-1)).
rewrite ap_equiv.
rewrite !ap_pp.
rewrite ap_pr1_path_sigma_hprop.
rewrite !concat_pp_p.
rewrite !ap_V.
rewrite concat_Vp.
rewrite (concat_p_pp (ap pr1 (eissect f (f^-1 (inl x))))^).
rewrite concat_Vp.
hott_simpl.
}
∃ (fun a ⇒ BuildhProp (P' a)).
∃ (f^-1 (inr tt)).1.
split.
{ unshelve eapply BuildEquiv.
{ refine (fun x ⇒ x.2.1). }
apply isequiv_biinv.
unshelve esplit;
∃ (fun x ⇒ (((f^-1 (inl x)).1; (x; idpath)))).
- intros [a [y p]]; cbn.
eapply path_sigma with p^.
apply path_ishprop.
- intros x.
reflexivity.
}
{ intros a.
unfold P'.
apply path_iff_hprop.
- intros Ha.
pose (y := f (a;Ha)).
assert (Hy : y = f (a; Ha)) by reflexivity.
destruct y as [y | []].
+ refine (tr (inl _)).
∃ y.
rewrite Hy.
by rewrite eissect.
+ refine (tr (inr (tr _))).
rewrite Hy.
by rewrite eissect.
- intros Hstuff.
strip_truncations.
destruct Hstuff as [[y Hy] | Ha].
+ rewrite Hy.
apply (f^-1 (inl y)).2.
+ strip_truncations.
rewrite Ha.
apply (f^-1 (inr tt)).2. }
Defined.
End split.
Arguments Bfin {_} _.
Arguments split {_} {_} _ _ _.
Section Bfin_no_singletons.
Definition S1toSig (x : S1) : {x : S1 & merely(x = base)}.
Proof.
∃ x.
simple refine (S1_ind (fun z ⇒ merely(z = base)) (tr idpath) _ x).
apply path_ishprop.
Defined.
Instance S1toSig_equiv : IsEquiv S1toSig.
Proof.
apply isequiv_biinv.
split.
- ∃ (fun x ⇒ x.1).
simple refine (S1_ind _ idpath _) ; simpl.
rewrite transport_paths_FlFr.
hott_simpl.
- ∃ (fun x ⇒ x.1).
intros [z x].
simple refine (path_sigma _ _ _ _ _) ; simpl.
× reflexivity.
× apply path_ishprop.
Defined.
Theorem no_singleton `{Univalence} (Hsing : Bfin {|base|}) : Empty.
Proof.
destruct Hsing as [n equiv].
strip_truncations.
assert (S1 <~> Fin n) as X.
{ apply (equiv_compose equiv S1toSig). }
assert (IsHSet S1) as X1.
{
rewrite (path_universe X).
apply _.
}
enough (idpath = loop).
- assert (S1_encode _ idpath = S1_encode _ (loopexp loop (pos Int.one))) as H' by f_ap.
rewrite S1_encode_loopexp in H'. simpl in H'. symmetry in H'.
apply (pos_neq_zero H').
- apply set_path2.
Defined.
End Bfin_no_singletons.
Section dec_membership.
Variable (A : Type).
Context `{MerelyDecidablePaths A} `{Univalence}.
Global Instance DecidableMembership (P : Sub A) (Hfin : Bfin P) (a : A) :
Decidable (a ∈ P).
Proof.
destruct Hfin as [n Hequiv].
strip_truncations.
revert Hequiv.
revert P.
induction n.
- intros.
pose (X_empty _ P Hequiv) as p.
rewrite p.
apply _.
- intros.
destruct (split P n Hequiv) as
(P' & b & HP' & HP).
unfold member, sub_membership.
rewrite (HP a).
destruct (IHn P' HP') as [IH | IH].
× apply (inl (tr (inl IH))).
× destruct (m_dec_path a b) as [Hab | Hab].
+ apply (inl (tr (inr Hab))).
+ refine (inr(fun a ⇒ _)).
strip_truncations.
destruct a as [? | t] ; [ | strip_truncations] ; try contradiction.
contradiction (Hab (tr t)).
Defined.
End dec_membership.
Section bfin_kfin.
Context `{Univalence}.
Lemma bfin_to_kfin : ∀ (B : Type), Finite B → Kf B.
Proof.
apply finite_ind_hprop.
- apply _.
- apply Kf_unfold.
∃ ∅. intros [].
- intros B [n f] IH.
apply Kf_sum ; try assumption.
apply Kf_Unit.
Defined.
Definition bfin_to_kfin_sub A : ∀ (P : Sub A), Bfin P → Kf_sub _ P.
Proof.
intros P [n f].
strip_truncations.
revert f. revert P.
induction n; intros P f.
- ∃ ∅.
apply path_forall; intro a; simpl.
apply path_iff_hprop; [ | contradiction ].
intros p.
apply (f (a;p)).
- destruct (split P n f) as
(P' & b & HP' & HP).
destruct (IHn P' HP') as [Y HY].
∃ (Y ∪ {|b|}).
apply path_forall; intro a. simpl.
rewrite <- HY.
apply HP.
Defined.
End bfin_kfin.
Section kfin_bfin.
Variable (A : Type).
Context `{DecidablePaths A} `{Univalence}.
Lemma notIn_ext_union_singleton (b : A) (Y : Sub A) :
¬ (b ∈ Y) →
{a : A & a ∈ ({|b|} ∪ Y)} <~> {a : A & a ∈ Y} + Unit.
Proof.
intros HYb.
unshelve eapply BuildEquiv.
- intros [a Ha]. cbn in Ha.
destruct (dec (BuildhProp (a = b))) as [Hab | Hab].
+ apply (inr tt).
+ refine (inl(a;_)).
strip_truncations.
destruct Ha as [HXa | HYa].
× refine (Empty_rec _).
strip_truncations.
by apply Hab.
× apply HYa.
- apply isequiv_biinv.
unshelve esplit ; (unshelve eexists
; [intros [[a Ha] | []]
; [apply (a;(tr(inr Ha))) | apply (b;(tr(inl (tr idpath))))]
| ]).
+ intros [a Ha]; cbn.
strip_truncations.
simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
destruct (H a b); cbn.
× apply p^.
× reflexivity.
+ intros [[a Ha] | []]; cbn.
destruct (dec (a = b)) as [Hb | Hb]; cbn.
× refine (Empty_rec _).
rewrite Hb in Ha.
contradiction.
× reflexivity.
× destruct (dec (b = b)); [ reflexivity | contradiction ].
Defined.
Theorem bfin_union : @closedUnion A Bfin.
Proof.
intros X Y [n fX] HY.
strip_truncations.
revert fX. revert X.
induction n; intros X fX.
- rewrite (X_empty _ X fX), (neutralL_max (Sub A)).
apply HY.
- destruct (split X n fX) as
(X' & b & HX' & HX).
assert (Bfin (X'∪ Y)) by (by apply IHn).
destruct (dec (b ∈ (X' ∪ Y))) as [HX'Yb | HX'Yb].
+ cut (X ∪ Y = X' ∪ Y).
{ intros HXY. rewrite HXY. assumption. }
apply path_forall. intro a.
unfold union, sub_union, max_fun.
rewrite HX.
rewrite (commutativity (X' a)).
rewrite (associativity _ (X' a)).
apply path_iff_hprop.
× intros Ha.
strip_truncations.
destruct Ha as [HXa | HYa]; [ | assumption ].
strip_truncations.
rewrite HXa.
by apply tr.
× intros Ha.
apply (tr (inr Ha)).
+ destruct (IHn X' HX') as [n' fw].
strip_truncations.
∃ (n'.+1).
apply tr.
transitivity ({a : A & a ∈ (fun a ⇒ merely (a = b)) ∪ (X' ∪ Y)}).
× apply equiv_functor_sigma_id.
intro a.
rewrite <- (associative_max (Sub A)).
assert (X = X' ∪ (fun a ⇒ merely (a = b))) as HX_.
** apply path_forall. intros ?.
unfold union, sub_union, max_fun.
apply HX.
** rewrite HX_, <- (commutative_max (Sub A) X').
reflexivity.
× etransitivity.
{ apply (notIn_ext_union_singleton b _ HX'Yb). }
by rewrite ((equiv_path _ _)^-1 fw).
Defined.
Definition FSet_to_Bfin : ∀ (X : FSet A), Bfin (map X).
Proof.
hinduction; try (intros; apply path_ishprop).
- ∃ 0.
apply tr.
simple refine (BuildEquiv _ _ _ _).
destruct 1 as [? []].
- apply _.
- intros.
apply bfin_union ; assumption.
Defined.
End kfin_bfin.
Global Instance Kf_to_Bf (X : Type) `{Univalence} `{DecidablePaths X} (Hfin : Kf X) : Finite X.
Proof.
destruct (Kf_unfold _ Hfin) as [Y HY].
simple refine (finite_equiv' _ _ (FSet_to_Bfin _ Y)).
unshelve esplit.
- apply (fun z ⇒ z.1).
- apply isequiv_biinv.
split.
× ∃ (fun a ⇒ (a;HY a)).
intros [b Hb].
apply path_sigma' with idpath.
apply path_ishprop.
× refine (fun a ⇒ (a;HY a);fun _ ⇒ _).
reflexivity.
Defined.