Merge pull request #158 from arnoudvanderleer/reflections

Change universal arrows to (co)reflections

Author: nmvdw

Modules/Prelims/lib.v

@@ -28,6 +28,7 @@ Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.catiso.
 
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
 
 
 Local Notation "'SET'" := hset_category.
@@ -57,21 +58,20 @@ Proof.
     + apply (pr2 ini).
 Defined.
 
-Lemma initial_universal_to_lift_initial {D C : precategory}
+Lemma initial_universal_to_lift_initial {D C : category}
       (S : D ⟶ C)
       (c : Initial C)
       {r : D} {f : C ⟦ c, S r ⟧}
-      (unif : is_universal_arrow_to  S c r f) :
+      (unif : is_reflection (make_reflection_data r f)) :
   isInitial _ r.
 Proof.
   intro d.
-  specialize (unif d (InitialArrow _ _)).
+  specialize (unif (make_reflection_data d (InitialArrow _ _))).
   use make_iscontr.
   - apply (iscontrpr1 unif).
   - intro g.
-    cbn.
     apply path_to_ctr.
-    apply InitialArrowUnique.
+    refine (!InitialArrowUnique _ _ _).
 Qed.
 
 (**

Modules/Signatures/EpiSigRepresentability.v

@@ -31,6 +31,7 @@ Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 Require Import UniMath.CategoryTheory.whiskering.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import Modules.Prelims.EpiComplements.
@@ -597,25 +598,21 @@ Lemma u_rep_universal (R : model _)
     (cond_R :
        (isEpi (C := [_, _]) (pr1 (F (R' _ Repi) )) × sig_preservesNatEpiMonad a)
          ⨿ (isEpi (C := [_, _]) (pr1 (F (pr1 R))) × sig_preservesNatEpiMonad b))
-  :
-
-  is_universal_arrow_to FF R (rep_of_b_in_R' R Repi epiab cond_R)
-    (projR_rep R Repi epiab cond_R).
+  : is_reflection (make_reflection_data (F := FF) (rep_of_b_in_R' R Repi epiab cond_R)
+    (projR_rep R Repi epiab cond_R)).
 Proof.
-    intros S m. cbn in S, m.
-    use unique_exists.
-    + unshelve use (u_rep _ _ _ m).
+    intro m.
+    use make_reflection_arrow.
+    + unshelve use (u_rep _ _ _ (m : Rep_a⟦_, _⟧)).
     + (* Ici ca devrait être apply quotientmonad.u_def *)
-      apply pathsinv0.
       apply model_mor_mor_equiv.
       intro x.
-      etrans. { apply u_def. }
-      use (helper _ Repi epiab _ _ (u_rep R _ _ m cond_R)).
-    + intro y; apply homset_property.
+      refine (u_def _ _ _ _ @ _).
+      exact (helper _ Repi epiab _ _ (u_rep R _ _ (m : Rep_a⟦_, _⟧) cond_R) _).
     + intros u' hu'.
       hnf in hu'.
       apply u_rep_unique.
-      rewrite <- hu'.
+      rewrite hu'.
       intro x.
       apply helper.
 Qed.
@@ -632,7 +629,7 @@ Proof.
   intro iniR.
   eapply tpair.
   eapply (initial_universal_to_lift_initial _ (_ ,, iniR)).
-  use ( u_rep_universal R R_epi epiab cond_R ).
+  exact (u_rep_universal R R_epi epiab cond_R).
 Qed.
 
 Theorem push_initiality
@@ -681,15 +678,15 @@ Definition is_right_adjoint_functor_of_reps
   : is_right_adjoint FF.
 Proof.
   set (cond_F := fun R R_epi => inl ((Fepi R R_epi),, aepi) : cond_isEpi_hab R R_epi).
-  use right_adjoint_left_from_partial.
-  - intro R.
-    use (rep_of_b_in_R' R _ _ (cond_F R _ )).
+  apply left_adjoint_weq_reflections.
+  intro R.
+  use make_reflection'.
+  - use (rep_of_b_in_R' R _ _ (cond_F R _ )).
     + apply epiall.
     + apply ii1.
       apply epiall.
-  - intro R. apply projR_rep.
-  - intro R.
-    apply u_rep_universal.
+  - apply projR_rep.
+  - apply u_rep_universal.
 Qed.
 
 Corollary is_right_adjoint_functor_of_reps_from_pw_epi

Modules/SoftEquations/AdjunctionEquationRep.v

@@ -57,6 +57,7 @@ Require Import Modules.Signatures.BindingSig.
 Require Import Modules.SoftEquations.BindingSig.
 
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
 Require Import UniMath.CategoryTheory.Limits.Initial.
 
 
@@ -115,33 +116,33 @@ Section QuotientRep.
     := projR_rep Sig epiSig R_epi SigR_epi  d ff.
 
   Lemma u_rep_universal (R : model _) (R_epi: preserves_Epi R) (SigR_epi : preserves_Epi (Sig R))
-    : is_universal_arrow_to (ModEq_Mod_functor eq) R (R' R_epi SigR_epi) (projR_rep R R_epi SigR_epi).
+    : is_reflection (make_reflection_data (F := ModEq_Mod_functor eq) (R' R_epi SigR_epi) (projR_rep R R_epi SigR_epi)).
   Proof.
-    intros S f.
-    set (j := tpair (fun (x : model_equations _) => R →→ x) (S : model_equations _)  f).
-    eassert (def_u :=(u_rep_def _ _ _  _ (@d R) (@ff R) j)).
-    unshelve eapply unique_exists.
-    - exact (u_rep_arrow R_epi SigR_epi f ,, tt).
-    - exact (! def_u).
-    - intro.
-      apply homset_property.
+    intros f.
+    set (j := tpair (λ (x : model_equations _), R →→ x) (reflection_data_object f) (f : REP_CAT⟦_, _⟧)).
+    eassert (def_u := u_rep_def _ _ _  _ (@d R) (@ff R) j).
+    use make_reflection_arrow.
+    - exact (u_rep_arrow R_epi SigR_epi (f : REP_CAT⟦_, _⟧) ,, tt).
+    - exact def_u.
     - intros g eq'.
-      use eq_in_sub_precategory.
-      cbn.
-      use (_ : isEpi (C := REP_CAT) (projR_rep R _ _)); [apply isEpi_projR_rep|].
-      etrans;[exact eq'|exact def_u].
+      apply eq_in_sub_precategory.
+      use (isEpi_projR_rep _ _ _ _ _ _ : isEpi (C := REP_CAT) (projR_rep R _ _)).
+      refine (!eq' @ _).
+      exact def_u.
   Qed.
 
   (** If all models preserve epis, and their image by the signature
       preserve epis, then we have an adjunctions *)
   Definition ModEq_Mod_is_right_adjoint
              (modepis : ∏ (R : model Sig), preserves_Epi R)
              (SigR_epis : ∏ (R : model Sig) , preserves_Epi (Sig R))
-    : is_right_adjoint (ModEq_Mod_functor eq) :=
-    right_adjoint_left_from_partial (ModEq_Mod_functor (λ x : O, eq x))
-                                    (fun R => R' (modepis R) (SigR_epis R ))
-                                    (fun R => projR_rep R (modepis R)(SigR_epis R ))
-                                    (fun R => u_rep_universal R (modepis R)(SigR_epis R )).
+    : is_right_adjoint (ModEq_Mod_functor eq)
+    := invmap (left_adjoint_weq_reflections _)
+      (λ (R : REP_CAT), make_reflection'
+        (F := ModEq_Mod_functor eq)
+        (R' (modepis R) (SigR_epis R))
+        (projR_rep R (modepis R)(SigR_epis R ))
+        (u_rep_universal R (modepis R) (SigR_epis R))).
 
 
   (** If the initial model and its image by the signature preserve epis,

Modules/SoftEquations/CatOfTwoSignatures.v

@@ -54,6 +54,7 @@ Require Import UniMath.CategoryTheory.Limits.Coproducts.
 Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 Require Import UniMath.CategoryTheory.Limits.Pushouts.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
 
 Section TwoSig.
 
@@ -294,25 +295,26 @@ Definition OneSig_to_TwoSig (S : signature C) : TwoSignature := (S ,, ∅ ,, emp
 
 (** This induces a left adjoint to the forgetful functor *)
 Lemma universal_OneSig_to_TwoSig (S : signature C) :
-  is_universal_arrow_to (pr1_category two_signature_disp) S (OneSig_to_TwoSig S) (identity _).
+  is_reflection (F := pr1_category two_signature_disp)
+    (make_reflection_data (OneSig_to_TwoSig S) (identity _)).
 Proof.
-  intros TT f.
-  unshelve eapply unique_exists.
-  - refine (f ,, _) .
-    intro.
-    use empty_rect.
-  - apply id_left.
-  - intro.
-    apply homset_property.
+  intro f.
+  use make_reflection_arrow.
+  - exists (f : signature_category⟦_, _⟧).
+    intro x.
+    exact (empty_rect _).
+  - exact (!id_left _).
   - intros y eqy.
     apply subtypePath_prop.
-    etrans;[|exact eqy].
-    apply pathsinv0, id_left.
+    refine (_ @ !eqy).
+    symmetry.
+    apply id_left.
 Defined.
 
 Definition TwoSig_OneSig_is_right_adjoint
   : is_right_adjoint (pr1_category two_signature_disp)
-  := right_adjoint_left_from_partial (X := signature_category ) _ _ _ universal_OneSig_to_TwoSig.
+  := invmap (left_adjoint_weq_reflections _)
+    (λ (S : signature_category), make_reflection _ (universal_OneSig_to_TwoSig S)).
 
 Lemma OneSig_TwoSig_fully_faithful
   : fully_faithful (left_adjoint TwoSig_OneSig_is_right_adjoint : _ ⟶  TwoSig_category).
@@ -462,20 +464,17 @@ Definition OneMod_TwoMod (M : MOD1) : MOD2 :=
 
 (** This induces a left adjoint to the forgetful functor *)
 Lemma universal_OneMod_TwoMod (M : MOD1) :
-  is_universal_arrow_to TwoMod_OneMod_functor M  (OneMod_TwoMod M ) (identity _).
+  is_reflection (F := TwoMod_OneMod_functor)
+    (make_reflection_data (OneMod_TwoMod M ) (identity _)).
 Proof.
-  intros TT f.
-  unshelve eapply unique_exists.
-  - exact ((pr1 f ,, fun x => empty_rect _) ,, pr2 f) .
-  - apply id_left.
-  - intro.
-    apply homset_property.
-  -
-    intros y eqy.
+  intro f.
+  use make_reflection_arrow.
+  - exact ((pr1 (f : MOD1⟦_, _⟧) ,, fun x => empty_rect _) ,, pr2 (f : MOD1⟦_, _⟧)).
+  - exact (!id_left _).
+  - intros y eqy.
     rewrite id_left in eqy.
-    cbn in eqy.
-    rewrite <- eqy.
-    cbn.
+    cbn in *.
+    rewrite eqy.
     set (y2' := fun (x : model_equations _) => _).
     assert (e : y2' = (pr2 (pr1 y))).
     {
@@ -491,8 +490,9 @@ Proof.
 Defined.
 
 
-Definition TwoMod_OneMod_is_right_adjoint : is_right_adjoint TwoMod_OneMod_functor :=
-  right_adjoint_left_from_partial (X := MOD1) _ _ _ universal_OneMod_TwoMod.
+Definition TwoMod_OneMod_is_right_adjoint : is_right_adjoint TwoMod_OneMod_functor
+  := invmap (left_adjoint_weq_reflections _)
+    (λ M, make_reflection _ (universal_OneMod_TwoMod M)).
 
 Lemma OneMod_TwoMod_fully_faithful : fully_faithful (left_adjoint TwoMod_OneMod_is_right_adjoint).
 Proof.