Fix composition for pairs

3 years ago · 6d82ecd85f
--- a/intro.tt
+++ b/intro.tt
@ -260,7 +260,7 @@ trans {A} {x} p q i =
 -- single point, which corresponds to transport.

 transp : (A : I -> Type) (x : A i0) -> A i1
 transp A x = comp A (\i [ ]) (inS x)
 transp A x = comp A {i0} (\i [ ]) (inS x)

 -- Since we have the iand operator, we can also derive the *filler* of a cube,
 -- which connects the given face and the output of composition.
@ -319,7 +319,7 @@ fiber f y = (x : A) * Path (f x) y
 -- point in the input which f maps to y.

 isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type
 isEquiv {A} {B} f = (y : B) -> isContr (fiber f y)
 isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)

 -- By extracting this point, which must exist because the fiber is contractible,
 -- we can get an inverse of f:
@ -337,7 +337,7 @@ section f eqv i y = (eqv y) .1 .2 i
 -- equivalence to get a capital-E Equivalence.

 Equiv : (A : Type) (B : Type) -> Type
 Equiv A B = (f : A -> B) * isEquiv f
 Equiv A B = (f : A -> B) * isEquiv {A} {B} f

 -- The identity function is an equivalence between any type A and
 -- itself.
@ -419,6 +419,7 @@ univalence {A} {B} equiv i =
 Glue B (\[ (i = i0) -> (A, equiv),
 (i = i1) -> (B, the B, idEquiv {B}) ]) 


 -- The fact that this diagram has 2 filled-in B sides explains the
 -- complication in the proof below.
 --
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@ -206,6 +206,7 @@ vApp p (VLam p' k) arg
 | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
 vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg)
 vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
 vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
 vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x))

 (@@) :: HasCallStack => Value -> Value -> Value
@ -216,12 +217,14 @@ vProj1 :: HasCallStack => Value -> Value
 vProj1 (VPair a _) = a
 vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
 vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
 vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c)
 vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))

 vProj2 :: HasCallStack => Value -> Value
 vProj2 (VPair _ b) = b
 vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2)
 vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
 vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c)
 vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))

 data NotEqual = NotEqual Value Value
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@ -22,6 +22,8 @@ import qualified Presyntax.Presyntax as P
 import Syntax

 import System.IO.Unsafe
 import Syntax.Pretty (prettyTm)
 import GHC.Stack (HasCallStack)

 wiType :: WiredIn -> NFType
 wiType WiType = VType
@ -201,16 +203,17 @@ inot = \case
 x -> VINot x

 ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value
 ielim _line _left _right fn i =
 ielim line left right fn i =
 case force fn of
 VLine _ _ _ fun -> fun @@ i
 x -> case i of
 VI1 -> _right
 VI0 -> _left
 VI1 -> right
 VI0 -> left
 _ -> case x of
 VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i)
 VSystem map -> VSystem (fmap (flip (ielim _line _left _right) i) map)
 _ -> error $ "can't ielim " ++ show fn
 VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
 VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
 VInc (VPath _ _ _) _ u -> ielim line left right u i
 _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))

 outS :: NFSort -> NFEndp -> Value -> Value -> Value
 outS _ (force -> VI1) u _ = u @@ VItIsOne
@ -219,10 +222,10 @@ outS _ _phi _ (VInc _ _ x) = x
 outS _ VI0 _ x = x

 outS a phi u (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
 outS _ _ _ v = error $ "can't outS " ++ show v
 outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))

 -- Composition
 comp :: NFLine -> NFEndp -> Value -> Value -> Value
 comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
 comp _ VI1 u _ = u @@ VI1 @@ VItIsOne
 comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
 case force $ a @@ VVar (Bound (T.pack "i") 0) of
@ -246,8 +249,8 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =

 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))
 c2 = comp (fun (($ w VI1) . rng)) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (rng VI0 (dom VI0)) phi (vProj2 a0))
 in
 c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
 in 
 VPair c1 c2

 VPath{} ->
@ -309,7 +312,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
 -- fibrancy structure of the booleans is trivial
 VBool{} -> a0

 _ -> VComp a phi u a0
 _ -> VComp a phi u (VInc (a @@ VI0) phi a0)

 compOutS :: NFSort -> NFEndp -> Value -> Value -> Value
 compOutS _ _hi _0 vl@VComp{} = vl
@ -380,17 +383,17 @@ pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), p

 path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0

 opEquiv :: Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
 opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
 opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
 fn = vProj1 f
 ty = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x)
 v = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))

 contr :: Value -> Value -> NFEndp -> (Value -> Value) -> Value
 contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value
 contr a aC phi u =
 comp (line (const a))
 phi
 (system \i is1 -> ielim (line (const a)) a (vProj1 (u is1)) (vProj2 (u is1)) i)
 (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
 (vProj1 aC)

 makeEquiv :: (NFEndp -> Value) -> Value
--- a/src/Elab/WiredIn.hs-boot
+++ b/src/Elab/WiredIn.hs-boot
@ -1,6 +1,7 @@
 module Elab.WiredIn where

 import Syntax
 import GHC.Stack

 wiType :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
@ -10,7 +11,7 @@ inot :: NFEndp -> NFEndp
 ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value

 outS :: NFSort -> NFEndp -> Value -> Value -> Value
 comp :: NFLine -> NFEndp -> Value -> Value -> Value
 comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value

 glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
 glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
--- a/src/Main.hs
+++ b/src/Main.hs
@ -157,8 +157,8 @@ displayExceptions lines =
 , Handler \(NotEqual ta tb) -> do
 putStrLn . unlines $
 [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
 , " * \x1b[1mActual\x1b[0m: " ++ showValue (zonk ta)
 , " * \x1b[1mExpected\x1b[0m: " ++ showValue (zonk tb)
 , " * \x1b[1mActual\x1b[0m: " ++ show (zonk ta)
 , " * \x1b[1mExpected\x1b[0m: " ++ show (zonk tb)
 ]
 , Handler \(NoSuchPrimitive x) -> do
 putStrLn $ "Unknown primitive: " ++ T.unpack x
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@ -118,7 +118,7 @@ instance Eq MV where
 instance Ord MV where
 (<=) = (<=) `on` mvName
 instance Show MV where
 show = ('?':) . T.unpack . mvName
 show x = show (mvName x, mvSpan x)

 instance Data MV where
 toConstr _ = error "toConstr"