Merge pull request #241 from rmatthes/restorecompafterunimathPR1768

upstream change to is_univalent_full_sub_category
UniMath · Aug 29, 2023 · 3dfd601 · 3dfd601
2 parents 7205f8b + 30227b8
commit 3dfd601
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/TypeTheory/RelUniv/RelUniv_Cat_Simple.v b/TypeTheory/RelUniv/RelUniv_Cat_Simple.v
@@ -310,7 +310,7 @@ Section WeakRelUniv_is_univalent.
       : is_univalent weak_reluniv_cat.
     Proof.
       use (catiso_univalent _ _ weak_reluniv_cat_to_full_subcat).
-      apply (is_univalent_full_subcat
+      apply (is_univalent_full_sub_category
                (arrow_category D)
                is_weak_reluniv_ob
                (arrow_category_is_univalent D_univ)