experiment with HITs and rewritng rules

dune

@@ -74,7 +74,7 @@
     --utf8
     --no-externals
     --parse-comments)
-   (flags -noinit -indices-matter -color on)))
+   (flags -noinit -indices-matter -color on -allow-rewrite-rules)))
  (_
   (coq
    (coqdoc_flags
@@ -83,7 +83,7 @@
     --utf8
     --no-externals
     --parse-comments)
-   (flags -noinit -indices-matter))))
+   (flags -noinit -indices-matter -allow-rewrite-rules))))
 
 ; Bench
 

etc/generate_coqproject.sh

@@ -30,6 +30,7 @@ COQPROJECT_HEADER=\
 
 -arg -noinit
 -arg -indices-matter
+-arg -allow-rewrite-rules
 -arg -native-compiler -arg no
 "
 

theories/Basics/Equivalences.v

@@ -247,7 +247,8 @@ Proof.
                       end)).
   intros [x y].
   rewrite <- ap_compose.
-  symmetry; apply ap_const.
+  symmetry.
+  nrapply ap_const.
 Defined.
 
 Definition equiv_pr1 {A : Type} (P : A -> Type) `{forall x, Contr (P x)}

theories/Basics/Overture.v

@@ -370,8 +370,19 @@ Arguments internal_paths_rew_r {A%_type_scope} {a y} P%_function_scope HC X.
 
 (** Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A], then [ap f p : f x = f y].  We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
 
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
-  := match p with idpath => idpath end.
+(* Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end. *)
+
+Unset Universe Polymorphism.
+Symbol ap@{u v} : forall {A : Type@{u}}{B : Type@{v}} (f : A -> B) {x y : A}
+  (p : x = y), f x = f y.
+Rewrite Rule ap_comp :=
+| @ap ?A ?P ?f _ _ (@idpath@{u} _ ?a) => @idpath ?P (?f ?a).
+Symbol apD@{u v} : forall {A : Type@{u}} {P : A -> Type@{v}}
+  (f : forall x, P x) {x y : A} (p : x = y), p # f x = f y.
+Rewrite Rule apD_comp :=
+| @apD ?A ?P ?f _ _ (@idpath _ ?a) => @idpath (?P ?a) (?f ?a).
+Set Universe Polymorphism.
 
 Global Arguments ap {A B}%_type_scope f%_function_scope {x y} p%_path_scope.
 
@@ -445,13 +456,13 @@ Arguments ap {A B} f {x y} p : simpl nomatch.
 
   The type [p # f x = f y] can profitably be considered as a heterogeneous or dependent equality type, of "paths from [f x] to [f y] over [p]". *)
 
-Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+(* Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
   p # (f x) = f y
   :=
-  match p with idpath => idpath end.
+  match p with idpath => idpath end. *)
 
 (** See above for the meaning of [simpl nomatch]. *)
-Arguments apD {A%_type_scope B} f%_function_scope {x y} p%_path_scope : simpl nomatch.
+Arguments apD {A%_type_scope P} f%_function_scope {x y} p%_path_scope : simpl nomatch.
 
 (** ** Equivalences *)
 

theories/Basics/PathGroupoids.v

@@ -485,7 +485,7 @@ Definition apD_homotopic {A : Type} {B : A -> Type} {f g : forall x, B x}
   : apD f q = ap (transport B q) (p x) @ apD g q @ (p y)^.
 Proof.
   apply moveL_pV.
-  destruct q; unfold apD, transport.
+  destruct q; unfold transport.
   symmetry.
   exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
 Defined.
@@ -774,49 +774,49 @@ Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a
 Definition ap011 {A B C} (f : A -> B -> C) {x x' y y'} (p : x = x') (q : y = y')
   : f x y = f x' y'.
 Proof.
-  destruct p.
-  apply ap.
-  exact q.
+  destruct q.
+  apply (ap (fun x => f x _)).
+  exact p.
 Defined.
 
 Definition ap011_V {A B C} (f : A -> B -> C) {x x' y y'} (p : x = x') (q : y = y')
   : ap011 f p^ q^ = (ap011 f p q)^.
 Proof.
-  destruct p.
-  apply ap_V.
+  destruct q.
+  rapply ap_V.
 Defined.
 
 Definition ap011_pp {A B C} (f : A -> B -> C) {x x' x'' y y' y''}
   (p : x = x') (p' : x' = x'') (q : y = y') (q' : y' = y'')
   : ap011 f (p @ p') (q @ q') = ap011 f p q @ ap011 f p' q'.
 Proof.
-  destruct p, p'.
-  apply ap_pp.
+  destruct q, q'.
+  rapply ap_pp.
 Defined.
 
 Definition ap011_compose {A B C D} (f : A -> B -> C) (g : C -> D) {x x' y y'}
   (p : x = x') (q : y = y')
   : ap011 (fun x y => g (f x y)) p q = ap g (ap011 f p q).
 Proof.
-  destruct p; simpl.
-  apply ap_compose.
+  destruct q; simpl.
+  rapply ap_compose.
 Defined.
 
 Definition ap011_compose' {A B C D E} (f : A -> B -> C) (g : D -> A) (h : E -> B)
   {x x' y y'}
   (p : x = x') (q : y = y')
   : ap011 (fun x y => f (g x) (h y)) p q = ap011 f (ap g p) (ap h q).
 Proof.
-  destruct p; simpl.
-  apply ap_compose.
+  destruct q; simpl.
+  rapply ap_compose.
 Defined.
 
 Definition ap011_is_ap {A B C} (f : A -> B -> C) {x x' : A} {y y' : B} (p : x = x') (q : y = y')
   : ap011 f p q = ap (fun x => f x y) p @ ap (fun y => f x' y) q.
 Proof.
-  destruct p.
+  destruct q.
   symmetry.
-  apply concat_1p.
+  rapply concat_p1.
 Defined.
 
 (** It would be nice to have a consistent way to name the different ways in which this can be dependent.  The following are a sort of half-hearted attempt. *)
@@ -1391,9 +1391,9 @@ Definition ap022 {A B C} (f : A -> B -> C) {x x' y y'}
   {p p' : x = x'} (r : p = p') {q q' : y = y'} (s : q = q')
   : ap011 f p q = ap011 f p' q'.
 Proof.
-  destruct r, p.
-  apply ap02.
-  exact s.
+  destruct s, q.
+  cbn; apply ap.
+  exact r.
 Defined.
 
 (** These lemmas need better names. *)

theories/Cubical/PathSquare.v

@@ -366,7 +366,7 @@ Proof.
   refine (_ oE (equiv_concat_l (concat_pp_p _ _ _) _)^-1).
   refine (_ oE equiv_moveL_Mp _ _ _).
   refine (_ oE sq_path).
-  exact (sq_ccGG (ap_fst_path_prod _ _) (ap_snd_path_prod _ _)).
+  exact (sq_ccGG (ap_fst_path_prod' _ _) (ap_snd_path_prod' _ _)).
 Defined.
 
 Notation sq_dp_prod := equiv_sq_dp_prod.

theories/HFiber.v

@@ -117,7 +117,7 @@ Proof.
   refine (concat_p1 _ @ _).
   refine (inv_pp _ _ @ ap _ _).
   refine ((ap_V _ _)^ @ ap _ _^).
-  apply concat_p1.
+  cbn; apply concat_p1.
 Defined.
 
 (** ** The 3x3 lemma for fibrations *)

theories/Interval2.v

@@ -0,0 +1,64 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import Basics.PathGroupoids Types.Paths.
+
+Set Universe Minimization ToSet.
+Unset Universe Polymorphism.
+
+Symbol Interval : Type0.
+Symbol i0 : Interval.
+Symbol i1 : Interval.
+Symbol seg : i0 = i1.
+
+
+Symbol Interval_ind@{u}
+  : forall (P : Interval -> Type@{u})
+      (a : P i0) (b : P i1) (p : seg # a = b),
+      forall x, P x.
+
+Symbol Interval_rec@{u} : forall (P : Type@{u}) (a b : P) (p : a = b), Interval -> P.
+
+
+Rewrite Rule interval_rewrite :=
+| Interval_ind ?P ?a ?b ?p i0 => ?a
+| Interval_ind ?P ?a ?b ?p i1 => ?b
+| apD (Interval_ind ?P ?a ?b ?p) seg => ?p
+| ap (Interval_rec ?P ?a ?b ?p) seg => ?p
+.
+
+
+Require Import Metatheory.Core Metatheory.FunextVarieties.
+
+Definition interval_rec (P : Type) (a b : P) (p : a = b)
+  : Interval -> P
+  := Interval_ind (fun _ => P) a b (transport_const _ _ @ p).
+
+Definition funext_type_from_interval : Funext_type
+  := WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
+    (fun A P f g p =>
+      let h := fun (x:Interval) (a:A) =>
+        interval_rec _ (f a) (g a) (p a) x
+        in ap h seg)).
+
+
+Definition path_forall {A : Type} {P : A -> Type} (f g : forall x : A, P x)
+  : f == g -> f = g.
+Proof.
+  refine (@apD10 A P f g)^-1.
+  apply funext_type_from_interval.
+Defined.
+
+
+Definition path_forall_1 A {P : A -> Type} (f : forall x, P x)
+  : (path_forall f f (fun x => 1)) = 1.
+Proof.
+  cbn.
+  unfold htpy_ind.
+
+cbv.
+  eflexivity.
+  simpl.
+  := eta_path_forall f f 1.
+
+
+
+

theories/Metatheory/FunextVarieties.v

@@ -2,7 +2,7 @@
 
 (** * Varieties of function extensionality *)
 
-Require Import HoTT.Basics HoTT.Types.
+Require Import Basics HoTT.Types.
 Require Import Metatheory.Core.
 Local Open Scope path_scope.
 
@@ -152,10 +152,10 @@ Definition NaiveNondepFunext_implies_Funext@{i j max}
 (** ** Functional extensionality is downward closed *)
 
 (** If universe [U_i] is functionally extensional, then so are universes [U_i'] for [i' ≤ i]. *)
-Lemma Funext_downward_closed@{i j max i' j' max' | i <= max, j <= max, i' <= max', j' <= max', i' <= i, j' <= j}
+(* Lemma Funext_downward_closed@{i j max i' j' max' | i <= max, j <= max, i' <= max', j' <= max', i' <= i, j' <= j}
   `{H : Funext_type@{i j max}} : Funext_type@{i' j' max'}.
 Proof.
   hnf in *.
   (* Here we make use of cumulativity. *)
   exact (fun A P => H A P).
-Defined.
+Defined. *)

theories/Types/Arrow.v

@@ -174,8 +174,10 @@ Defined.
 
 (** The action of maps given by application. *)
 Definition ap_apply_l {A B : Type} {x y : A -> B} (p : x = y) (z : A) :
-  ap (fun f => f z) p = ap10 p z
-:= 1.
+  ap (fun f => f z) p = ap10 p z.
+Proof.
+  by destruct p.
+Defined.
 
 Definition ap_apply_Fl {A B C : Type} {x y : A} (p : x = y) (M : A -> B -> C) (z : B) :
   ap (fun a => (M a) z) p = ap10 (ap M p) z

theories/Types/Forall.v

@@ -119,8 +119,10 @@ Defined.
 
 (** The action of maps given by application. *)
 Definition ap_apply_lD {A} {B : A -> Type} {f g : forall x, B x} (p : f = g) (z : A)
-  : ap (fun f => f z) p = apD10 p z
-:= 1.
+  : ap (fun f => f z) p = apD10 p z.
+Proof.
+  by destruct p.
+Defined.
 
 Definition ap_apply_lD2 {A} {B : A -> Type} { C : forall x, B x -> Type}
            {f g : forall x y, C x y} (p : f = g) (z1 : A) (z2 : B z1)
@@ -230,8 +232,10 @@ Definition functor_forall_equiv_pb_beta {A B : Type} {P : B -> Type} (f : A -> B
   `{!IsEquiv f} (h : forall a, P (f a))
   : forall a, functor_forall_equiv_pb f h (f a) = h a.
 Proof.
-  intro a; srapply (_ @ apD h (eissect f a)); srapply (_ @ (transport_compose _ _ _ _)^).
-  srapply ap10; apply ap; apply eisadj.
+  intro a; srapply (_ @ apD h (eissect f a)).
+  rhs nrapply (transport_compose P).
+  apply transport2.
+  apply eisadj.
 Defined.
 
 (** ** Equivalences *)

theories/Types/Sum.v

@@ -6,6 +6,7 @@ Require Import Types.Empty Types.Unit Types.Prod Types.Sigma.
 (** The following are only required for the equivalence between [sum] and a sigma type *)
 Require Import Types.Bool.
 
+Unset Universe Checking.
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
 

theories/Types/Unit.v

@@ -81,7 +81,7 @@ Global Instance isequiv_unit_name@{i j} `{Funext} (A : Type@{i})
 Proof.
   refine (isequiv_adjointify _ (fun f : Unit -> _ => f tt) _ _).
   - intros f; apply path_forall@{i i j}; intros x.
-    apply ap@{i i}, path_unit.
+    apply ap, path_unit.
   - intros a; reflexivity.
 Defined.
 

theories/Types/Universe.v

@@ -4,6 +4,7 @@
 Require Import HoTT.Basics.
 Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.
 
+Unset Universe Checking.
 Local Open Scope path_scope.
 
 Generalizable Variables A B f.