(** * Dependent Product Category *)
Require Import Category.Strict.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Basics.Trunc.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope category_scope.
Local Open Scope morphism_scope.

(** ** Definition of [∀], or [∏], for categories *)
Section pi.
  Context `{Funext}.
  Variable A : Type.
  Variable P : A -> PreCategory.

  Definition pi : PreCategory.
H: Funext
A: Type
P: A -> PreCategory
PreCategory
    refine (@Build_PreCategory
              (forall a : A, P a)
              (fun s d => forall a : A, morphism (P a) (s a) (d a))
              (fun x => fun a => identity (x a))
              (fun s d d' m2 m1 => fun a => m2 a o m1 a)
              _
              _
              _
              _);
    abstract (
        repeat (intro || apply path_forall);
        auto with morphism
      ).
  Defined.
End pi.

Local Notation "'forall'  x .. y , P" := (forall x, .. (forall y, P) ..) : type_scope.
Local Notation "'forall'  x .. y , P" := (pi (fun x => .. (pi (fun y => P)) .. )) : category_scope.

(** ** The product of strict categories is strict *)
Global Instance isstrict_category_pi
       `{Funext}
       `{forall a : A, IsStrictCategory (P a)}
: IsStrictCategory (forall a, P a).
H: Funext
A: Type
P: A -> PreCategory
H0: (forall a : A, IsStrictCategory (P a))%type
IsStrictCategory (forall a : A, P a)
Proof.
H: Funext
A: Type
P: A -> PreCategory
H0: (forall a : A, IsStrictCategory (P a))%type
IsStrictCategory (forall a : A, P a)
  typeclasses eauto.
Qed.

Local Set Warnings Append "-notation-overridden".
Module Export CategoryPiNotations.
  Notation "'forall'  x .. y , P" := (forall x, .. (forall y, P) ..)%type : type_scope.
  Notation "'forall'  x .. y , P" := (pi (fun x => .. (pi (fun y => P)) .. )) : category_scope.
End CategoryPiNotations.