Definition indexed_cat_laws {C : category} (F : indexed_cat_data C) : UU := (∏ (x y : C) (f : x --> y) (xx : F x), identity ((F $ f) xx) = # (F $ f) (indexed_cat_id F x xx) · indexed_cat_comp F (identity x) f xx · idtoiso (maponpaths (λ g, (F $ g) xx) (id_left f))) × (∏ (x y : C) (f : x --> y) (xx : F x), identity ((F $ f) xx) = indexed_cat_id F y ((F $ f) xx) · indexed_cat_comp F f (identity y) xx · idtoiso (maponpaths (λ g, (F $ g) xx) (id_right f))) × (∏ (w x y z : C) (f : w --> x) (g : x --> y) (h : y --> z) (ww : F w), indexed_cat_comp F g h ((F $ f) ww) · indexed_cat_comp F f (g · h) ww · idtoiso (maponpaths (λ k, (F $ k) ww) (assoc f g h)) = # (F $ h) (indexed_cat_comp F f g ww) · indexed_cat_comp F (f · g) h ww).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations.