Library HoTT.WildCat.Forall

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

Instance isgraph_forall (A : Type) (B : A → Type)
  `{∀ a, IsGraph (B a)}
  : IsGraph (∀ a, B a).
Proof.
  srapply Build_IsGraph.
  intros x y; exact (∀ (a : A), x a $-> y a).
Defined.

Instance is01cat_forall (A : Type) (B : A → Type)
  `{∀ a, IsGraph (B a)} `{∀ a, Is01Cat (B a)}
  : Is01Cat (∀ a, B a).
Proof.
  srapply Build_Is01Cat.
  + intros x a; exact (Id (x a)).
  + intros x y z f g a; exact (f a $o g a).
Defined.

Instance is0gpd_forall (A : Type) (B : A → Type)
  (* Apparently when there's a ∀ there, Coq can't automatically add the Is01Cat instance from the Is0Gpd instance. *)
  `{∀ a, IsGraph (B a)} `{∀ a, Is01Cat (B a)} `{∀ a, Is0Gpd (B a)}
  : Is0Gpd (∀ a, B a).
Proof.
  constructor.
  intros f g p a; exact ((p a)^$).
Defined.

Instance is2graph_forall (A : Type) (B : A → Type)
  `{∀ a, IsGraph (B a)} `{∀ a, Is2Graph (B a)}
  : Is2Graph (∀ a, B a).
Proof.
  intros x y; srapply Build_IsGraph.
  intros f g; exact (∀ a, f a $-> g a).
Defined.

Instance is1cat_forall (A : Type) (B : A → Type)
  `{∀ a, IsGraph (B a)} `{∀ a, Is01Cat (B a)}
  `{∀ a, Is2Graph (B a)} `{∀ a, Is1Cat (B a)}
  : Is1Cat (∀ a, B a).
Proof.
  srapply Build_Is1Cat.
  + intros x y z h; srapply Build_Is0Functor.
    intros f g p a.
    exact (h a $@L p a).
  + intros x y z h; srapply Build_Is0Functor.
    intros f g p a.
    exact (p a $@R h a).
  + intros w x y z f g h a; apply cat_assoc.
  + intros w x y z f g h a; apply cat_assoc_opp.
  + intros x y f a; apply cat_idl.
  + intros x y f a; apply cat_idr.
Defined.