|
|
|
@ -22,8 +22,6 @@ import qualified Presyntax.Presyntax as P |
|
|
|
import Syntax |
|
|
|
|
|
|
|
import System.IO.Unsafe |
|
|
|
import GHC.Stack |
|
|
|
import Syntax.Pretty |
|
|
|
|
|
|
|
wiType :: WiredIn -> NFType |
|
|
|
wiType WiType = VType |
|
|
|
@ -214,7 +212,7 @@ ielim _line _left _right fn i = |
|
|
|
VSystem (Map.toList -> []) -> VSystem (Map.fromList []) |
|
|
|
_ -> error $ "can't ielim " ++ show fn |
|
|
|
|
|
|
|
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value |
|
|
|
outS :: NFSort -> NFEndp -> Value -> Value -> Value |
|
|
|
outS _ (force -> VI1) u _ = u @@ VItIsOne |
|
|
|
|
|
|
|
outS _ _phi _ (VInc _ _ x) = x |
|
|
|
@ -245,8 +243,8 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
(VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg))) |
|
|
|
VSigma{} -> |
|
|
|
let |
|
|
|
dom i = let VSigma d _ = a @@ i in d |
|
|
|
rng i = let VSigma _ (Closure _ r) = a @@ i in r |
|
|
|
dom i = let VSigma d _ = force (a @@ i) in d |
|
|
|
rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r |
|
|
|
|
|
|
|
w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i |
|
|
|
c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) |
|
|
|
@ -256,9 +254,9 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
|
|
|
|
VPath{} -> |
|
|
|
let |
|
|
|
a' i = let VPath thea _ _ = a @@ i in thea |
|
|
|
u' i = let VPath _ theu _ = a @@ i in theu |
|
|
|
v' i = let VPath _ _ thev = a @@ i in thev |
|
|
|
a' i = let VPath thea _ _ = force (a @@ i) in thea |
|
|
|
u' i = let VPath _ theu _ = force (a @@ i) in theu |
|
|
|
v' i = let VPath _ _ thev = force (a @@ i) in thev |
|
|
|
in |
|
|
|
VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j -> |
|
|
|
comp (fun a') |
|
|
|
@ -306,7 +304,9 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
a1' |
|
|
|
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1 |
|
|
|
in b1 |
|
|
|
|
|
|
|
|
|
|
|
VType -> VGlueTy a0 phi (system \_ _ -> u @@ VI1 @@ VItIsOne) (system \_ _ -> makeEquiv (\j -> (u @@ inot j))) |
|
|
|
|
|
|
|
-- fibrancy structure of the booleans is trivial |
|
|
|
VBool{} -> a0 |
|
|
|
|
|
|
|
@ -394,14 +394,22 @@ contr a aC phi u = |
|
|
|
(system \i is1 -> ielim (line (const a)) a (vProj1 (u is1)) (vProj2 (u is1)) i) |
|
|
|
(vProj1 aC) |
|
|
|
|
|
|
|
makeEquiv :: (NFEndp -> Value) -> Value |
|
|
|
makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem mempty) (VPair idfun idisequiv) where |
|
|
|
a = line VI0 |
|
|
|
idfun = fun id |
|
|
|
-- idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j))) |
|
|
|
u_ty = exists' "y" a \x -> VPath (fun (const a)) x x |
|
|
|
idisequiv = fun \y -> VPair (id_fiber y) $ fun \u -> |
|
|
|
VLine u_ty (id_fiber y) u $ fun \i -> VPair (ielim (fun (const a)) y y (vProj2 u) i) $ |
|
|
|
VLine (fun (const a)) y (vProj1 u) $ fun \j -> |
|
|
|
ielim (fun (const a)) y y (vProj2 u) (iand i j) |
|
|
|
|
|
|
|
id_fiber y = VPair y (VLine a y y (fun (const y))) |
|
|
|
|
|
|
|
elimBool :: NFSort -> Value -> Value -> Value -> Value |
|
|
|
elimBool prop x y bool = |
|
|
|
case force bool of |
|
|
|
VTt -> x |
|
|
|
VFf -> y |
|
|
|
VNe _ (_ Seq.:|> PIElim _ a b c) -> |
|
|
|
case c of |
|
|
|
VI0 -> elimBool prop x y a |
|
|
|
VI1 -> elimBool prop x y b |
|
|
|
_ -> VIf prop x y bool |
|
|
|
_ -> VIf prop x y bool |
