From 53d66c91fcfbaf28ee75ac35be6f098d1b79dc59 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Sat, 22 Nov 2014 23:41:47 -0500 Subject: [PATCH] chore(library/hott) made ua_implies_funext a class instance --- library/hott/funext_from_ua.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/hott/funext_from_ua.lean b/library/hott/funext_from_ua.lean index 8ce8793f98..94cca2b3de 100644 --- a/library/hott/funext_from_ua.lean +++ b/library/hott/funext_from_ua.lean @@ -126,5 +126,5 @@ theorem ua_implies_weak_funext [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : wea ) -- In the following we will proof function extensionality using the univalence axiom -definition ua_implies_funext {ua ua2 : ua_type} : funext := +definition ua_implies_funext [instance] [ua ua2 : ua_type] : funext := weak_funext_implies_funext (@ua_implies_weak_funext ua ua2)