feat(set_quotient): add some properties for set_quotients

hott/hit/set_quotient.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of set-quotients, i.e. quotient of a mere relation which is then set-truncated.
 -/
 
-import .quotient .trunc function
+import function algebra.relation types.trunc types.eq
 
 open eq is_trunc trunc quotient equiv
 
@@ -23,7 +23,7 @@ section
   definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' :=
   ap tr (eq_of_rel _ H)
 
-  theorem is_hset_set_quotient : is_hset set_quotient :=
+  theorem is_hset_set_quotient [instance] : is_hset set_quotient :=
   begin unfold set_quotient, exact _ end
 
   protected definition rec {P : set_quotient → Type} [Pt : Πaa, is_hset (P aa)]
@@ -75,10 +75,10 @@ attribute set_quotient.class_of [constructor]
 attribute set_quotient.rec set_quotient.elim [unfold 7] [recursor 7]
 attribute set_quotient.rec_on set_quotient.elim_on [unfold 4]
 
-open sigma
+open sigma relation function
 
 namespace set_quotient
-  variables {A : Type} (R : A → A → hprop)
+  variables {A B C : Type} (R : A → A → hprop) (S : B → B → hprop) (T : C → C → hprop)
 
   definition is_surjective_class_of : is_surjective (class_of : A → set_quotient R) :=
   λx, set_quotient.rec_on x (λa, tr (fiber.mk a idp)) (λa a' r, !is_hprop.elimo)
@@ -98,4 +98,45 @@ namespace set_quotient
         intro a a' r, apply eq_pathover, apply hdeg_square, apply elim_eq_of_rel}
   end
 
+  definition code [unfold 4] (a : A) (x : set_quotient R) [H : is_equivalence R] : hprop :=
+  set_quotient.elim_on x (R a)
+    begin
+      intros a' a'' H1,
+      refine to_inv !trunctype_eq_equiv _, esimp,
+      apply ua,
+      apply equiv_of_is_hprop,
+      { intro H2, exact is_transitive.trans R H2 H1},
+      { intro H2, apply is_transitive.trans R H2, exact is_symmetric.symm R H1}
+    end
+
+  definition encode {a : A} {x : set_quotient R} (p : class_of a = x)
+    [H : is_equivalence R] : code R a x :=
+  begin
+    induction p, esimp, apply is_reflexive.refl R
+  end
+
+  definition rel_of_eq {a a' : A} (p : class_of a = class_of a' :> set_quotient R)
+    [H : is_equivalence R] : R a a' :=
+  encode R p
+
+  variables {R S T}
+  definition quotient_unary_map (f : A → B) (H : Π{a a'} (r : R a a'), S (f a) (f a')) :
+    set_quotient R → set_quotient S :=
+  set_quotient.elim (class_of ∘ f) (λa a' r, eq_of_rel (H r))
+
+  definition quotient_binary_map (f : A → B → C)
+    (H : Π{a a'} (r : R a a') {b b'} (s : S b b'), T (f a b) (f a' b'))
+    [HR : is_reflexive R] [HS : is_reflexive S] :
+    set_quotient R → set_quotient S → set_quotient T :=
+  begin
+    refine set_quotient.elim _ _,
+    { intro a, refine set_quotient.elim _ _,
+      { intro b, exact class_of (f a b)},
+      { intro b b' s, apply eq_of_rel, apply H, apply is_reflexive.refl R, exact s}},
+    { intro a a' r, apply eq_of_homotopy, refine set_quotient.rec _ _,
+      { intro b, esimp, apply eq_of_rel, apply H, exact r, apply is_reflexive.refl S},
+      { intro b b' s, apply eq_pathover, esimp, apply is_hset.elims}}
+  end
+
+
 end set_quotient