Library HoTT.WildCat.Sigma

(* -*- mode: coq; mode: visual-line -*-  *)

Require Import Basics.Overture Basics.Tactics.
Require Import WildCat.Core.

Section Sigma.

  Context (A : Type) (B : A → Type)
    `{∀ a, IsGraph (B a)}
    `{∀ a, Is01Cat (B a)}
    `{∀ a, Is0Gpd (B a)}.

Global Instance isgraph_sigma : IsGraph (sig B).
Proof.
  srapply Build_IsGraph.
  intros [x u] [y v].
  exact {p : x = y & p # u $-> v}.
Defined.

Global Instance is01cat_sigma : Is01Cat (sig B).
Proof.
  srapply Build_Is01Cat.
  + intros [x u].
    ∃ idpath. exact (Id u).
  + intros [x u] [y v] [z w] [q g] [p f].
    ∃ (p @ q).
    destruct p, q; cbn in ×.
    exact (g $o f).
Defined.

Global Instance is0gpd_sigma : Is0Gpd (sig B).
Proof.
  constructor.
  intros [x u] [y v] [p f].
  ∃ (p^).
  destruct p; cbn in ×.
  exact (f^$).
Defined.

End Sigma.

Global Instance is0functor_sigma {A : Type} (B C : A → Type)
       `{∀ a, IsGraph (B a)} `{∀ a, IsGraph (C a)}
       `{∀ a, Is01Cat (B a)} `{∀ a, Is01Cat (C a)}
       (F : ∀ a, B a → C a) {ff : ∀ a, Is0Functor (F a)}
  : Is0Functor (fun (x:sig B) ⇒ (x.1 ; F x.1 x.2)).
Proof.
  constructor; intros [a1 b1] [a2 b2] [p f]; cbn.
  ∃ p.
  destruct p; cbn in ×.
  exact (fmap (F a1) f).
Defined.