(** * ∑-categories on objects - a generalization of subcategories *)
Require Import HoTT.Basics HoTT.Types.
Require Import Category.Core Functor.Core Category.Sigma.Core.
Require Functor.Composition.Core Functor.Identity.
Require Import Functor.Paths.
Import Functor.Identity.FunctorIdentityNotations.
Import Functor.Composition.Core.FunctorCompositionCoreNotations.

Set Implicit Arguments.
Generalizable All Variables.

Local Notation sig_type := Overture.sig.
Local Notation pr1_type := Overture.pr1.

Local Open Scope morphism_scope.
Local Open Scope functor_scope.

Section sig_obj.
  Variable A : PreCategory.
  Variable Pobj : A -> Type.

  (** ** Definition of [sig_obj]-precategory *)
  Definition sig_obj : PreCategory
    := @Build_PreCategory
         (sig_type Pobj)
         (fun s d => morphism A (pr1_type s) (pr1_type d))
         (fun x => @identity A (pr1_type x))
         (fun s d d' m1 m2 => m1 o m2)%morphism
         (fun _ _ _ _ => associativity A _ _ _ _)
         (fun _ _ => left_identity A _ _)
         (fun _ _ => right_identity A _ _)
         _.

  (** ** First projection functor *)
  Definition pr1_obj : Functor sig_obj A
    := Build_Functor
         sig_obj A
         (@pr1_type _ _)
         (fun s d m => m)
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Definition sig_obj_as_sig : PreCategory
    := @sig A Pobj (fun _ _ _ => Unit) _ (fun _ => tt) (fun _ _ _ _ _ _ _ => tt).

  Definition sig_functor_obj : Functor sig_obj_as_sig sig_obj
    := Build_Functor sig_obj_as_sig sig_obj
                     (fun x => x)
                     (fun _ _ => @pr1_type _ _)
                     (fun _ _ _ _ _ => idpath)
                     (fun _ => idpath).

  Definition sig_functor_obj_inv : Functor sig_obj sig_obj_as_sig
    := Build_Functor sig_obj sig_obj_as_sig
                     (fun x => x)
                     (fun _ _ m => exist _ m tt)
                     (fun _ _ _ _ _ => idpath)
                     (fun _ => idpath).

  Local Open Scope functor_scope.

  Lemma sig_obj_eq `{Funext}
  : sig_functor_obj o sig_functor_obj_inv = 1
    /\ sig_functor_obj_inv o sig_functor_obj = 1.
A: PreCategory
Pobj: A -> Type
H: Funext
(sig_functor_obj o sig_functor_obj_inv = 1) *
(sig_functor_obj_inv o sig_functor_obj = 1)
  Proof.
A: PreCategory
Pobj: A -> Type
H: Funext
(sig_functor_obj o sig_functor_obj_inv = 1) *
(sig_functor_obj_inv o sig_functor_obj = 1)
    split; path_functor; trivial.
A: PreCategory
Pobj: A -> Type
H: Funext
transport
  (fun GO : sig_type Pobj -> sig_type Pobj =>
   forall s d : sig_type Pobj,
   sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit) ->
   sig_type (fun _ : morphism A (pr1_type (GO s)) (pr1_type (GO d)) => Unit))
  1
  (fun (s d : sig_type Pobj)
     (m : sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit)) =>
   (pr1_type m; tt)) =
(fun s d : sig_type Pobj => idmap)
    apply path_forall; intros [].
A: PreCategory
Pobj: A -> Type
H: Funext
proj1: A
proj2: Pobj proj1
transport
  (fun GO : sig_type Pobj -> sig_type Pobj =>
   forall s d : sig_type Pobj,
   sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit) ->
   sig_type (fun _ : morphism A (pr1_type (GO s)) (pr1_type (GO d)) => Unit))
  1
  (fun (s d : sig_type Pobj)
     (m : sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit)) =>
   (pr1_type m; tt))
  (proj1; proj2) =
(fun d : sig_type Pobj => idmap)
    apply path_forall; intros [].
A: PreCategory
Pobj: A -> Type
H: Funext
proj1: A
proj2: Pobj proj1
proj0: A
proj3: Pobj proj0
transport
  (fun GO : sig_type Pobj -> sig_type Pobj =>
   forall s d : sig_type Pobj,
   sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit) ->
   sig_type (fun _ : morphism A (pr1_type (GO s)) (pr1_type (GO d)) => Unit))
  1
  (fun (s d : sig_type Pobj)
     (m : sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit)) =>
   (pr1_type m; tt))
  (proj1; proj2) (proj0; proj3) =
idmap
    apply path_forall; intros [? []].
A: PreCategory
Pobj: A -> Type
H: Funext
proj1: A
proj2: Pobj proj1
proj0: A
proj3: Pobj proj0
proj4: morphism A (pr1_type (proj1; proj2)) (pr1_type (proj0; proj3))
transport
  (fun GO : sig_type Pobj -> sig_type Pobj =>
   forall s d : sig_type Pobj,
   sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit) ->
   sig_type (fun _ : morphism A (pr1_type (GO s)) (pr1_type (GO d)) => Unit))
  1
  (fun (s d : sig_type Pobj)
     (m : sig_type (fun _ : morphism A (pr1_type s) (pr1_type d) => Unit)) =>
   (pr1_type m; tt))
  (proj1; proj2) (proj0; proj3) (proj4; tt) =
(proj4; tt)
    reflexivity.
  Qed.

  Definition sig_obj_compat : pr1_obj o sig_functor_obj = pr1'
    := idpath.
End sig_obj.

Arguments pr1_obj {A Pobj}.

Module Export CategorySigmaOnObjectsNotations.
  Notation "{ x : A | P }" := (sig_obj A (fun x => P)) : category_scope.
End CategorySigmaOnObjectsNotations.