dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

If Bfin has union, then decidable paths

This commit is contained in:
Niels van der Weide 2017-10-04 15:01:15 +02:00
parent b638c2592d
commit c7df8ae8aa
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
FiniteSets/subobjects/b_finite.v
View File

@ -64,7 +64,7 @@ Section finite_hott.
Lemma no_union `{IsHSet A} Lemma no_union `{IsHSet A}
(f : forall (X Y : Sub A), (f : forall (X Y : Sub A),
Bfin X -> Bfin Y -> Bfin (X ∪ Y)) Bfin X -> Bfin Y -> Bfin (X ∪ Y))
: MerelyDecidablePaths A. : DecidablePaths A.
Proof. Proof.
intros a b. intros a b.
specialize (f {|a|} {|b|} (singleton a) (singleton b)). specialize (f {|a|} {|b|} (singleton a) (singleton b)).
@ -78,7 +78,7 @@ Section finite_hott.
exists a. apply (tr(inl(tr idpath))). exists a. apply (tr(inl(tr idpath))).
- destruct n as [|n]. - destruct n as [|n].
+ (* If the size of the union is 1, then (a = b) *) + (* If the size of the union is 1, then (a = b) *)
refine (inl (tr _)). refine (inl _).
pose (s1 := (a;tr(inl(tr idpath))) pose (s1 := (a;tr(inl(tr idpath)))
: {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}). : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
pose (s2 := (b;tr(inr(tr idpath))) pose (s2 := (b;tr(inr(tr idpath)))
@ -89,7 +89,6 @@ Section finite_hott.
refine (ap (fun x => (g x).1) fs_eq). refine (ap (fun x => (g x).1) fs_eq).
+ (* Otherwise, ¬(a = b) *) + (* Otherwise, ¬(a = b) *)
refine (inr (fun p => _)). refine (inr (fun p => _)).
strip_truncations.
pose (s1 := inl (inr tt) : Fin n + Unit + Unit). pose (s1 := inl (inr tt) : Fin n + Unit + Unit).
pose (s2 := inr tt : Fin n + Unit + Unit). pose (s2 := inr tt : Fin n + Unit + Unit).
pose (gs1 := g s1). pose (gs1 := g s1).