From: Simon Huber <hubsim@gmail.com>
Date: Tue, 16 Jun 2015 20:11:52 +0000 (+0200)
Subject: Adds projections for equivs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f1a06ce0eeeea5e9cc1983c3b31a7cc962d8f245;p=cubicaltt.git

Adds projections for equivs
---

diff --git a/Eval.hs b/Eval.hs
index f16918b..501df76 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -10,6 +10,7 @@ import qualified Data.Map as Map
 import Connections
 import CTT
 
+
 look :: String -> Env -> Val
 look x (Upd y rho,v:vs,fs) | x == y = v
                            | otherwise = look x (rho,vs,fs)
@@ -434,6 +435,12 @@ equivDom = fstVal
 equivFun :: Val -> Val
 equivFun = fstVal . sndVal
 
+equivCenter :: Val -> Val
+equivCenter = fstVal . sndVal . sndVal
+
+equivIsCenter :: Val -> Val
+equivIsCenter = sndVal . sndVal . sndVal
+
 -- TODO: adapt to equivs
 -- Every path in the universe induces an hiso
 -- eqToIso :: Val -> Val
@@ -610,9 +617,9 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us'
 -- s.t. f us = border v. Outputs (u,p) s.t. border u = us and an
 -- L-path p between v and f u.
 gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
-gradLemma b equiv@(VPair a (VPair f (VPair s t))) us v =
-  (u,VPath j $ tau `sym` j)
-  where i:j:_ = freshs (b,equiv,us,v)
+gradLemma b e us v = (u,VPath j $ tau `sym` j)
+  where i:j:_ = freshs (b,e,us,v)
+        (a,f,s,t) = (equivDom e,equivFun e,equivCenter e,equivIsCenter e)
         g y = fstVal (app s y) -- g : b -> a
         eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b
         us' = mapWithKey