Opaque functor_comp.
Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
{ reification_r_obj : K -> K -> C
; reification_rstar_obj : enr_v K -> enr_v C
; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
Opaque functor_comp.
Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
{ reification_r_obj : K -> K -> C
; reification_rstar_obj : enr_v K -> enr_v C
; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj