(** An axiomatisation of “1-dimensional W-types”, a class of HIT’s which — while probably(?) not strong enough to give the full generality of “all HIT’s” (whatever that means) — is fairly large, and in particular is general enough to present most of the dfficulties that arise in formally giving the fully general definition. – pll, 15-11-2012 *) Set Printing Universes. Require Import Paths Fibrations ExtensionalityAxiom. Notation "'Paths'" := paths. Definition Paths_over {X : Type} {Y : X -> Type} {x0 x1:X} (p:Paths x0 x1) : (Y x0) -> (Y x1) -> Type := fun y0 => Paths (transport p y0). Definition transport_d {X : Type} {Y : X -> Type} {Z : forall x, Y x -> Type} {x0 x1:X} (p:Paths x0 x1) {y : Y x0} : (Z x0 y) -> (Z x1 (transport p y)). Proof. path_induction. Defined. Definition Paths_over2 {X : Type} {Y : X -> Type} {Z : forall x, Y x -> Type} {x0 x1:X} (p:Paths x0 x1) {y0 y1} (q : Paths_over p y0 y1) : (Z x0 y0) -> (Z x1 y1) -> Type := fun z0 => Paths (transport q (transport_d p z0)). Lemma dep2_map_on_paths {I} {X} {Y : forall (i:I) (x:X i), Type} (f : forall i x, Y i x) {i1 i2} {p : i1 = i2} {x1 : X i1} {x2 : X i2} (q : Paths_over p x1 x2) : Paths_over2 p q (f i1 x1) (f i2 x2). Proof. unfold Paths_over2. unfold Paths_over in q. path_induction. Defined. Section Signatures_0. Record Sig0 := { Index : Type ; Constructor : Type ; Arity : Constructor -> Type ; inp_index : forall {c : Constructor}, Arity c -> Index ; outp_index : Constructor -> Index }. Global Implicit Arguments outp_index [[s]]. Global Implicit Arguments Arity [[s]]. Global Implicit Arguments inp_index [[s] [c]]. Definition Poly0 (S : Sig0) : (Index S -> Type) -> Constructor S -> Type := fun X c => forall a : Arity c, X (inp_index a). (* Was originally the following def as more expected; but Σ-types are a pain in the neck to work with (blasted [existT] not inferring its first arguments…) Definition Poly_Funct (S : Sig0) : (S.(Index) -> Type) -> Type := fun X => { c : S.(Constructor) & forall a : Arity c, X (inp_index a) }. *) Record W0_Alg (S : Sig0) := { Carrier : Index S -> Type ; fold : forall c (inps : Poly0 S Carrier c), Carrier (outp_index c) }. Coercion Carrier : W0_Alg >-> Funclass. Global Implicit Arguments Carrier [[S]]. Global Implicit Arguments fold [[S] [w]]. Definition Poly0_d (S : Sig0) (X : Index S -> Type) : (forall i : Index S, X i -> Type) -> forall (c : Constructor S), Poly0 S X c -> Type := fun Y c inps => forall a : Arity c, Y (inp_index a) (inps a). Record W0_Alg_d (S : Sig0) (X : W0_Alg S) := { Carrier_d : forall i : Index S, X i -> Type ; fold_d : forall c (inps : Poly0 S X c) (inps_d : Poly0_d S X Carrier_d c inps), Carrier_d (outp_index c) (fold c inps) }. Coercion Carrier_d : W0_Alg_d >-> Funclass. Global Implicit Arguments Carrier_d [[S] [X]]. Global Implicit Arguments fold_d [[S] [X] [w]]. Record alg_section {S} {X} (Y : W0_Alg_d S X) := { sec_map : forall {i} (x : X i), Y i x ; sec_homo : forall c inps, fold_d c inps (fun a => sec_map (inps a)) = sec_map (fold c inps) }. Coercion sec_map : alg_section >-> Funclass. Global Implicit Arguments sec_map [[S] [X] [Y] [i]]. (* Oddly, this doesn’t seem to succeed in making [i] implicit; I’m not sure why not. *) Global Implicit Arguments sec_homo [[S] [X] [Y] [a]]. End Signatures_0. Section Misc_defs_0. Inductive W0 (S : Sig0) : S.(Index) -> Type := | w0 (c : S.(Constructor)) (inps : forall a : Arity c, W0 S (inp_index a)) : W0 S (outp_index c). Fixpoint interp {S} (X : W0_Alg S) {i} (t : W0 S i) : X i := match t with | (w0 c inps) => fold c (fun j => interp X (inps j)) end. Fixpoint interp_d {S} {X : W0_Alg S} (Y : W0_Alg_d S X) {i} (t : W0 S i) : Y i (interp X t) := match t with | (w0 c inps) => fold_d c (fun a => interp X (inps a)) (fun a => interp_d Y (inps a)) end. Fixpoint interp_section_homo {S} {X : W0_Alg S} {Y : W0_Alg_d S X} (s : alg_section Y) {i} (t : W0 S i) : interp_d Y t = s _ (interp X t). Proof. intros. destruct t as [c inps]; simpl. path_via (fold_d c (fun a : Arity c => interp X (inps a)) (fun a : Arity c => s _ (interp X (inps a)))). set (H := funext_dep). unfold funext_dep_statement in H. apply (H (f :=(fold_d c (fun a : Arity c => interp X (inps a)) (fun a : Arity c => interp_d Y (inps a)))) (g := (fold_d c (fun a : Arity c => interp X (inps a)) (fun a : Arity c => s (inp_index a) (interp X (inps a)))))). unfold ext_dep_eq; intros. apply interp_section_homo. apply sec_homo. Defined. Definition add_vars (S : Sig0) V (f : V -> Index S) : Sig0 := {| Index := (S.(Index)) ; Constructor := (S.(Constructor) + V)%type ; Arity := fun c => match c with | inl c => Arity c | inr _ => False end ; inp_index := fun c => match c with | inl c => inp_index | inr _ => fun f => match f with end end ; outp_index := fun c => match c with | inl c => outp_index c | inr x => f x end |}. Definition Alg_add_vars {S} (X : W0_Alg S) V (f : V -> Index S) (f1 : forall v, X (f v)) : W0_Alg (add_vars S V f). Proof. esplit. instantiate (1 := X). intros c inps. destruct c as [c | v]; simpl in *. (* Case c = constructor of S *) exact (fold c inps). (* Case c = var *) exact (f1 v). Defined. Definition Alg_add_vars_d {S} {X : W0_Alg S} (Y : W0_Alg_d S X) V (f : V -> Index S) (f1 : forall v, X (f v)) (f2 : forall v, Y (f v) (f1 v)) : W0_Alg_d (add_vars S V f) (Alg_add_vars X V f f1). Proof. esplit. instantiate (1 := Y). intros c inps inps_d. destruct c as [c | v]; simpl in *. (* Case c = constructor of S *) exact (fold_d c inps inps_d). (* Case c = var *) exact (f2 v). Defined. Definition section_add_vars {S} {X} {Y : W0_Alg_d S X} (s : alg_section Y) V (f : V -> Index S) (f1 : forall v, X (f v)) : alg_section (Alg_add_vars_d Y V f f1 (fun v => s _ (f1 v))). Proof. esplit. instantiate (1 := s). (* To prove: homomorphism. *) intros; destruct c; simpl. apply sec_homo. auto. Defined. Set Printing Coercions. Definition section_interp_add_vars {S} {X} {Y : W0_Alg_d S X} (s : alg_section Y) V (f : V -> Index S) (f1 : forall v, X (f v)) {i} (t : W0 (add_vars S V f) i) : interp_d (Alg_add_vars_d Y V f f1 (fun v => s _ (f1 v))) t = s _ (interp (Alg_add_vars X V f f1) t) := interp_section_homo (section_add_vars s V f f1) t. End Misc_defs_0. Section Signatures_1. Record Sig1 := { Undlg_Sig0 : Sig0 ; Constructor1 : Type ; Arity1 : Constructor1 -> Type ; inp_index1 : forall {c : Constructor1}, Arity1 c -> Index Undlg_Sig0 ; src_index : Constructor1 -> Index Undlg_Sig0 ; src : forall c : Constructor1, (W0 (add_vars Undlg_Sig0 (Arity1 c) (inp_index1)) (src_index c)) ; tgt_index : Constructor1 -> Index Undlg_Sig0 ; tgt : forall c : Constructor1, (W0 (add_vars Undlg_Sig0 (Arity1 c) (inp_index1)) (tgt_index c)) ; outp_index1 : forall c : Constructor1, Paths (src_index c) (tgt_index c) }. Coercion Undlg_Sig0 : Sig1 >-> Sig0. Global Implicit Arguments Arity1 [[s]]. Global Implicit Arguments inp_index1 [[s] [c]]. Global Implicit Arguments src_index [[s]]. Global Implicit Arguments src [[s]]. Global Implicit Arguments tgt_index [[s]]. Global Implicit Arguments tgt [[s]]. Global Implicit Arguments outp_index1 [[s]]. Definition Poly1 (S : Sig1) : (Index S -> Type) -> Constructor1 S -> Type := fun X c => forall a : Arity1 c, X (inp_index1 a). Definition poly1_src0 {S : Sig1} {X : W0_Alg S} : forall c (inps : Poly1 S X c), X (src_index c) := fun c inps => let X' := Alg_add_vars X (Arity1 c) inp_index1 inps in (interp X' (src c)). Definition poly1_tgt0 {S : Sig1} {X : W0_Alg S} : forall c (inps : Poly1 S X c), X (tgt_index c) := fun c inps => let X' := Alg_add_vars X (Arity1 c) inp_index1 inps in (interp X' (tgt c)). (* In practice this seems less convenient to use, but it’s helpful to think of: Definition Fold1_Type (S1 : Sig1 S) (X : W0_Alg S) : Type := forall (c : Constructor1 S) (inps : Poly1 S X c), Paths_over (outp_index1 c) (poly1_src0 c inps) (poly1_tgt0 c inps). *) Record W1_Alg (S : Sig1) := { Undlg_W0_Alg : W0_Alg S ; fold1 : forall c (inps : Poly1 S (Undlg_W0_Alg) c), Paths_over (outp_index1 c) (poly1_src0 c inps) (poly1_tgt0 c inps) }. Coercion Undlg_W0_Alg : W1_Alg >-> W0_Alg. Global Implicit Arguments fold1 [[S] [w]]. Definition Poly1_d (S : Sig1) (X : Index S -> Type) : (forall i : Index S, X i -> Type) -> forall (c : Constructor1 S), Poly1 S X c -> Type := fun Y => fun c inps => forall a : Arity1 c, Y (inp_index1 a) (inps a). Definition poly1_src0_d {S : Sig1} {X : W0_Alg S} {Y : W0_Alg_d S X} : forall c (inps : Poly1 S X c) (inps_d : Poly1_d S X Y c inps), Y (src_index c) (poly1_src0 c inps) := fun c inps inps_d => let Y' := Alg_add_vars_d Y (Arity1 c) inp_index1 inps inps_d in (interp_d Y' (src c)). Definition poly1_tgt0_d {S : Sig1} {X : W0_Alg S} {Y : W0_Alg_d S X} : forall c (inps : Poly1 S X c) (inps_d : Poly1_d S X Y c inps), Y (tgt_index c) (poly1_tgt0 c inps) := fun c inps inps_d => let Y' := Alg_add_vars_d Y (Arity1 c) inp_index1 inps inps_d in (interp_d Y' (tgt c)). Record W1_Alg_d (S : Sig1) (X : W1_Alg S) := { Undlg_W0_Alg_d : W0_Alg_d S X ; fold1_d : forall (c : Constructor1 S) (inps : Poly1 S X c) (inps_d : Poly1_d S X Undlg_W0_Alg_d c inps), Paths_over2 (outp_index1 c) (fold1 c inps) (poly1_src0_d c inps inps_d) (poly1_tgt0_d c inps inps_d) }. Coercion Undlg_W0_Alg_d : W1_Alg_d >-> W0_Alg_d. Global Implicit Arguments fold1_d [[S] [X] [w]]. Definition section_poly1_src0_commutes {S : Sig1} {X : W0_Alg S} {Y : W0_Alg_d S X} (s : alg_section Y) : forall c (inps : Poly1 S X c), poly1_src0_d c inps (fun a => s _ (inps a)) = s _ (poly1_src0 c inps). Proof. intros. unfold poly1_src0_d. unfold poly1_src0. apply (section_interp_add_vars s (Arity1 c) inp_index1 inps). Defined. Definition section_poly1_tgt0_commutes {S : Sig1} {X : W0_Alg S} {Y : W0_Alg_d S X} (s : alg_section Y) : forall c (inps : Poly1 S X c), poly1_tgt0_d c inps (fun a => s _ (inps a)) = s _ (poly1_tgt0 c inps). Proof. intros. unfold poly1_tgt0_d. unfold poly1_tgt0. apply (section_interp_add_vars s (Arity1 c) inp_index1 inps). Defined. (* To define the 1-homomorphism condition for a section [s] of a W1-algebra, a little coercion is needed. Morally, the condition is [ fold_d c inps (fun a => s _ (inps a)) = dep2_map_on_paths s (fold1 c inps) ] but compare the types of these: fold_d c inps inps_d : Paths_over2 (outp_index1 c) (fold1 c inps) (poly1_src0_d c inps inps_d) (poly1_tgt0_d c inps inps_d) dep2_map_on_paths undlg_alg0_section (fold1 c inps) : Paths_over2 (outp_index1 c) (fold1 c inps) (undlg_alg0_section (src_index c) (poly1_src0 c inps)) (undlg_alg0_section (tgt_index c) (poly1_tgt0 c inps)) To go between these, we need to rewrite along the equality witnessing that the underlying 0-algebra section really is a section. Since this conversion is cumbersome to write inline, we define it in advance. *) Definition homo1_tgt {S} {X} {Y : W1_Alg_d S X} (s : alg_section Y) c inps : let inps_d := (fun a => s _ (inps a)) in Paths_over2 (outp_index1 c) (fold1 c inps) (poly1_src0_d c inps inps_d) (poly1_tgt0_d c inps inps_d). Proof. simpl. unfold Paths_over2. path_via (transport (fold1 c inps) (transport_d (outp_index1 c) (s _ (poly1_src0 c inps)))). (* Whoa! It applies map_dep right off the bat! Impressed! *) apply section_poly1_src0_commutes. path_via (s _ (poly1_tgt0 c inps)). apply (dep2_map_on_paths s (fold1 c inps)). symmetry; apply section_poly1_tgt0_commutes. Defined. Record alg1_section {S} {X} (Y : W1_Alg_d S X) := { undlg_alg0_section : alg_section Y ; sec_homo1 : forall c inps, let inps_d := (fun a => undlg_alg0_section _ (inps a)) in fold1_d c inps inps_d = homo1_tgt undlg_alg0_section c inps }. Coercion undlg_alg0_section : alg1_section >-> alg_section. Global Implicit Arguments sec_homo1 [[S] [X] [Y] [a]]. Record W1_Type (S : Sig1) := { Undlg_W1_Alg : W1_Alg S ; elim1 : forall P : W1_Alg_d S Undlg_W1_Alg, alg1_section P }. Coercion Undlg_W1_Alg : W1_Type >-> W1_Alg. Global Implicit Arguments elim1 [[S]]. Axiom W1 : forall S : Sig1, W1_Type S. End Signatures_1. (* Local Variables: coq-prog-name: "hoqtop" End: *)