From 3d43f42aec55f0b8b423d12f28abde0bd9b4dae4 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 30 Dec 2015 19:58:37 +0100 Subject: [PATCH] add standard formulation of univalence --- examples/testContr.ctt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/testContr.ctt b/examples/testContr.ctt index 61d031b..95b5022 100644 --- a/examples/testContr.ctt +++ b/examples/testContr.ctt @@ -143,6 +143,8 @@ univalence (A X:U) : isEquiv (Id U X A) (equiv X A) (lem2 A X) = thmUniv lem2 A corrUniv (A X:U) : Id U (Id U X A) (equiv X A) = equivId (Id U X A) (equiv X A) (lem2 A X) (univalence A X) +corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A) + testUniv1 (A:U) : Id U A A = trans (equiv A A) (Id U A A) (corrUniv A A@-i) (idEquiv A) -- obtained by normal form -- 2.34.1