mirror of https://github.com/nmvdw/HITs-Examples
Improved interface.v
This commit is contained in:
Niels
parent
06701dcdf8
commit
e29e978218
|
|
@ -19,69 +19,179 @@ Section interface.
|
|||
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)
|
||||
}.
|
||||
|
||||
Global Instance f_surjective A `{sets} : IsSurjection (f A).
|
||||
Proof.
|
||||
unfold IsSurjection.
|
||||
hinduction ; try (intros ; apply path_ishprop).
|
||||
- simple refine (BuildContr _ _ _).
|
||||
* refine (tr(∅;_)).
|
||||
apply f_empty.
|
||||
* intros ; apply path_ishprop.
|
||||
- intro a.
|
||||
simple refine (BuildContr _ _ _).
|
||||
* refine (tr({|a|};_)).
|
||||
apply f_singleton.
|
||||
* intros ; apply path_ishprop.
|
||||
- intros Y1 Y2 HY1 HY2.
|
||||
destruct HY1 as [X1' HX1].
|
||||
destruct HY2 as [X2' HX2].
|
||||
simple refine (BuildContr _ _ _).
|
||||
* simple refine (Trunc_rec _ X1') ; intro X1.
|
||||
simple refine (Trunc_rec _ X2') ; intro X2.
|
||||
destruct X1 as [X1 fX1].
|
||||
destruct X2 as [X2 fX2].
|
||||
refine (tr(X1 ∪ X2;_)).
|
||||
rewrite f_union, fX1, fX2.
|
||||
reflexivity.
|
||||
* intros ; apply path_ishprop.
|
||||
Defined.
|
||||
|
||||
End interface.
|
||||
|
||||
Section properties.
|
||||
Context `{Univalence}.
|
||||
Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
|
||||
Section quotient_surjection.
|
||||
Variable (A B : Type)
|
||||
(f : A -> B)
|
||||
(H : IsSurjection f).
|
||||
Context `{IsHSet B} `{Univalence}.
|
||||
|
||||
Definition f_eq : relation A := fun a1 a2 => f a1 = f a2.
|
||||
Definition quotientB : Type := quotient f_eq.
|
||||
|
||||
Global Instance quotientB_recursion : HitRecursion quotientB :=
|
||||
{
|
||||
indTy := _;
|
||||
recTy :=
|
||||
forall (P : Type) (HP: IsHSet P) (u : A -> P),
|
||||
(forall x y : A, f_eq x y -> u x = u y) -> quotientB -> P;
|
||||
H_inductor := quotient_ind f_eq ;
|
||||
H_recursor := @quotient_rec _ f_eq _
|
||||
}.
|
||||
|
||||
Global Instance R_refl : Reflexive f_eq.
|
||||
Proof.
|
||||
intro.
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Global Instance R_sym : Symmetric f_eq.
|
||||
Proof.
|
||||
intros a b Hab.
|
||||
apply (Hab^).
|
||||
Defined.
|
||||
|
||||
Global Instance R_trans : Transitive f_eq.
|
||||
Proof.
|
||||
intros a b c Hab Hbc.
|
||||
apply (Hab @ Hbc).
|
||||
Defined.
|
||||
|
||||
Definition quotientB_to_B : quotientB -> B.
|
||||
Proof.
|
||||
hrecursion.
|
||||
- apply f.
|
||||
- done.
|
||||
Defined.
|
||||
|
||||
Instance quotientB_emb : IsEmbedding (quotientB_to_B).
|
||||
Proof.
|
||||
apply isembedding_isinj_hset.
|
||||
unfold isinj.
|
||||
simpl.
|
||||
hrecursion ; [ | intros; apply path_ishprop ].
|
||||
intro.
|
||||
hrecursion ; [ | intros; apply path_ishprop ].
|
||||
intros.
|
||||
by apply related_classes_eq.
|
||||
Defined.
|
||||
|
||||
Instance quotientB_surj : IsSurjection (quotientB_to_B).
|
||||
Proof.
|
||||
apply BuildIsSurjection.
|
||||
intros Y.
|
||||
destruct (H Y).
|
||||
simple refine (Trunc_rec _ center) ; intro X.
|
||||
apply tr.
|
||||
destruct X as [a fa].
|
||||
apply (class_of _ a;fa).
|
||||
Defined.
|
||||
|
||||
Definition quotient_iso : quotientB <~> B.
|
||||
Proof.
|
||||
refine (BuildEquiv _ _ quotientB_to_B _).
|
||||
apply isequiv_surj_emb; apply _.
|
||||
Defined.
|
||||
|
||||
Definition reflect_eq : forall (X Y : A),
|
||||
f X = f Y -> f_eq X Y.
|
||||
Proof.
|
||||
done.
|
||||
Defined.
|
||||
|
||||
Lemma same_class : forall (X Y : A),
|
||||
class_of f_eq X = class_of f_eq Y -> f_eq X Y.
|
||||
Proof.
|
||||
intros.
|
||||
simple refine (classes_eq_related _ _ _ _) ; assumption.
|
||||
Defined.
|
||||
|
||||
End quotient_surjection.
|
||||
|
||||
Ltac reduce T :=
|
||||
intros ;
|
||||
repeat (rewrite (f_empty T _)
|
||||
|| rewrite (f_singleton T _)
|
||||
|| rewrite (f_union T _)
|
||||
|| rewrite (f_filter T _)
|
||||
|| rewrite (f_member T _)).
|
||||
Ltac simplify T := intros ; autounfold in * ; apply reflect_eq ; reduce T.
|
||||
Ltac reflect_equality T := simplify T ; eauto with lattice_hints typeclass_instances.
|
||||
Ltac reflect_eq T := autounfold
|
||||
; repeat (hinduction ; try (intros ; apply path_ishprop) ; intro)
|
||||
; apply related_classes_eq
|
||||
; reflect_equality T.
|
||||
|
||||
Section quotient_properties.
|
||||
Variable (T : Type -> Type).
|
||||
Variable (f : forall {A : Type}, T A -> FSet A).
|
||||
Context `{sets T f}.
|
||||
|
||||
Definition set_eq : forall A, T A -> T A -> hProp :=
|
||||
fun A X Y => (BuildhProp (f A X = f A Y)).
|
||||
Definition set_eq A := f_eq (T A) (FSet A) (f A).
|
||||
Definition View A : Type := quotientB (T A) (FSet A) (f A).
|
||||
|
||||
Definition set_subset : forall A, T A -> T A -> hProp :=
|
||||
fun A X Y => (f A X) ⊆ (f A Y).
|
||||
|
||||
Ltac reduce :=
|
||||
intros ;
|
||||
repeat (rewrite (f_empty T _)
|
||||
|| rewrite (f_singleton T _)
|
||||
|| rewrite (f_union T _)
|
||||
|| rewrite (f_filter T _)
|
||||
|| rewrite (f_member T _)).
|
||||
|
||||
Definition empty_isIn : forall (A : Type) (a : A),
|
||||
a ∈ ∅ = False_hp.
|
||||
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 y : View A), P.
|
||||
Proof.
|
||||
by reduce.
|
||||
intros Hresp.
|
||||
assert (resp1 : forall x y y', set_eq A y y' -> u x y = u x y').
|
||||
{ intros x y y'.
|
||||
apply (Hresp _ _ idpath).
|
||||
}
|
||||
assert (resp2 : forall x x' y, set_eq A x x' -> u x y = u x' y).
|
||||
{ intros x x' y Hxx'.
|
||||
apply Hresp. apply Hxx'.
|
||||
reflexivity. }
|
||||
unfold View.
|
||||
hrecursion.
|
||||
- intros a.
|
||||
hrecursion.
|
||||
+ intros b.
|
||||
apply (u a b).
|
||||
+ intros b b' Hbb'. simpl.
|
||||
by apply resp1.
|
||||
- intros a a' Haa'. simpl.
|
||||
apply path_forall. red.
|
||||
hinduction.
|
||||
+ intros b. apply resp2. apply Haa'.
|
||||
+ intros; apply HP.
|
||||
Defined.
|
||||
|
||||
Definition singleton_isIn : forall (A : Type) (a b : A),
|
||||
a ∈ {|b|} = merely (a = b).
|
||||
Proof.
|
||||
by reduce.
|
||||
Defined.
|
||||
|
||||
Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
|
||||
a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y).
|
||||
Proof.
|
||||
by reduce.
|
||||
Defined.
|
||||
|
||||
Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
|
||||
member a (filter ϕ X) = if ϕ a then member a X else False_hp.
|
||||
Proof.
|
||||
reduce.
|
||||
apply properties.comprehension_isIn.
|
||||
Defined.
|
||||
|
||||
Definition reflect_eq : forall (A : Type) (X Y : T A),
|
||||
f A X = f A Y -> set_eq A X Y.
|
||||
Proof. done. Defined.
|
||||
|
||||
Definition reflect_subset : forall (A : Type) (X Y : T A),
|
||||
subset (f A X) (f A Y) -> set_subset A X Y.
|
||||
Proof. done. Defined.
|
||||
|
||||
Hint Unfold set_eq set_subset.
|
||||
|
||||
Ltac simplify := intros ; autounfold in * ; apply reflect_eq ; reduce.
|
||||
|
||||
Definition well_defined_union (A : Type) (X1 X2 Y1 Y2 : T A) :
|
||||
set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
|
||||
Proof.
|
||||
intros HXY1 HXY2.
|
||||
simplify.
|
||||
simplify T.
|
||||
by rewrite HXY1, HXY2.
|
||||
Defined.
|
||||
|
||||
|
|
@ -89,241 +199,153 @@ Section properties.
|
|||
set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
|
||||
Proof.
|
||||
intros HXY.
|
||||
simplify.
|
||||
simplify T.
|
||||
by rewrite HXY.
|
||||
Defined.
|
||||
|
||||
Ltac reflect_equality := simplify ; eauto with lattice_hints typeclass_instances.
|
||||
|
||||
Lemma union_comm : forall A (X Y : T A),
|
||||
set_eq A (X ∪ Y) (Y ∪ X).
|
||||
Global Instance View_member A: hasMembership (View A) A.
|
||||
Proof.
|
||||
reflect_equality.
|
||||
intros a ; unfold View.
|
||||
hrecursion.
|
||||
- apply (member a).
|
||||
- intros X Y HXY.
|
||||
reduce T.
|
||||
rewrite HXY.
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Lemma union_assoc : forall A (X Y Z : T A),
|
||||
set_eq A ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)).
|
||||
Global Instance View_empty A: hasEmpty (View A).
|
||||
Proof.
|
||||
reflect_equality.
|
||||
apply (class_of _ ∅).
|
||||
Defined.
|
||||
|
||||
Lemma union_idem : forall A (X : T A),
|
||||
set_eq A (X ∪ X) X.
|
||||
Global Instance View_singleton A: hasSingleton (View A) A.
|
||||
Proof.
|
||||
reflect_equality.
|
||||
intros a.
|
||||
apply (class_of _ {|a|}).
|
||||
Defined.
|
||||
|
||||
Lemma union_neutral : forall A (X : T A),
|
||||
set_eq A (∅ ∪ X) X.
|
||||
Instance View_max A : maximum (View A).
|
||||
Proof.
|
||||
reflect_equality.
|
||||
simple refine (View_rec2 _ _ _ _).
|
||||
- intros a b.
|
||||
apply (class_of _ (union a b)).
|
||||
- intros x x' Hxx' y y' Hyy' ; simpl.
|
||||
apply related_classes_eq.
|
||||
eapply well_defined_union; eauto.
|
||||
Defined.
|
||||
|
||||
End properties.
|
||||
Global Instance View_union A: hasUnion (View A).
|
||||
Proof.
|
||||
apply max_L.
|
||||
Defined.
|
||||
|
||||
Section quot.
|
||||
Variable (T : Type -> Type).
|
||||
Variable (f : forall {A : Type}, T A -> FSet A).
|
||||
Context `{sets T f}.
|
||||
Global Instance View_comprehension A: hasComprehension (View A) A.
|
||||
Proof.
|
||||
intros ϕ ; unfold View.
|
||||
hrecursion.
|
||||
- intros X.
|
||||
apply (class_of _ (filter ϕ X)).
|
||||
- intros X X' HXX' ; simpl.
|
||||
apply related_classes_eq.
|
||||
eapply well_defined_filter; eauto.
|
||||
Defined.
|
||||
|
||||
Definition R A : relation (T A) := set_eq T f A.
|
||||
Definition View A : Type := quotient (R A).
|
||||
Hint Unfold Commutative Associative Idempotent NeutralL NeutralR.
|
||||
|
||||
Arguments f {_} _.
|
||||
Instance bottom_view A : bottom (View A).
|
||||
Proof.
|
||||
unfold bottom.
|
||||
apply ∅.
|
||||
Defined.
|
||||
|
||||
Instance R_refl A : Reflexive (R A).
|
||||
Proof. intro. reflexivity. Defined.
|
||||
Global Instance view_lattice A : JoinSemiLattice (View A).
|
||||
Proof.
|
||||
split ; reflect_eq T.
|
||||
Defined.
|
||||
|
||||
Instance R_sym A : Symmetric (R A).
|
||||
Proof. intros a b Hab. apply (Hab^). Defined.
|
||||
|
||||
Instance R_trans A: Transitive (R A).
|
||||
Proof. intros a b c Hab Hbc. apply (Hab @ Hbc). Defined.
|
||||
|
||||
(* Instance quotient_recursion `{A : Type} (Q : relation A) `{is_mere_relation _ Q} : HitRecursion (quotient Q) := *)
|
||||
(* { *)
|
||||
(* indTy := _; recTy := _; *)
|
||||
(* H_inductor := quotient_ind Q; H_recursor := quotient_rec Q *)
|
||||
(* }. *)
|
||||
|
||||
Instance View_recursion A : HitRecursion (View A) :=
|
||||
{
|
||||
indTy := _; recTy := forall (P : Type) (HP: IsHSet P) (u : T A -> P), (forall x y : T A, set_eq T (@f) A x y -> u x = u y) -> View A -> P;
|
||||
H_inductor := quotient_ind (R A); H_recursor := @quotient_rec _ (R A) _
|
||||
}.
|
||||
End quotient_properties.
|
||||
|
||||
Arguments set_eq {_} _ {_} _ _.
|
||||
|
||||
Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) :
|
||||
(forall (x x' : T A), set_eq (@f) x x' -> forall (y y' : T A), set_eq (@f) y y' -> u x y = u x' y') ->
|
||||
forall (x y : View A), P.
|
||||
Proof.
|
||||
intros Hresp.
|
||||
assert (resp1 : forall x y y', set_eq (@f) y y' -> u x y = u x y').
|
||||
{ intros x y y'.
|
||||
apply Hresp.
|
||||
reflexivity. }
|
||||
assert (resp2 : forall x x' y, set_eq (@f) x x' -> u x y = u x' y).
|
||||
{ intros x x' y Hxx'.
|
||||
apply Hresp. apply Hxx'.
|
||||
reflexivity. }
|
||||
hrecursion.
|
||||
- intros a.
|
||||
hrecursion.
|
||||
+ intros b.
|
||||
apply (u a b).
|
||||
+ intros b b' Hbb'. simpl.
|
||||
by apply resp1.
|
||||
- intros a a' Haa'. simpl.
|
||||
apply path_forall. red.
|
||||
hinduction.
|
||||
+ intros b. apply resp2. apply Haa'.
|
||||
+ intros; apply HP.
|
||||
Defined.
|
||||
Section properties.
|
||||
Context `{Univalence}.
|
||||
Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
|
||||
Context `{sets T f}.
|
||||
|
||||
Instance View_max A : maximum (View A).
|
||||
Proof.
|
||||
compute-[View].
|
||||
simple refine (View_rec2 _ _ _ _).
|
||||
- intros a b. apply class_of. apply (union a b).
|
||||
- intros x x' Hxx' y y' Hyy'. simpl.
|
||||
apply related_classes_eq.
|
||||
unfold R in *.
|
||||
eapply well_defined_union; eauto.
|
||||
Defined.
|
||||
Definition set_subset : forall A, T A -> T A -> hProp :=
|
||||
fun A X Y => (f A X) ⊆ (f A Y).
|
||||
|
||||
Ltac reduce :=
|
||||
intros ;
|
||||
repeat (rewrite (f_empty T _)
|
||||
|| rewrite (f_singleton T _)
|
||||
|| rewrite (f_union T _)
|
||||
|| rewrite (f_filter T _)
|
||||
|| rewrite (f_member T _)).
|
||||
Definition empty_isIn : forall (A : Type) (a : A),
|
||||
a ∈ ∅ = False_hp.
|
||||
Proof.
|
||||
by (reduce T).
|
||||
Defined.
|
||||
|
||||
Instance View_member A: hasMembership (View A) A.
|
||||
Proof.
|
||||
intros a.
|
||||
hrecursion.
|
||||
- apply (member a).
|
||||
- intros X Y HXY.
|
||||
reduce.
|
||||
unfold R, set_eq in HXY. rewrite HXY.
|
||||
Definition singleton_isIn : forall (A : Type) (a b : A),
|
||||
a ∈ {|b|} = merely (a = b).
|
||||
Proof.
|
||||
by (reduce T).
|
||||
Defined.
|
||||
|
||||
Definition union_isIn : forall (A : Type) (a : A) (X Y : T A),
|
||||
a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y).
|
||||
Proof.
|
||||
by (reduce T).
|
||||
Defined.
|
||||
|
||||
Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
|
||||
member a (filter ϕ X) = if ϕ a then member a X else False_hp.
|
||||
Proof.
|
||||
reduce T.
|
||||
apply properties.comprehension_isIn.
|
||||
Defined.
|
||||
|
||||
Definition reflect_f_eq : forall (A : Type) (X Y : T A),
|
||||
class_of (set_eq f) X = class_of (set_eq f) Y -> set_eq f X Y.
|
||||
Proof.
|
||||
intros.
|
||||
refine (same_class _ _ _ _ _ _) ; assumption.
|
||||
Defined.
|
||||
|
||||
Lemma class_union (A : Type) (X Y : T A) :
|
||||
class_of (set_eq f) (X ∪ Y) = (class_of (set_eq f) X) ∪ (class_of (set_eq f) Y).
|
||||
Proof.
|
||||
reflexivity.
|
||||
Defined.
|
||||
Defined.
|
||||
|
||||
Instance View_empty A: hasEmpty (View A).
|
||||
Proof.
|
||||
apply class_of.
|
||||
apply ∅.
|
||||
Defined.
|
||||
Lemma class_filter (A : Type) (X : T A) (ϕ : A -> Bool) :
|
||||
class_of (set_eq f) ({|X & ϕ|}) = {|(class_of (set_eq f) X) & ϕ|}.
|
||||
Proof.
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Instance View_singleton A: hasSingleton (View A) A.
|
||||
Proof.
|
||||
intros a.
|
||||
apply class_of.
|
||||
apply {|a|}.
|
||||
Defined.
|
||||
Ltac via_quotient := intros ; apply reflect_f_eq
|
||||
; rewrite ?class_union, ?class_filter
|
||||
; eauto with lattice_hints typeclass_instances.
|
||||
|
||||
Instance View_union A: hasUnion (View A).
|
||||
Proof.
|
||||
intros X Y.
|
||||
apply (max_L X Y).
|
||||
Defined.
|
||||
Lemma union_comm : forall A (X Y : T A),
|
||||
set_eq f (X ∪ Y) (Y ∪ X).
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Instance View_comprehension A: hasComprehension (View A) A.
|
||||
Proof.
|
||||
intros ϕ.
|
||||
hrecursion.
|
||||
- intros X.
|
||||
apply class_of.
|
||||
apply (filter ϕ X).
|
||||
- intros X X' HXX'. simpl.
|
||||
apply related_classes_eq.
|
||||
eapply well_defined_filter; eauto.
|
||||
Defined.
|
||||
Lemma union_assoc : forall A (X Y Z : T A),
|
||||
set_eq f ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)).
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Instance View_max_comm A: Commutative (@max_L (View A) _).
|
||||
Proof.
|
||||
unfold Commutative.
|
||||
hinduction.
|
||||
- intros X.
|
||||
hinduction.
|
||||
+ intros Y. cbn.
|
||||
apply related_classes_eq.
|
||||
eapply union_comm; eauto.
|
||||
+ intros. apply set_path2.
|
||||
- intros. apply path_forall; intro. apply set_path2.
|
||||
Defined.
|
||||
Lemma union_idem : forall A (X : T A),
|
||||
set_eq f (X ∪ X) X.
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Ltac buggeroff := intros; apply path_ishprop.
|
||||
Lemma union_neutral : forall A (X : T A),
|
||||
set_eq f (∅ ∪ X) X.
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Instance View_max_assoc A: Associative (@max_L (View A) _).
|
||||
Proof.
|
||||
unfold Associative.
|
||||
hinduction; try buggeroff.
|
||||
intros X.
|
||||
hinduction; try buggeroff.
|
||||
intros Y.
|
||||
hinduction; try buggeroff.
|
||||
intros Z. cbn.
|
||||
apply related_classes_eq.
|
||||
eapply union_assoc; eauto.
|
||||
Defined.
|
||||
|
||||
Instance View_max_idem A: Idempotent (@max_L (View A) _).
|
||||
Proof.
|
||||
unfold Idempotent.
|
||||
hinduction; try buggeroff.
|
||||
intros X; cbn.
|
||||
apply related_classes_eq.
|
||||
eapply union_idem; eauto.
|
||||
Defined.
|
||||
|
||||
Instance View_max_neut A: NeutralL (@max_L (View A) _) ∅.
|
||||
Proof.
|
||||
unfold NeutralL.
|
||||
hinduction; try buggeroff.
|
||||
intros X; cbn.
|
||||
apply related_classes_eq.
|
||||
eapply union_neutral; eauto.
|
||||
Defined.
|
||||
|
||||
Definition View_FSet A : View A -> FSet A.
|
||||
Proof.
|
||||
hrecursion.
|
||||
- apply f.
|
||||
- done.
|
||||
Defined.
|
||||
|
||||
Instance View_emb A : IsEmbedding (View_FSet A).
|
||||
Proof.
|
||||
apply isembedding_isinj_hset.
|
||||
unfold isinj.
|
||||
hrecursion; [ | intros; apply path_ishprop ]. intro X.
|
||||
hrecursion; [ | intros; apply path_ishprop ]. intro Y.
|
||||
intros. by apply related_classes_eq.
|
||||
Defined.
|
||||
|
||||
Instance View_surj A: IsSurjection (View_FSet A).
|
||||
Proof.
|
||||
apply BuildIsSurjection.
|
||||
intros X. apply tr.
|
||||
hrecursion X; try (intros; apply path_ishprop).
|
||||
- exists ∅. simpl. eapply f_empty; eauto.
|
||||
- intros a. exists {|a|}; simpl. eapply f_singleton; eauto.
|
||||
- intros X Y [pX HpX] [pY HpY].
|
||||
exists (pX ∪ pY); simpl.
|
||||
rewrite <- HpX, <- HpY.
|
||||
clear HpX HpY.
|
||||
hrecursion pY; [ | intros; apply set_path2]. intro tY.
|
||||
hrecursion pX; [ | intros; apply set_path2]. intro tX.
|
||||
eapply f_union; eauto.
|
||||
Defined.
|
||||
|
||||
Definition view_iso A : View A <~> FSet A.
|
||||
Proof.
|
||||
refine (BuildEquiv _ _ (View_FSet A) _).
|
||||
apply isequiv_surj_emb; apply _.
|
||||
Defined.
|
||||
|
||||
End quot.
|
||||
End properties.
|
||||
Loading…
Reference in New Issue