From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 30 Dec 2015 18:58:37 +0000 (+0100)
Subject: add standard formulation of univalence
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=3d43f42aec55f0b8b423d12f28abde0bd9b4dae4;p=cubicaltt.git

add standard formulation of univalence
---

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) (<i>corrUniv A A@-i) (idEquiv A)
 
 -- obtained by normal form