mirror of https://github.com/nmvdw/HITs-Examples
Removed some useless files
This commit is contained in:
Niels
parent
474c9324ca
commit
4ae639ace3
|
|
@ -1,331 +0,0 @@
|
|||
Require Import HoTT.
|
||||
Require Import FSets.
|
||||
|
||||
Section interface.
|
||||
Context `{Univalence}.
|
||||
Variable (T : Type -> Type)
|
||||
(f : forall A, T A -> FSet A).
|
||||
Context `{forall A, hasMembership (T A) A
|
||||
, forall A, hasEmpty (T A)
|
||||
, forall A, hasSingleton (T A) A
|
||||
, forall A, hasUnion (T A)
|
||||
, forall A, hasComprehension (T A) A}.
|
||||
|
||||
Class sets :=
|
||||
{
|
||||
f_empty : forall A, f A ∅ = ∅ ;
|
||||
f_singleton : forall A a, f A (singleton a) = {|a|};
|
||||
f_union : forall A X Y, f A (union X Y) = (f A X) ∪ (f A Y);
|
||||
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 [X1' ?] [X2' ?].
|
||||
simple refine (BuildContr _ _ _).
|
||||
* simple refine (Trunc_rec _ X1') ; intros [X1 fX1].
|
||||
simple refine (Trunc_rec _ X2') ; intros [X2 fX2].
|
||||
refine (tr(X1 ∪ X2;_)).
|
||||
rewrite f_union, fX1, fX2.
|
||||
reflexivity.
|
||||
* intros ; apply path_ishprop.
|
||||
Defined.
|
||||
|
||||
End interface.
|
||||
|
||||
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.
|
||||
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) ; intros [a fa].
|
||||
apply (tr(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.
|
||||
|
||||
Arguments quotient_iso {_} {_} _ {_} {_} {_}.
|
||||
|
||||
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 _)).
|
||||
|
||||
Section quotient_properties.
|
||||
Variable (T : Type -> Type).
|
||||
Variable (f : forall {A : Type}, T A -> FSet A).
|
||||
Context `{sets T f}.
|
||||
|
||||
Definition set_eq A := f_eq (T A) (FSet A) (f A).
|
||||
Definition View A : Type := quotientB (T A) (FSet A) (f A).
|
||||
|
||||
Instance f_is_surjective A : IsSurjection (f A).
|
||||
Proof.
|
||||
apply (f_surjective T f A).
|
||||
Defined.
|
||||
|
||||
Global Instance view_union (A : Type) : hasUnion (View A).
|
||||
Proof.
|
||||
intros X Y.
|
||||
apply (quotient_iso _)^-1.
|
||||
simple refine (union _ _).
|
||||
- simple refine (quotient_iso (f A) X).
|
||||
- simple refine (quotient_iso (f A) Y).
|
||||
Defined.
|
||||
|
||||
Definition well_defined_union (A : Type) (X Y : T A) :
|
||||
(class_of _ X) ∪ (class_of _ Y) = class_of _ (X ∪ Y).
|
||||
Proof.
|
||||
rewrite <- (eissect (quotient_iso _)).
|
||||
simpl.
|
||||
rewrite (f_union T _).
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Global Instance view_comprehension (A : Type) : hasComprehension (View A) A.
|
||||
Proof.
|
||||
intros ϕ X.
|
||||
apply (quotient_iso _)^-1.
|
||||
simple refine ({|_ & ϕ|}).
|
||||
apply (quotient_iso (f A) X).
|
||||
Defined.
|
||||
|
||||
Definition well_defined_filter (A : Type) (ϕ : A -> Bool) (X : T A) :
|
||||
{|class_of _ X & ϕ|} = class_of _ {|X & ϕ|}.
|
||||
Proof.
|
||||
rewrite <- (eissect (quotient_iso _)).
|
||||
simpl.
|
||||
rewrite (f_filter T _).
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Global Instance View_empty A : hasEmpty (View A).
|
||||
Proof.
|
||||
apply ((quotient_iso _)^-1 ∅).
|
||||
Defined.
|
||||
|
||||
Definition well_defined_empty A : ∅ = class_of (set_eq A) ∅.
|
||||
Proof.
|
||||
rewrite <- (eissect (quotient_iso _)).
|
||||
simpl.
|
||||
rewrite (f_empty T _).
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Global Instance View_singleton A: hasSingleton (View A) A.
|
||||
Proof.
|
||||
intro a ; apply ((quotient_iso _)^-1 {|a|}).
|
||||
Defined.
|
||||
|
||||
Definition well_defined_sungleton A (a : A) : {|a|} = class_of _ {|a|}.
|
||||
Proof.
|
||||
rewrite <- (eissect (quotient_iso _)).
|
||||
simpl.
|
||||
rewrite (f_singleton T _).
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Global Instance View_member A : hasMembership (View A) A.
|
||||
Proof.
|
||||
intros a ; unfold View.
|
||||
hrecursion.
|
||||
- apply (member a).
|
||||
- intros X Y HXY.
|
||||
reduce T.
|
||||
apply (ap _ HXY).
|
||||
Defined.
|
||||
|
||||
Instance View_max A : maximum (View A).
|
||||
Proof.
|
||||
apply view_union.
|
||||
Defined.
|
||||
|
||||
Hint Unfold Commutative Associative Idempotent NeutralL NeutralR View_max view_union.
|
||||
|
||||
Instance bottom_view A : bottom (View A).
|
||||
Proof.
|
||||
apply View_empty.
|
||||
Defined.
|
||||
|
||||
Ltac sq1 := autounfold ; intros ; try f_ap
|
||||
; rewrite ?(eisretr (quotient_iso _))
|
||||
; eauto with lattice_hints typeclass_instances.
|
||||
|
||||
Ltac sq2 := autounfold ; intros
|
||||
; rewrite <- (eissect (quotient_iso _)), ?(eisretr (quotient_iso _))
|
||||
; f_ap ; simpl
|
||||
; reduce T ; eauto with lattice_hints typeclass_instances.
|
||||
|
||||
Global Instance view_lattice A : JoinSemiLattice (View A).
|
||||
Proof.
|
||||
split ; try sq1 ; try sq2.
|
||||
Defined.
|
||||
|
||||
End quotient_properties.
|
||||
|
||||
Arguments set_eq {_} _ {_} _ _.
|
||||
|
||||
Section properties.
|
||||
Context `{Univalence}.
|
||||
Variable (T : Type -> Type) (f : forall A, T A -> FSet A).
|
||||
Context `{sets T f}.
|
||||
|
||||
Definition set_subset : forall A, T A -> T A -> hProp :=
|
||||
fun A X Y => (f A X) ⊆ (f A Y).
|
||||
|
||||
Definition empty_isIn : forall (A : Type) (a : A),
|
||||
a ∈ ∅ = False_hp.
|
||||
Proof.
|
||||
by (reduce T).
|
||||
Defined.
|
||||
|
||||
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.
|
||||
|
||||
Ltac via_quotient := intros ; apply reflect_f_eq ; simpl
|
||||
; rewrite <- ?(well_defined_union T _), <- ?(well_defined_empty T _)
|
||||
; eauto with lattice_hints typeclass_instances.
|
||||
|
||||
Lemma union_comm : forall A (X Y : T A),
|
||||
set_eq f (X ∪ Y) (Y ∪ X).
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Lemma union_assoc : forall A (X Y Z : T A),
|
||||
set_eq f ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)).
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Lemma union_idem : forall A (X : T A),
|
||||
set_eq f (X ∪ X) X.
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Lemma union_neutralL : forall A (X : T A),
|
||||
set_eq f (∅ ∪ X) X.
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
Lemma union_neutralR : forall A (X : T A),
|
||||
set_eq f (X ∪ ∅) X.
|
||||
Proof.
|
||||
via_quotient.
|
||||
Defined.
|
||||
|
||||
End properties.
|
||||
|
|
@ -1,63 +0,0 @@
|
|||
(* Type which proves that all types have merely decidable equality implies LEM *)
|
||||
Require Import HoTT HitTactics Sub.
|
||||
|
||||
Section TR.
|
||||
Context `{Univalence}.
|
||||
Variable A : hProp.
|
||||
|
||||
Definition T := Unit + Unit.
|
||||
|
||||
Definition R (x y : T) : hProp :=
|
||||
match x, y with
|
||||
| inl tt, inl tt => Unit_hp
|
||||
| inl tt, inr tt => A
|
||||
| inr tt, inl tt => A
|
||||
| inr tt, inr tt => Unit_hp
|
||||
end.
|
||||
|
||||
Global Instance R_refl : Reflexive R.
|
||||
Proof.
|
||||
intro x ; destruct x as [[ ] | [ ]] ; apply tt.
|
||||
Defined.
|
||||
|
||||
Global Instance R_sym : Symmetric R.
|
||||
Proof.
|
||||
repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]])
|
||||
; auto ; apply tt.
|
||||
Defined.
|
||||
|
||||
Global Instance R_trans : Transitive R.
|
||||
Proof.
|
||||
repeat (let x := fresh in intro x ; destruct x as [[ ] | [ ]]) ; intros
|
||||
; auto ; apply tt.
|
||||
Defined.
|
||||
|
||||
Definition TR : Type := quotient R.
|
||||
Definition TR_zero : TR := class_of R (inl tt).
|
||||
Definition TR_one : TR := class_of R (inr tt).
|
||||
|
||||
Definition equiv_pathspace_T : (TR_zero = TR_one) = (R (inl tt) (inr tt))
|
||||
:= path_universe (sets_exact R (inl tt) (inr tt)).
|
||||
|
||||
Global Instance quotientB_recursion : HitRecursion TR :=
|
||||
{
|
||||
indTy := _;
|
||||
recTy :=
|
||||
forall (P : Type) (HP: IsHSet P) (u : T -> P),
|
||||
(forall x y : T, R x y -> u x = u y) -> TR -> P;
|
||||
H_inductor := quotient_ind R ;
|
||||
H_recursor := @quotient_rec _ R _
|
||||
}.
|
||||
|
||||
End TR.
|
||||
|
||||
Theorem merely_dec `{Univalence} : (forall (A : Type) (a b : A), hor (a = b) (~a = b))
|
||||
->
|
||||
forall (A : hProp), A + (~A).
|
||||
Proof.
|
||||
intros X A.
|
||||
specialize (X (TR A) (TR_zero A) (TR_one A)).
|
||||
rewrite equiv_pathspace_T in X.
|
||||
strip_truncations.
|
||||
apply X.
|
||||
Defined.
|
||||
|
|
@ -1,289 +0,0 @@
|
|||
(* This is a /bad/ definition of FSets, without the 0-truncation.
|
||||
Here we show that the resulting type is not an h-set. *)
|
||||
|
||||
Require Import HoTT HitTactics.
|
||||
Require Import notation.
|
||||
|
||||
Module Export FSet.
|
||||
|
||||
Section FSet.
|
||||
Private Inductive FSet (A : Type): Type :=
|
||||
| E : FSet A
|
||||
| L : A -> FSet A
|
||||
| U : FSet A -> FSet A -> FSet A.
|
||||
|
||||
Global Instance fset_empty : forall A, hasEmpty (FSet A) := E.
|
||||
Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L.
|
||||
Global Instance fset_union : forall A, hasUnion (FSet A) := U.
|
||||
|
||||
Variable A : Type.
|
||||
|
||||
Axiom assoc : forall (x y z : FSet A),
|
||||
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
||||
|
||||
Axiom comm : forall (x y : FSet A),
|
||||
x ∪ y = y ∪ x.
|
||||
|
||||
Axiom nl : forall (x : FSet A),
|
||||
∅ ∪ x = x.
|
||||
|
||||
Axiom nr : forall (x : FSet A),
|
||||
x ∪ ∅ = x.
|
||||
|
||||
Axiom idem : forall (x : A),
|
||||
{|x|} ∪ {|x|} = {|x|}.
|
||||
|
||||
End FSet.
|
||||
|
||||
Arguments assoc {_} _ _ _.
|
||||
Arguments comm {_} _ _.
|
||||
Arguments nl {_} _.
|
||||
Arguments nr {_} _.
|
||||
Arguments idem {_} _.
|
||||
|
||||
Section FSet_induction.
|
||||
Variable A: Type.
|
||||
Variable (P : FSet A -> Type).
|
||||
Variable (eP : P ∅).
|
||||
Variable (lP : forall a: A, P {|a |}).
|
||||
Variable (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)).
|
||||
Variable (assocP : forall (x y z : FSet A)
|
||||
(px: P x) (py: P y) (pz: P z),
|
||||
assoc x y z #
|
||||
(uP x (y ∪ z) px (uP y z py pz))
|
||||
=
|
||||
(uP (x ∪ y) z (uP x y px py) pz)).
|
||||
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
||||
comm x y #
|
||||
uP x y px py = uP y x py px).
|
||||
Variable (nlP : forall (x : FSet A) (px: P x),
|
||||
nl x # uP ∅ x eP px = px).
|
||||
Variable (nrP : forall (x : FSet A) (px: P x),
|
||||
nr x # uP x ∅ px eP = px).
|
||||
Variable (idemP : forall (x : A),
|
||||
idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x).
|
||||
|
||||
(* Induction principle *)
|
||||
Fixpoint FSet_ind
|
||||
(x : FSet A)
|
||||
{struct x}
|
||||
: P x
|
||||
:= (match x return _ -> _ -> _ -> _ -> _ -> P x with
|
||||
| E => fun _ _ _ _ _ => eP
|
||||
| L a => fun _ _ _ _ _ => lP a
|
||||
| U y z => fun _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
|
||||
end) assocP commP nlP nrP idemP.
|
||||
|
||||
Axiom FSet_ind_beta_assoc : forall (x y z : FSet A),
|
||||
apD FSet_ind (assoc x y z) =
|
||||
(assocP x y z (FSet_ind x) (FSet_ind y) (FSet_ind z)).
|
||||
|
||||
Axiom FSet_ind_beta_comm : forall (x y : FSet A),
|
||||
apD FSet_ind (comm x y) = commP x y (FSet_ind x) (FSet_ind y).
|
||||
|
||||
Axiom FSet_ind_beta_nl : forall (x : FSet A),
|
||||
apD FSet_ind (nl x) = nlP x (FSet_ind x).
|
||||
|
||||
Axiom FSet_ind_beta_nr : forall (x : FSet A),
|
||||
apD FSet_ind (nr x) = nrP x (FSet_ind x).
|
||||
|
||||
Axiom FSet_ind_beta_idem : forall (x : A), apD FSet_ind (idem x) = idemP x.
|
||||
End FSet_induction.
|
||||
|
||||
Section FSet_recursion.
|
||||
|
||||
Variable A : Type.
|
||||
Variable P : Type.
|
||||
Variable e : P.
|
||||
Variable l : A -> P.
|
||||
Variable u : P -> P -> P.
|
||||
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
||||
Variable commP : forall (x y : P), u x y = u y x.
|
||||
Variable nlP : forall (x : P), u e x = x.
|
||||
Variable nrP : forall (x : P), u x e = x.
|
||||
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
||||
|
||||
Definition FSet_rec : FSet A -> P.
|
||||
Proof.
|
||||
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _) ; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
||||
- apply e.
|
||||
- apply l.
|
||||
- intros x y ; apply u.
|
||||
- apply assocP.
|
||||
- apply commP.
|
||||
- apply nlP.
|
||||
- apply nrP.
|
||||
- apply idemP.
|
||||
Defined.
|
||||
|
||||
Definition FSet_rec_beta_assoc : forall (x y z : FSet A),
|
||||
ap FSet_rec (assoc x y z)
|
||||
=
|
||||
assocP (FSet_rec x) (FSet_rec y) (FSet_rec z).
|
||||
Proof.
|
||||
intros.
|
||||
unfold FSet_rec.
|
||||
eapply (cancelL (transport_const (assoc x y z) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSet_ind_beta_assoc.
|
||||
Defined.
|
||||
|
||||
Definition FSet_rec_beta_comm : forall (x y : FSet A),
|
||||
ap FSet_rec (comm x y)
|
||||
=
|
||||
commP (FSet_rec x) (FSet_rec y).
|
||||
Proof.
|
||||
intros.
|
||||
unfold FSet_rec.
|
||||
eapply (cancelL (transport_const (comm x y) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSet_ind_beta_comm.
|
||||
Defined.
|
||||
|
||||
Definition FSet_rec_beta_nl : forall (x : FSet A),
|
||||
ap FSet_rec (nl x)
|
||||
=
|
||||
nlP (FSet_rec x).
|
||||
Proof.
|
||||
intros.
|
||||
unfold FSet_rec.
|
||||
eapply (cancelL (transport_const (nl x) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSet_ind_beta_nl.
|
||||
Defined.
|
||||
|
||||
Definition FSet_rec_beta_nr : forall (x : FSet A),
|
||||
ap FSet_rec (nr x)
|
||||
=
|
||||
nrP (FSet_rec x).
|
||||
Proof.
|
||||
intros.
|
||||
unfold FSet_rec.
|
||||
eapply (cancelL (transport_const (nr x) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSet_ind_beta_nr.
|
||||
Defined.
|
||||
|
||||
Definition FSet_rec_beta_idem : forall (a : A),
|
||||
ap FSet_rec (idem a)
|
||||
=
|
||||
idemP a.
|
||||
Proof.
|
||||
intros.
|
||||
unfold FSet_rec.
|
||||
eapply (cancelL (transport_const (idem a) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSet_ind_beta_idem.
|
||||
Defined.
|
||||
|
||||
End FSet_recursion.
|
||||
|
||||
Instance FSet_recursion A : HitRecursion (FSet A) :=
|
||||
{
|
||||
indTy := _; recTy := _;
|
||||
H_inductor := FSet_ind A; H_recursor := FSet_rec A
|
||||
}.
|
||||
|
||||
End FSet.
|
||||
|
||||
Section set_sphere.
|
||||
From HoTT.HIT Require Import Circle.
|
||||
Context `{Univalence}.
|
||||
Instance S1_recursion : HitRecursion S1 :=
|
||||
{
|
||||
indTy := _; recTy := _;
|
||||
H_inductor := S1_ind; H_recursor := S1_rec
|
||||
}.
|
||||
|
||||
Variable A : Type.
|
||||
|
||||
Definition f (x : S1) : x = x.
|
||||
Proof.
|
||||
hrecursion x.
|
||||
- exact loop.
|
||||
- refine (transport_paths_FlFr _ _ @ _).
|
||||
hott_simpl.
|
||||
Defined.
|
||||
|
||||
Definition S1op (x y : S1) : S1.
|
||||
Proof.
|
||||
hrecursion y.
|
||||
- exact x. (* x + base = x *)
|
||||
- apply f.
|
||||
Defined.
|
||||
|
||||
Lemma S1op_nr (x : S1) : S1op x base = x.
|
||||
Proof. reflexivity. Defined.
|
||||
|
||||
Lemma S1op_nl (x : S1) : S1op base x = x.
|
||||
Proof.
|
||||
hrecursion x.
|
||||
- exact loop.
|
||||
- refine (transport_paths_FlFr loop _ @ _).
|
||||
hott_simpl.
|
||||
apply moveR_pM. apply moveR_pM. hott_simpl.
|
||||
refine (ap_V _ _ @ _).
|
||||
f_ap. apply S1_rec_beta_loop.
|
||||
Defined.
|
||||
|
||||
Lemma S1op_assoc (x y z : S1) : S1op x (S1op y z) = S1op (S1op x y) z.
|
||||
Proof.
|
||||
hrecursion z.
|
||||
- reflexivity.
|
||||
- refine (transport_paths_FlFr loop _ @ _).
|
||||
hott_simpl.
|
||||
apply moveR_Mp. hott_simpl.
|
||||
rewrite S1_rec_beta_loop.
|
||||
rewrite ap_compose.
|
||||
rewrite S1_rec_beta_loop.
|
||||
hrecursion y.
|
||||
+ symmetry. apply S1_rec_beta_loop.
|
||||
+ apply is1type_S1.
|
||||
Qed.
|
||||
|
||||
Lemma S1op_comm (x y : S1) : S1op x y = S1op y x.
|
||||
Proof.
|
||||
hrecursion x.
|
||||
- apply S1op_nl.
|
||||
- hrecursion y.
|
||||
+ rewrite transport_paths_FlFr. hott_simpl.
|
||||
rewrite S1_rec_beta_loop. reflexivity.
|
||||
+ apply is1type_S1.
|
||||
Defined.
|
||||
|
||||
Definition FSet_to_S : FSet A -> S1.
|
||||
Proof.
|
||||
hrecursion.
|
||||
- exact base.
|
||||
- intro a. exact base.
|
||||
- exact S1op.
|
||||
- apply S1op_assoc.
|
||||
- apply S1op_comm.
|
||||
- apply S1op_nl.
|
||||
- apply S1op_nr.
|
||||
- simpl. reflexivity.
|
||||
Defined.
|
||||
|
||||
Lemma FSet_S_ap : (nl (E A)) = (nr ∅) -> idpath = loop.
|
||||
Proof.
|
||||
intros H1.
|
||||
enough (ap FSet_to_S (nl ∅) = ap FSet_to_S (nr ∅)) as H'.
|
||||
- rewrite FSet_rec_beta_nl in H'.
|
||||
rewrite FSet_rec_beta_nr in H'.
|
||||
simpl in H'. unfold S1op_nr in H'.
|
||||
exact H'^.
|
||||
- f_ap.
|
||||
Defined.
|
||||
|
||||
Lemma FSet_not_hset : IsHSet (FSet A) -> False.
|
||||
Proof.
|
||||
intros H1.
|
||||
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 FSet_S_ap.
|
||||
apply set_path2.
|
||||
Qed.
|
||||
|
||||
End set_sphere.
|
||||
|
|
@ -1,116 +0,0 @@
|
|||
(* Definition of Finite Sets as via cons lists *)
|
||||
Require Import HoTT HitTactics.
|
||||
Require Export notation.
|
||||
|
||||
Module Export FSetC.
|
||||
|
||||
Section FSetC.
|
||||
Private Inductive FSetC (A : Type) : Type :=
|
||||
| Nil : FSetC A
|
||||
| Cns : A -> FSetC A -> FSetC A.
|
||||
|
||||
Global Instance fset_empty : forall A,hasEmpty (FSetC A) := Nil.
|
||||
|
||||
Variable A : Type.
|
||||
Arguments Cns {_} _ _.
|
||||
Infix ";;" := Cns (at level 8, right associativity).
|
||||
|
||||
Axiom dupl : forall (a : A) (x : FSetC A),
|
||||
a ;; a ;; x = a ;; x.
|
||||
|
||||
Axiom comm : forall (a b : A) (x : FSetC A),
|
||||
a ;; b ;; x = b ;; a ;; x.
|
||||
|
||||
Axiom trunc : IsHSet (FSetC A).
|
||||
|
||||
End FSetC.
|
||||
|
||||
Arguments Cns {_} _ _.
|
||||
Arguments dupl {_} _ _.
|
||||
Arguments comm {_} _ _ _.
|
||||
|
||||
Infix ";;" := Cns (at level 8, right associativity).
|
||||
|
||||
Section FSetC_induction.
|
||||
|
||||
Variable A: Type.
|
||||
Variable (P : FSetC A -> Type).
|
||||
Variable (H : forall x : FSetC A, IsHSet (P x)).
|
||||
Variable (eP : P ∅).
|
||||
Variable (cnsP : forall (a:A) (x: FSetC A), P x -> P (a ;; x)).
|
||||
Variable (duplP : forall (a: A) (x: FSetC A) (px : P x),
|
||||
dupl a x # cnsP a (a;;x) (cnsP a x px) = cnsP a x px).
|
||||
Variable (commP : forall (a b: A) (x: FSetC A) (px: P x),
|
||||
comm a b x # cnsP a (b;;x) (cnsP b x px) =
|
||||
cnsP b (a;;x) (cnsP a x px)).
|
||||
|
||||
(* Induction principle *)
|
||||
Fixpoint FSetC_ind
|
||||
(x : FSetC A)
|
||||
{struct x}
|
||||
: P x
|
||||
:= (match x return _ -> _ -> _ -> P x with
|
||||
| Nil => fun _ => fun _ => fun _ => eP
|
||||
| a ;; y => fun _ => fun _ => fun _ => cnsP a y (FSetC_ind y)
|
||||
end) H duplP commP.
|
||||
|
||||
|
||||
Axiom FSetC_ind_beta_dupl : forall (a: A) (x : FSetC A),
|
||||
apD FSetC_ind (dupl a x) = duplP a x (FSetC_ind x).
|
||||
|
||||
Axiom FSetC_ind_beta_comm : forall (a b: A) (x : FSetC A),
|
||||
apD FSetC_ind (comm a b x) = commP a b x (FSetC_ind x).
|
||||
|
||||
End FSetC_induction.
|
||||
|
||||
Section FSetC_recursion.
|
||||
|
||||
Variable A: Type.
|
||||
Variable (P: Type).
|
||||
Variable (H: IsHSet P).
|
||||
Variable (nil : P).
|
||||
Variable (cns : A -> P -> P).
|
||||
Variable (duplP : forall (a: A) (x: P), cns a (cns a x) = (cns a x)).
|
||||
Variable (commP : forall (a b: A) (x: P), cns a (cns b x) = cns b (cns a x)).
|
||||
|
||||
(* Recursion principle *)
|
||||
Definition FSetC_rec : FSetC A -> P.
|
||||
Proof.
|
||||
simple refine (FSetC_ind _ _ _ _ _ _ _ );
|
||||
try (intros; simple refine ((transport_const _ _) @ _ )); cbn.
|
||||
- apply nil.
|
||||
- apply (fun a => fun _ => cns a).
|
||||
- apply duplP.
|
||||
- apply commP.
|
||||
Defined.
|
||||
|
||||
Definition FSetC_rec_beta_dupl : forall (a: A) (x : FSetC A),
|
||||
ap FSetC_rec (dupl a x) = duplP a (FSetC_rec x).
|
||||
Proof.
|
||||
intros.
|
||||
eapply (cancelL (transport_const (dupl a x) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSetC_ind_beta_dupl.
|
||||
Defined.
|
||||
|
||||
Definition FSetC_rec_beta_comm : forall (a b: A) (x : FSetC A),
|
||||
ap FSetC_rec (comm a b x) = commP a b (FSetC_rec x).
|
||||
Proof.
|
||||
intros.
|
||||
eapply (cancelL (transport_const (comm a b x) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply FSetC_ind_beta_comm.
|
||||
Defined.
|
||||
|
||||
End FSetC_recursion.
|
||||
|
||||
|
||||
Instance FSetC_recursion A : HitRecursion (FSetC A) :=
|
||||
{
|
||||
indTy := _; recTy := _;
|
||||
H_inductor := FSetC_ind A; H_recursor := FSetC_rec A
|
||||
}.
|
||||
|
||||
End FSetC.
|
||||
|
||||
Infix ";;" := Cns (at level 8, right associativity).
|
||||
|
|
@ -1,130 +0,0 @@
|
|||
(* Definitions of the Kuratowski-finite sets via a HIT *)
|
||||
Require Import HoTT HitTactics.
|
||||
Require Export notation.
|
||||
|
||||
Module Export FSet.
|
||||
Section FSet.
|
||||
Private Inductive FSet (A : Type) : Type :=
|
||||
| E : FSet A
|
||||
| L : A -> FSet A
|
||||
| U : FSet A -> FSet A -> FSet A.
|
||||
|
||||
Global Instance fset_empty : forall A, hasEmpty (FSet A) := E.
|
||||
Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L.
|
||||
Global Instance fset_union : forall A, hasUnion (FSet A) := U.
|
||||
|
||||
Variable A : Type.
|
||||
|
||||
Axiom assoc : forall (x y z : FSet A),
|
||||
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
||||
|
||||
Axiom comm : forall (x y : FSet A),
|
||||
x ∪ y = y ∪ x.
|
||||
|
||||
Axiom nl : forall (x : FSet A),
|
||||
∅ ∪ x = x.
|
||||
|
||||
Axiom nr : forall (x : FSet A),
|
||||
x ∪ ∅ = x.
|
||||
|
||||
Axiom idem : forall (x : A),
|
||||
{|x|} ∪ {|x|} = {|x|}.
|
||||
|
||||
Axiom trunc : IsHSet (FSet A).
|
||||
|
||||
End FSet.
|
||||
|
||||
Arguments assoc {_} _ _ _.
|
||||
Arguments comm {_} _ _.
|
||||
Arguments nl {_} _.
|
||||
Arguments nr {_} _.
|
||||
Arguments idem {_} _.
|
||||
|
||||
Section FSet_induction.
|
||||
Variable A: Type.
|
||||
Variable (P : FSet A -> Type).
|
||||
Variable (H : forall X : FSet A, IsHSet (P X)).
|
||||
Variable (eP : P ∅).
|
||||
Variable (lP : forall a: A, P {|a|}).
|
||||
Variable (uP : forall (x y: FSet A), P x -> P y -> P (x ∪ y)).
|
||||
Variable (assocP : forall (x y z : FSet A)
|
||||
(px: P x) (py: P y) (pz: P z),
|
||||
assoc x y z #
|
||||
(uP x (y ∪ z) px (uP y z py pz))
|
||||
=
|
||||
(uP (x ∪ y) z (uP x y px py) pz)).
|
||||
Variable (commP : forall (x y: FSet A) (px: P x) (py: P y),
|
||||
comm x y #
|
||||
uP x y px py = uP y x py px).
|
||||
Variable (nlP : forall (x : FSet A) (px: P x),
|
||||
nl x # uP ∅ x eP px = px).
|
||||
Variable (nrP : forall (x : FSet A) (px: P x),
|
||||
nr x # uP x ∅ px eP = px).
|
||||
Variable (idemP : forall (x : A),
|
||||
idem x # uP {|x|} {|x|} (lP x) (lP x) = lP x).
|
||||
|
||||
(* Induction principle *)
|
||||
Fixpoint FSet_ind
|
||||
(x : FSet A)
|
||||
{struct x}
|
||||
: P x
|
||||
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
|
||||
| E => fun _ _ _ _ _ _ => eP
|
||||
| L a => fun _ _ _ _ _ _ => lP a
|
||||
| U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
|
||||
end) H assocP commP nlP nrP idemP.
|
||||
|
||||
End FSet_induction.
|
||||
|
||||
Section FSet_recursion.
|
||||
|
||||
Variable A : Type.
|
||||
Variable P : Type.
|
||||
Variable H: IsHSet P.
|
||||
Variable e : P.
|
||||
Variable l : A -> P.
|
||||
Variable u : P -> P -> P.
|
||||
Variable assocP : forall (x y z : P), u x (u y z) = u (u x y) z.
|
||||
Variable commP : forall (x y : P), u x y = u y x.
|
||||
Variable nlP : forall (x : P), u e x = x.
|
||||
Variable nrP : forall (x : P), u x e = x.
|
||||
Variable idemP : forall (x : A), u (l x) (l x) = l x.
|
||||
|
||||
Definition FSet_rec : FSet A -> P.
|
||||
Proof.
|
||||
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _)
|
||||
; try (intros ; simple refine ((transport_const _ _) @ _)) ; cbn.
|
||||
- apply e.
|
||||
- apply l.
|
||||
- intros x y ; apply u.
|
||||
- apply assocP.
|
||||
- apply commP.
|
||||
- apply nlP.
|
||||
- apply nrP.
|
||||
- apply idemP.
|
||||
Defined.
|
||||
|
||||
End FSet_recursion.
|
||||
|
||||
Instance FSet_recursion A : HitRecursion (FSet A) :=
|
||||
{
|
||||
indTy := _; recTy := _;
|
||||
H_inductor := FSet_ind A; H_recursor := FSet_rec A
|
||||
}.
|
||||
|
||||
End FSet.
|
||||
|
||||
Lemma union_idem {A : Type} : forall x: FSet A, x ∪ x = x.
|
||||
Proof.
|
||||
hinduction ; try (intros ; apply set_path2).
|
||||
- apply nl.
|
||||
- apply idem.
|
||||
- intros x y P Q.
|
||||
rewrite assoc.
|
||||
rewrite (comm x y).
|
||||
rewrite <- (assoc y x x).
|
||||
rewrite P.
|
||||
rewrite (comm y x).
|
||||
rewrite <- (assoc x y y).
|
||||
f_ap.
|
||||
Defined.
|
||||
Loading…
Reference in New Issue