Merge remote-tracking branch 'origin/master' into coq-8.15

Functor/Hom.v

@@ -2,6 +2,7 @@ Require Import Category.Lib.
 Require Import Category.Theory.Category.
 Require Import Category.Theory.Functor.
 Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Theory.Isomorphism.
 Require Import Category.Construction.Product.
 Require Import Category.Construction.Opposite.
 Require Import Category.Instance.Fun.
@@ -74,6 +75,23 @@ Proof.
     now rewrite Fnat, id_right).
 Defined.
 
+Corollary Yoneda_Embedding' (C: Category) (c d : C) :
+  @IsIsomorphism Sets {| carrier := hom d c |}
+                 {| carrier := hom (fobj[C] c) (fobj[C] d) |}
+                 {| morphism := @fmap _ _ (Curried_Hom C) c d;
+                            proper_morphism := fmap_respects _ _ |}.
+Proof.
+  apply bijective_is_iso.
+  - abstract(assert (H := Yoneda_Faithful C); constructor;
+             intros x y eq; apply H; exact eq).
+  - constructor. simpl. 
+    intro A; exists (@prefmap _ _ _ (Yoneda_Full C) _ _ A ).
+    abstract(intros x f; unfold op;
+             assert (M := @fmap_sur _ _ _ (Yoneda_Full C));
+             specialize M with _ _ A; simpl in M;
+             unfold op in M; apply M).
+Defined.
+
 Program Definition CoHom_Alt `(C : Category) : C ∏ C^op ⟶ Sets :=
   Hom C ◯ Swap.
 
@@ -83,23 +101,9 @@ Program Definition CoHom `(C : Category) : C ∏ C^op ⟶ Sets := {|
   fmap := fun x y (f : x ~{C ∏ C^op}~> y) =>
     {| morphism := fun g => snd f ∘ g ∘ fst f |}
 |}.
+Next Obligation. now rewrite <- ! comp_assoc. Qed.
 
-Program Definition Curried_CoHom `(C : Category) : C ⟶ [C^op, Sets] := {|
-  fobj := fun x => {|
-    fobj := fun y => {| carrier := @hom (C^op) x y
-                      ; is_setoid := @homset (C^op) x y |};
-    fmap := fun y z (f : y ~{C^op}~> z) =>
-              {| morphism := fun (g : x ~{C^op}~> y) =>
-                               (f ∘ g) : x ~{C^op}~> z |}
-  |};
-  fmap := fun x y (f : x ~{C}~> y) => {|
-    transform := fun _ => {| morphism := fun g => g ∘ op f |}
-  |}
-|}.
-Next Obligation.
-  simpl; intros.
-  symmetry.
-  now rewrite !comp_assoc.
-Qed.
+Definition Curried_CoHom `(C : Category) : C ⟶ [C^op, Sets] :=
+  Curried_Hom C^op.
 
 Notation "[Hom ─ , A ]" := (@Curried_CoHom _ A) : functor_scope.

Instance/Comp.v

@@ -250,7 +250,7 @@ Section Examples.
    and long. *)
 
 (* Group operations *)
-Inductive Group_operation :=
+Inductive Group_operation : Set :=
   | one : Group_operation  (* unit *)
   | mul : Group_operation  (* multiplication *)
   | inv : Group_operation. (* inverse *)
@@ -283,7 +283,7 @@ Definition inv' {G : OpAlgebra GroupOp} (x : G) :=
   op G inv (fun _ => x).
 
 (* There are five group equations. *)
-Inductive Group_equation :=
+Inductive Group_equation : Set :=
   | assoc : Group_equation
   | unit_left : Group_equation
   | unit_right : Group_equation

Instance/Fun/Cartesian.v

@@ -0,0 +1,107 @@
+Require Import Category.Lib.
+Require Import Category.Theory.Category.
+Require Import Category.Theory.Functor.
+Require Import Category.Theory.Natural.Transformation.
+Require Import Category.Instance.Sets.
+Require Import Category.Instance.Fun.
+Require Import Category.Structure.Cartesian.
+Require Import Category.Lib.Tactics2.
+
+Proposition fmap_respects' (C D : Category) (F : C ⟶ D) : forall (x y : C) (f g: hom x y),
+    f ≈ g -> fmap[F] f ≈ fmap[F] g.
+Proof. now apply fmap_respects. Defined.
+#[export] Hint Resolve fmap_respects' : cat.
+
+Proposition ump_product' (C : Category) `{@Cartesian C} (x y z: C)
+  (h h': z ~> x × y) : (exl ∘ h) ≈ (exl ∘ h') -> (exr ∘ h) ≈ (exr ∘ h') -> h ≈ h'.
+Proof.
+  intros.
+  assert (RW: h ≈ fork (exl ∘ h) (exr ∘ h)). {
+  apply (snd (ump_products _ _ _)); split; reflexivity.
+  }
+  rewrite RW; symmetry.
+  apply (snd (ump_products _ _ _)); split; symmetry; assumption. 
+Qed.
+
+Proposition ump_product_auto1 (C : Category) `{@Cartesian C} (x y z: C)
+  (h : z ~> x × y) (f : z ~> x) (g : z ~> y) : (exl ∘ h) ≈ f -> (exr ∘ h) ≈ g -> h ≈ fork f g.
+Proof.
+  intros. apply (snd (ump_products _ _ _)); split; trivial.
+Qed.
+
+Proposition ump_product_auto2 (C : Category) `{@Cartesian C} (x y z: C)
+  (h : z ~> x × y) (f : z ~> x) (g : z ~> y) : (exl ∘ h) ≈ f -> (exr ∘ h) ≈ g -> fork f g ≈ h.
+Proof.
+  intros. symmetry. apply (snd (ump_products _ _ _)); split; trivial.
+Qed.
+
+#[export] Hint Resolve ump_product_auto1 : cat.
+#[export] Hint Resolve ump_product_auto2 : cat.
+(* #[export] Hint Resolve ump_product' : cat. *)
+
+#[export] Hint Rewrite @exl_fork_assoc  : categories.
+#[export] Hint Rewrite @exl_fork_comp : categories.
+#[export] Hint Rewrite @exr_fork_assoc  : categories.
+#[export] Hint Rewrite @exr_fork_comp : categories.
+
+Proposition ump_product_auto3 (C : Category) `{@Cartesian C}
+ (c d p q: C) (h : c ~> d) (f : d ~> p) (g : d ~> q) (k : c ~> p × q) :
+ f ∘ h ≈ exl ∘ k -> g ∘ h ≈ exr ∘ k -> (fork f g ∘ h) ≈ k.
+Proof.
+  intros H1 H2.
+  rewrite <- fork_comp.
+  apply ump_product_auto2; symmetry; assumption.
+Qed.
+
+Proposition ump_product_auto4 (C : Category) `{@Cartesian C}
+ (c d p q: C) (h : c ~> d) (f : d ~> p) (g : d ~> q) (k : c ~> p × q) :
+ f ∘ h ≈ exl ∘ k -> g ∘ h ≈ exr ∘ k -> k ≈ (fork f g ∘ h).
+Proof.
+  intros H1 H2.
+  rewrite <- fork_comp.
+  apply ump_product_auto1; symmetry; assumption.
+Qed.
+
+#[export] Hint Resolve ump_product_auto3 : cat.
+#[export] Hint Resolve ump_product_auto4 : cat.
+
+Ltac component_of_nat_trans :=
+  match goal with
+  | [ H : @Transform ?C ?D ?F ?G |- @hom ?D (fobj[?F] ?x) (fobj[?G] ?x) ] => apply H
+  end.
+#[export] Hint Extern 1 (hom (fobj[ _ ] ?x) (fobj[ _ ] ?x)) => component_of_nat_trans : cat.
+#[local] Hint Rewrite @fmap_comp : categories.
+#[local] Hint Rewrite @exl_split : categories.
+#[local] Hint Rewrite @exr_split : categories.
+
+#[export]
+Instance Functor_Category_Cartesian (C D : Category) (_ : @Cartesian D) : @Cartesian (@Fun C D).
+Proof.
+  unshelve econstructor.
+  - simpl. intros F G. unshelve econstructor.
+    + exact (fun c => fobj[F] c × fobj[G] c).
+    + exact (fun x y f => Cartesian.split (fmap[F] f) (fmap[G] f)).
+    + abstract(intros x y; repeat(intro); apply split_respects; auto with cat).
+    + abstract(intro; simpl; unfold split; auto with cat).
+    + abstract(intros x y z f g; simpl; unfold split; auto with cat).
+  - intros F G H σ τ. cbn in *.
+    unshelve econstructor; simpl.
+    + intro x. simpl. auto with cat.
+    + abstract(intros x y f;
+      unfold split; autorewrite with categories;
+      apply ump_product_auto3; autorewrite with categories;
+        destruct σ, τ; auto). 
+    + abstract(intros x y f; destruct σ, τ; unfold split; auto with cat).
+  - simpl. intros F G; unshelve econstructor.
+    + intro a. simpl. exact exl.
+    + abstract(simpl; intros; now autorewrite with categories).
+    + abstract(simpl; intros; now autorewrite with categories).
+  - simpl; intros F G. unshelve econstructor.
+    + intro a. simpl. exact exr.
+    + abstract(simpl; intros; now autorewrite with categories).
+    + abstract(simpl; intros; now autorewrite with categories).
+  - abstract(simpl; repeat(intro); simpl; auto with cat).
+  - simpl. intros F G H s t fk. split.
+    + abstract(intro l; split; intro; rewrite l; now autorewrite with categories).
+    + abstract(intros [l1 l2] x; rewrite <- l1, <- l2; auto with cat).
+Defined.

Instance/Lambda/Eval.v

@@ -17,14 +17,14 @@ Section Eval.
 
 Import ListNotations.
 
-Inductive Closed : Ty → Type :=
+Inductive Closed : Ty → Set :=
   | Closure {Γ τ} : Exp Γ τ → ClEnv Γ → Closed τ
 
-with ClEnv : Env → Type :=
+with ClEnv : Env → Set :=
   | NoCl : ClEnv []
   | AddCl {Γ τ} : Value τ → ClEnv Γ → ClEnv (τ :: Γ)
 
-with Value : Ty → Type :=
+with Value : Ty → Set :=
   | Val {Γ τ} (x : Exp Γ τ) : ValueP x → ClEnv Γ → Value τ.
 
 Derive Signature NoConfusion NoConfusionHom Subterm for ClEnv Closed Value.
@@ -43,7 +43,7 @@ Fixpoint snoc {a : Type} (x : a) (xs : list a) : list a :=
   | x :: xs => x :: snoc x xs
   end.
 
-Inductive EvalContext : Ty → Ty → Type :=
+Inductive EvalContext : Ty → Ty → Set :=
   | MT {τ} : EvalContext τ τ
   | AR {dom cod τ} :
     Closed dom → EvalContext cod τ → EvalContext (dom ⟶ cod) τ
@@ -56,7 +56,7 @@ Inductive EvalContext : Ty → Ty → Type :=
 
 Derive Signature NoConfusion NoConfusionHom Subterm for EvalContext.
 
-Inductive Σ : Ty → Type :=
+Inductive Σ : Ty → Set :=
   | MkΣ {u    : Ty}
         (exp  : Closed u)
         {τ    : Ty}

Instance/Lambda/Exp.v

@@ -19,13 +19,13 @@ Open Scope Ty_scope.
 
 Definition Env := list Ty.
 
-Inductive Var : Env → Ty → Type :=
+Inductive Var : Env → Ty → Set :=
   | ZV {Γ τ}    : Var (τ :: Γ) τ
   | SV {Γ τ τ'} : Var Γ τ → Var (τ' :: Γ) τ.
 
 Derive Signature NoConfusion EqDec for Var.
 
-Inductive Exp Γ : Ty → Type :=
+Inductive Exp Γ : Ty → Set :=
   | EUnit         : Exp Γ TyUnit
 
   | Pair {τ1 τ2}  : Exp Γ τ1 → Exp Γ τ2 → Exp Γ (TyPair τ1 τ2)

Instance/Lambda/Full.v

@@ -24,7 +24,7 @@ Open Scope Ty_scope.
 
 (* A context defines a hole which, after substitution, yields an expression of
    the index type. *)
-Inductive Frame Γ : Ty → Ty → Type :=
+Inductive Frame Γ : Ty → Ty → Set :=
   | F_PairL {τ1 τ2}  : Exp Γ τ2 → Frame τ1 (τ1 × τ2)
   | F_PairR {τ1 τ2}  : Exp Γ τ1 → Frame τ2 (τ1 × τ2)
   | F_Fst {τ1 τ2}    : Frame (τ1 × τ2) τ1
@@ -34,7 +34,7 @@ Inductive Frame Γ : Ty → Ty → Type :=
 
 Derive Signature NoConfusion Subterm for Frame.
 
-Inductive Ctxt Γ : Ty → Ty → Type :=
+Inductive Ctxt Γ : Ty → Ty → Set :=
   | C_Nil {τ}         : Ctxt τ τ
   | C_Cons {τ τ' τ''} : Frame Γ τ' τ → Ctxt τ'' τ' → Ctxt τ'' τ.
 
@@ -65,7 +65,7 @@ Theorem Ctxt_comp_assoc {Γ τ τ' τ'' τ'''}
   Ctxt_comp C (Ctxt_comp C' C'') = Ctxt_comp (Ctxt_comp C C') C''.
 Proof. induction C; simpl; auto; now f_equal. Qed.
 
-Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Redex {Γ} : ∀ {τ}, Exp Γ τ → Exp Γ τ → Set :=
   | R_Beta {dom cod} (e : Exp (dom :: Γ) cod) v :
     ValueP v →
     Redex (APP (LAM e) v) (SubExp {|| v ||} e)
@@ -82,7 +82,7 @@ Derive Signature for Redex.
 
 Unset Elimination Schemes.
 
-Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Type :=
+Inductive Plug {Γ τ'} (e : Exp Γ τ') : ∀ {τ}, Ctxt Γ τ' τ → Exp Γ τ → Set :=
   | Plug_Hole : Plug (C_Nil _) e
 
   | Plug_PairL {τ1 τ2} {C : Ctxt Γ τ' τ1} {e' : Exp Γ τ1} {e2 : Exp Γ τ2} :
@@ -147,7 +147,7 @@ Theorem Plug_id_left {Γ τ τ'} {C : Ctxt Γ τ' τ} {x : Exp Γ τ'} {y : Exp
   Plug_comp Plug_id P ~= P.
 *)
 
-Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step {Γ τ} : Exp Γ τ → Exp Γ τ → Set :=
   | StepRule {τ'} {C : Ctxt Γ τ' τ} {e1 e2 : Exp Γ τ'} {e1' e2' : Exp Γ τ} :
     Plug e1 C e1' →
     Plug e2 C e2' →

Instance/Lambda/Norm.v

@@ -100,6 +100,8 @@ Arguments SN_Sub {Γ Γ'} /.
 
 Definition SN_halts {Γ τ} {e : Γ ⊢ τ} : SN e → halts e := ExpP_P _.
 
+#[local] Transparent ExpP.
+
 Lemma step_preserves_SN {Γ τ} {e e' : Γ ⊢ τ} :
   (e ---> e') → SN e → SN e'.
 Proof.

Instance/Lambda/Ren.v

@@ -15,7 +15,7 @@ Section Ren.
 
 Import ListNotations.
 
-Inductive Ren : Env → Env → Type :=
+Inductive Ren : Env → Env → Set :=
   | NoRen : Ren [] []
   | Drop {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) Γ'
   | Keep {τ Γ Γ'} : Ren Γ Γ' → Ren (τ :: Γ) (τ :: Γ').

Instance/Lambda/Step.v

@@ -25,7 +25,7 @@ Open Scope Ty_scope.
 
 Reserved Notation " t '--->' t' " (at level 40).
 
-Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Type :=
+Inductive Step : ∀ {Γ τ}, Exp Γ τ → Exp Γ τ → Set :=
   | ST_Pair1 Γ τ1 τ2 (x x' : Exp Γ τ1) (y : Exp Γ τ2) :
     x ---> x' →
     Pair x y ---> Pair x' y

Instance/Lambda/Sub.v

@@ -16,7 +16,7 @@ Section Sub.
 
 Import ListNotations.
 
-Inductive Sub (Γ : Env) : Env → Type :=
+Inductive Sub (Γ : Env) : Env → Set :=
   | NoSub : Sub []
   | Push {Γ' τ} : Exp Γ τ → Sub Γ' → Sub (τ :: Γ').
 

Instance/Lambda/Ty.v

@@ -7,7 +7,7 @@ Set Transparent Obligations.
 
 Section Ty.
 
-Inductive Ty : Type :=
+Inductive Ty : Set :=
   | TyUnit  : Ty
   | TyPair  : Ty → Ty → Ty
   | TyArrow : Ty → Ty → Ty.

Instance/Lambda/Value.v

@@ -16,7 +16,7 @@ Open Scope Ty_scope.
 
 (* [ValueP] is an inductive proposition that indicates whether an expression
    represents a value, i.e., that it does reduce any further. *)
-Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Type :=
+Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Set :=
   | UnitP : ValueP EUnit
   | PairP {τ1 τ2} {x : Exp Γ τ1} {y : Exp Γ τ2} :
     ValueP x → ValueP y → ValueP (Pair x y)

Instance/Parallel.v

@@ -12,9 +12,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify equalizers. *)
 
-Inductive ParObj : Type := ParX | ParY.
+Inductive ParObj : Set := ParX | ParY.
 
-Inductive ParHom : bool → ParObj → ParObj → Type :=
+Inductive ParHom : bool → ParObj → ParObj → Set :=
   | ParIdX : ParHom true ParX ParX
   | ParIdY : ParHom true ParY ParY
   | ParOne : ParHom true ParX ParY

Instance/Roof.v

@@ -15,9 +15,9 @@ Generalizable All Variables.
 
   This is used to build diagrams that identify spans and pullbacks. *)
 
-Inductive RoofObj : Type := RNeg | RZero | RPos.
+Inductive RoofObj : Set := RNeg | RZero | RPos.
 
-Inductive RoofHom : RoofObj → RoofObj → Type :=
+Inductive RoofHom : RoofObj → RoofObj → Set :=
   | IdNeg   : RoofHom RNeg  RNeg
   | ZeroNeg : RoofHom RZero RNeg
   | IdZero  : RoofHom RZero RZero