X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReification.v;fp=src%2FReification.v;h=2f2ba67f62f0e7a5be45f6c4ae7993cd00c2e743;hp=a56ded8e745fd5636585deb80d3302fca990c83d;hb=e536cc4194f350ed6de5d465bcf53fda650b3d12;hpb=3351499d7cb3d32c8df441426309ec6a1ef2a035

diff --git a/src/Reification.v b/src/Reification.v
index a56ded8..2f2ba67 100644
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -31,7 +31,7 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI: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
 ; reification_rstar     :             MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
-; reification_commutes  : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
+; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
 }.
 Transparent RepresentableFunctor.
 Transparent functor_comp.