Adding helper functions

_CoqProject

@@ -17,6 +17,7 @@ theories/Param_paths.v
 theories/Param_sigma.v
 theories/Param_prod.v
 theories/Param_option.v
+theories/Common.v
 
 examples/Example.v
 examples/int_to_Zp.v

examples/peano_bin_nat.v

@@ -92,7 +92,7 @@ Definition Nsucc (n : N) := Npos (succ_pos n).
 Definition Nadd (m n : N) := match m, n with
 | N0, x | x, N0 => x
 | Npos p, Npos q => Npos (Pos.add p q)
-end. 
+end.
 Infix "+" := Nadd : N_scope.
 Notation "n .+1" := (Nsucc n) : N_scope.
 
@@ -107,7 +107,7 @@ Definition Nmap (n : N) : nat :=
 Fixpoint Ncomap (n : nat) : N :=
   match n with O => 0 | S n => Nsucc (Ncomap n) end.
 
-Definition RN@{} (m : N) (n : nat) := paths@{Set} (Ncomap n) m.
+Definition RN@{} := sym_rel@{Set} (graph@{Set} Ncomap).
 
 Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0.
 Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed.
@@ -127,16 +127,12 @@ Proof. by move=> kp; rewrite NcomapD kp Naddpp. Qed.
 Lemma NmapK (n : N) : Ncomap (Nmap n) = n.
 Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed.
 
-Lemma Nmap_in_R@{} (m : N) (n : nat) :
-  paths@{Set} (Nmap m) n -> sym_rel@{Set} RN n m.
-Proof. by move<-; apply: NmapK. Qed.
-
 (* the best we can do to link these types is (4,4), but
 we only need (2a,3) which is morally that Nmap is a split injection *)
-
-Definition RN2a3@{} : Param2a3.Rel@{Set} N nat := @Param2a3.BuildRel@{Set} N nat RN@{}
-   (@Map2a.BuildHas@{Set} _ _ _ Nmap Nmap_in_R)
-   (@Map3.BuildHas@{Set} _ _ _ Ncomap (fun _ _ p => p) (fun _ _ p => p)).
+Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitSurj.toParamSym@{Set} {|
+   SplitSurj.retract := Ncomap;
+   SplitSurj.section := Nmap;
+   SplitSurj.sectionK := NmapK |}.
 
 (* for brevity, we create witnesses at lower classes by forgetting fields in RN2a3 *)
 (* this behaviour can be automated so as to only declare Rn2a3 and get for free all the instances

theories/Common.v

@@ -0,0 +1,129 @@
+(*****************************************************************************)
+(*                            *                    Trocq                     *)
+(*  _______                   *           Copyright (C) 2023 MERCE           *)
+(* |__   __|                  *    (Mitsubishi Electric R&D Centre Europe)   *)
+(*    | |_ __ ___   ___ __ _  *       Cyril Cohen <[email protected]>     *)
+(*    | | '__/ _ \ / __/ _` | *       Enzo Crance <[email protected]>     *)
+(*    | | | | (_) | (_| (_| | *   Assia Mahboubi <[email protected]>   *)
+(*    |_|_|  \___/ \___\__, | ************************************************)
+(*                        | | * This file is distributed under the terms of  *)
+(*                        |_| * GNU Lesser General Public License Version 3  *)
+(*                            * see LICENSE file for the text of the license *)
+(*****************************************************************************)
+
+Require Import ssreflect.
+From elpi Require Export elpi.
+From HoTT Require Export HoTT.
+From Trocq Require Export
+  HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param
+  Param_paths Vernac.
+
+Definition graph@{i} {A B : Type@{i}} (f : A -> B) := paths o f.
+
+Module Fun.
+Section Fun.
+Universe i.
+Context {A B : Type@{i}} (f : A -> B) (g : B -> A).
+Definition toParam : Param40.Rel@{i} A B :=
+  @Param40.BuildRel A B (graph f)
+     (@Map4.BuildHas@{i} _ _ _ _
+       (fun _ _ => id) (fun _ _ => id) (fun _ _ _ => 1%path))
+     (@Map0.BuildHas@{i} _ _ _).
+
+Definition toParamSym : Param04.Rel@{i} A B :=
+  @Param04.BuildRel A B (sym_rel (graph g))
+     (@Map0.BuildHas@{i} _ _ _)
+     (@Map4.BuildHas@{i} _ _ _ g (fun _ _ => id) (fun _ _ => id)
+        (fun _ _ _ => 1%path)).
+End Fun.
+End Fun.
+
+Module SplitInj.
+Section SplitInj.
+Universe i.
+Context {A B : Type@{i}}.
+Record type@{} := {
+  section :> A -> B;
+  retract : B -> A;
+  sectionK : forall x, retract (section x) = x
+}.
+
+Definition fromParam@{} (R : Param2a2b.Rel@{i} A B) := {|
+  section := map R;
+  retract := comap R;
+  sectionK x := R_in_comap R _ _ (map_in_R R _ _ 1%path)
+|}.
+
+Section to.
+Variable (f : type).
+
+Let section_in_retract b a (e : f a = b) : retract f b = a :=
+  transport (fun x => retract f x = a) e (sectionK f a).
+
+Definition toParam@{} : Param42b.Rel@{i} A B :=
+  @Param42b.BuildRel A B (graph f)
+     (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id)
+        (fun _ _ _ => 1%path))
+     (@Map2b.BuildHas@{i} _ _ _ _ section_in_retract).
+
+Definition toParamSym@{} : Param2b4.Rel@{i} B A :=
+  @Param2b4.BuildRel B A (sym_rel (graph f))
+     (@Map2b.BuildHas@{i} _ _ _ _ section_in_retract)
+     (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id)
+        (fun _ _ _ => 1%path)).
+
+End to.
+
+End SplitInj.
+End SplitInj.
+
+Module SplitSurj.
+Section SplitSurj.
+Universe i.
+Context {A B : Type@{i}}.
+Record type := {
+  retract :> A -> B;
+  section : B -> A;
+  sectionK : forall x, retract (section x) = x
+}.
+
+Definition fromParam@{} (R : Param2b2a.Rel@{i} A B) := {|
+  retract := map R;
+  section := comap R;
+  sectionK x := R_in_map R (comap R x) x (comap_in_R R x (comap R x) 1%path)
+|}.
+
+Section to.
+Context (f : type).
+
+Let section_in_retract b a (e : section f b = a) : f a = b :=
+  transport (fun x => f x = b) e (sectionK f b).
+
+Definition toParam@{} : Param42a.Rel@{i} A B :=
+  @Param42a.BuildRel A B (graph f)
+     (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id)
+        (fun _ _ _ => 1%path))
+     (@Map2a.BuildHas@{i} _ _ _ _ section_in_retract).
+
+Definition toParamSym@{} : Param2a4.Rel@{i} B A :=
+  @Param2a4.BuildRel B A (sym_rel (graph f))
+     (@Map2a.BuildHas@{i} _ _ _ _ (section_in_retract))
+     (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id)
+        (fun _ _ _ => 1%path)).
+
+End to.
+
+End SplitSurj.
+End SplitSurj.
+
+Module Equiv.
+(* This is exactly adjointify *)
+Definition fromParam@{i} {A B : Type@{i}} (R : Param33.Rel@{i} A B) :
+   A <~> B := {|
+   equiv_fun := map R;
+   equiv_isequiv := isequiv_adjointify _ (comap R)
+     (fun b => R_in_map R _ _ (comap_in_R R _ _ 1%path))
+     (fun a => R_in_comap R _ _ (map_in_R R _ _ 1%path))
+  |}.
+
+End Equiv.

theories/Trocq.v

@@ -15,4 +15,4 @@ From elpi Require Export elpi.
 From HoTT Require Export HoTT.
 From Trocq Require Export
   HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param
-  Param_paths Vernac.
+  Param_paths Vernac Common.