dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-04 07:33:51 +01:00
Code Issues Releases Wiki Activity

Further simplifications in interface

Browse Source
This commit is contained in:
Niels
2017-08-15 22:05:31 +02:00
parent e29e978218
commit e1bc900abc
1 changed files with 15 additions and 23 deletions
Download Patch File Download Diff File Expand all files Collapse all files

38
FiniteSets/implementations/interface.v
View File

@@ -19,13 +19,13 @@ Section interface.
f_filter : forall A φ X, f A (filter φ X) = {| f A X & φ |}; f_filter : forall A φ X, f A (filter φ X) = {| f A X & φ |};
f_member : forall A a X, member a X = a ∈ (f A X) f_member : forall A a X, member a X = a ∈ (f A X)
}. }.
Global Instance f_surjective A `{sets} : IsSurjection (f A). Global Instance f_surjective A `{sets} : IsSurjection (f A).
Proof. Proof.
unfold IsSurjection. unfold IsSurjection.
hinduction ; try (intros ; apply path_ishprop). hinduction ; try (intros ; apply path_ishprop).
- simple refine (BuildContr _ _ _). - simple refine (BuildContr _ _ _).
* refine (tr(∅;_)). * refine (tr(∅;_)).
apply f_empty. apply f_empty.
* intros ; apply path_ishprop. * intros ; apply path_ishprop.
- intro a. - intro a.
@@ -33,14 +33,10 @@ Section interface.
* refine (tr({|a|};_)). * refine (tr({|a|};_)).
apply f_singleton. apply f_singleton.
* intros ; apply path_ishprop. * intros ; apply path_ishprop.
- intros Y1 Y2 HY1 HY2. - intros Y1 Y2 [X1' ?] [X2' ?].
destruct HY1 as [X1' HX1].
destruct HY2 as [X2' HX2].
simple refine (BuildContr _ _ _). simple refine (BuildContr _ _ _).
* simple refine (Trunc_rec _ X1') ; intro X1. * simple refine (Trunc_rec _ X1') ; intros [X1 fX1].
simple refine (Trunc_rec _ X2') ; intro X2. simple refine (Trunc_rec _ X2') ; intros [X2 fX2].
destruct X1 as [X1 fX1].
destruct X2 as [X2 fX2].
refine (tr(X1 ∪ X2;_)). refine (tr(X1 ∪ X2;_)).
rewrite f_union, fX1, fX2. rewrite f_union, fX1, fX2.
reflexivity. reflexivity.
@@ -57,7 +53,7 @@ Section quotient_surjection.
Definition f_eq : relation A := fun a1 a2 => f a1 = f a2. Definition f_eq : relation A := fun a1 a2 => f a1 = f a2.
Definition quotientB : Type := quotient f_eq. Definition quotientB : Type := quotient f_eq.
Global Instance quotientB_recursion : HitRecursion quotientB := Global Instance quotientB_recursion : HitRecursion quotientB :=
{ {
indTy := _; indTy := _;
@@ -97,29 +93,26 @@ Section quotient_surjection.
Proof. Proof.
apply isembedding_isinj_hset. apply isembedding_isinj_hset.
unfold isinj. unfold isinj.
simpl.
hrecursion ; [ | intros; apply path_ishprop ]. hrecursion ; [ | intros; apply path_ishprop ].
intro. intro.
hrecursion ; [ | intros; apply path_ishprop ]. hrecursion ; [ | intros; apply path_ishprop ].
intros. intros.
by apply related_classes_eq. by apply related_classes_eq.
Defined. Defined.
Instance quotientB_surj : IsSurjection (quotientB_to_B). Instance quotientB_surj : IsSurjection (quotientB_to_B).
Proof. Proof.
apply BuildIsSurjection. apply BuildIsSurjection.
intros Y. intros Y.
destruct (H Y). destruct (H Y).
simple refine (Trunc_rec _ center) ; intro X. simple refine (Trunc_rec _ center) ; intros [a fa].
apply tr. apply (tr(class_of _ a;fa)).
destruct X as [a fa].
apply (class_of _ a;fa).
Defined. Defined.
Definition quotient_iso : quotientB <~> B. Definition quotient_iso : quotientB <~> B.
Proof. Proof.
refine (BuildEquiv _ _ quotientB_to_B _). refine (BuildEquiv _ _ quotientB_to_B _).
apply isequiv_surj_emb; apply _. apply isequiv_surj_emb ; apply _.
Defined. Defined.
Definition reflect_eq : forall (X Y : A), Definition reflect_eq : forall (X Y : A),
@@ -158,7 +151,7 @@ Section quotient_properties.
Definition set_eq A := f_eq (T A) (FSet A) (f A). Definition set_eq A := f_eq (T A) (FSet A) (f A).
Definition View A : Type := quotientB (T A) (FSet A) (f A). Definition View A : Type := quotientB (T A) (FSet A) (f A).
Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) : Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) :
(forall (x x' : T A), set_eq A x x' -> forall (y y' : T A), set_eq A y y' -> u x y = u x' y') -> (forall (x x' : T A), set_eq A x x' -> forall (y y' : T A), set_eq A y y' -> u x y = u x' y') ->
forall (x y : View A), P. forall (x y : View A), P.
@@ -210,8 +203,7 @@ Section quotient_properties.
- apply (member a). - apply (member a).
- intros X Y HXY. - intros X Y HXY.
reduce T. reduce T.
rewrite HXY. apply (ap _ HXY).
reflexivity.
Defined. Defined.
Global Instance View_empty A: hasEmpty (View A). Global Instance View_empty A: hasEmpty (View A).
@@ -232,7 +224,7 @@ Section quotient_properties.
apply (class_of _ (union a b)). apply (class_of _ (union a b)).
- intros x x' Hxx' y y' Hyy' ; simpl. - intros x x' Hxx' y y' Hyy' ; simpl.
apply related_classes_eq. apply related_classes_eq.
eapply well_defined_union; eauto. eapply well_defined_union ; eauto.
Defined. Defined.
Global Instance View_union A: hasUnion (View A). Global Instance View_union A: hasUnion (View A).
@@ -248,7 +240,7 @@ Section quotient_properties.
apply (class_of _ (filter ϕ X)). apply (class_of _ (filter ϕ X)).
- intros X X' HXX' ; simpl. - intros X X' HXX' ; simpl.
apply related_classes_eq. apply related_classes_eq.
eapply well_defined_filter; eauto. eapply well_defined_filter ; eauto.
Defined. Defined.
Hint Unfold Commutative Associative Idempotent NeutralL NeutralR. Hint Unfold Commutative Associative Idempotent NeutralL NeutralR.
@@ -318,7 +310,7 @@ Section properties.
class_of (set_eq f) ({|X & ϕ|}) = {|(class_of (set_eq f) X) & ϕ|}. class_of (set_eq f) ({|X & ϕ|}) = {|(class_of (set_eq f) X) & ϕ|}.
Proof. Proof.
reflexivity. reflexivity.
Defined. Defined.
Ltac via_quotient := intros ; apply reflect_f_eq Ltac via_quotient := intros ; apply reflect_f_eq
; rewrite ?class_union, ?class_filter ; rewrite ?class_union, ?class_filter