From 67638e218f1c7f4c69d3df17628a246aa1e01e49 Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 18 Jun 2015 18:57:12 +0200 Subject: [PATCH] Restate univalence --- examples/univalence.ctt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 6512d28..1d4af7d 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -39,9 +39,9 @@ idToId (A B : U) (w : equiv A B) (transEquiv A B (transEquivToId A B w)) w (transIdFun A B w) -univAx (A B : U) : isEquiv (Id U A B) (equiv A B) (transEquiv A B) = - gradLemma (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B) - (idToId A B) (eqToEq A B) +univalence (A B : U) : equiv (Id U A B) (equiv A B) = + (transEquiv A B,gradLemma (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B)) -- Alternative definition: -- 2.34.1