Skip to content

Commit d25bb14

Browse files
Merge pull request #194 from rmatthes/repairafterupdatetoUniMathforz_iso
repairs compilation with UniMath PR #1364 (as of today)
2 parents 7b8b39c + 3dc5620 commit d25bb14

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

TypeTheory/ALV1/CwF_SplitTypeCat_Equivalence.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ Definition canonical_TM_to_given_iso
142142
: @iso (preShv C) (tm_from_qq Z) (TM (pr1 Y)).
143143
Proof.
144144
exists canonical_TM_to_given.
145-
apply functor_iso_if_pointwise_iso.
145+
apply functor_iso_if_pointwise_iso. intro c.
146146
apply canonical_TM_to_given_pointwise_iso.
147147
Defined.
148148

0 commit comments

Comments
 (0)