prettify equivalences by abusing gluedvl

intro.tt

@@ -399,7 +399,7 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -
 --       A i0 --------- A i1
 --                A
 --
--- Where the the two "e" sides are equivalences, and the bottom side is
+-- Where the the two "e" sides are equivalences, and the Bottom side is
 -- the line i : I |- A.
 --
 -- Thus, by choosing a base type, a set of partial types and partial
@@ -433,7 +433,7 @@ univalence {A} {B} equiv i =
 -- (x : A) is not just to apply f x to get a B (the left side), it also
 -- needs to:
 --
---   * For the bottom side, compose along (\i -> B) (the bottom side)
+--   * For the Bottom side, compose along (\i -> B) (the Bottom side)
 --   * For the right side, apply the inverse of the identity, which
 --     is just identity, to get *some* b : B
 -- 
@@ -443,29 +443,29 @@ univalence {A} {B} equiv i =
 --
 -- Thus the proof: a simple cubical argument suffices, since
 -- for any composition, its filler connects either endpoints. So
--- we need to come up with a filler for the bottom and right faces.
+-- we need to come up with a filler for the Bottom and right faces.
 
 univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1
 univalenceBeta {A} {B} f i a =
   let
-    -- The bottom left corner
+    -- The Bottom left corner
     botLeft : B
     botLeft = transp (\i -> B) (f.1 a)
 
-    -- The "bottom face" filler connects the bottom-left corner, f.1 a,
-    -- and the bottom-right corner, which is the transport of f.1 a
+    -- The "Bottom face" filler connects the Bottom-left corner, f.1 a,
+    -- and the Bottom-right corner, which is the transport of f.1 a
     -- along \i -> B.
     botFace : Path (f.1 a) botLeft
     botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i
 
-    -- The "right face" filler connects the bottom-right corner and the
+    -- The "right face" filler connects the Bottom-right corner and the
     -- upper-right corner, which is again a simple transport along
     -- \i -> B.
     rightFace : Path (transp (\i -> B) botLeft) botLeft
     rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)
 
-    -- The goal is a path between the bottom-left and top-right corners,
-    -- which we can get by composing (in the path sense) the bottom and
+    -- The goal is a path between the Bottom-left and top-right corners,
+    -- which we can get by composing (in the path sense) the Bottom and
     -- right faces.
     goal : Path (transp (\i -> B) botLeft) (f.1 a)
     goal = trans rightFace (\i -> botFace (inot i))
@@ -619,19 +619,19 @@ notp = univalence (IsoToEquiv (not, involToIso not notInvol))
 -- proving it's not an h-set is the furthest we can go.
 
 -- First we define what it means for something to be false. In type theory,
--- we take ¬P = P → ⊥, where the bottom type is the only type satisfying
+-- we take ¬P = P → ⊥, where the Bottom type is the only type satisfying
 -- the elimination principle
 --
---    elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b
+--    elimBottom : (P : Bottom -> Type) -> (b : Bottom) -> P b
 --
--- This follows from setting bottom := ∀ A, A.
+-- This follows from setting Bottom := ∀ A, A.
 
-data bottom : Type where {}
+data Bottom : Type where {}
 
-elimBottom : (P : bottom -> Pretype) -> (b : bottom) -> P b
+elimBottom : (P : Bottom -> Pretype) -> (b : Bottom) -> P b
 elimBottom P = \case {}
 
-absurd : {P : Pretype} -> bottom -> P
+absurd : {P : Pretype} -> Bottom -> P
 absurd = \case {}
 
 -- We prove that true != false by transporting along the path
@@ -646,8 +646,8 @@ absurd = \case {}
 --
 -- and evaluate the if at either end.
 
-trueNotFalse : Path true false -> bottom
-trueNotFalse p = transp (\i -> if (Bool -> Bool) bottom (p i)) id
+trueNotFalse : Path true false -> Bottom
+trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id
 
 -- To be an h-Set is to have no "higher path information". Alternatively,
 --
@@ -664,7 +664,7 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
 -- Since transp notp = not but transp refl = id, that's what we go with. The choice
 -- of false as the point x is just from the endpoints of trueNotFalse.
 
-universeNotSet : isHSet Type -> bottom
+universeNotSet : isHSet Type -> Bottom
 universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)
 
 -- Funext is an inverse of happly
@@ -715,12 +715,12 @@ Nat_elim P pz ps = \case
   zero -> pz
   succ x -> ps x (Nat_elim P pz ps x)
 
-zeroNotSucc : {x : Nat} -> Path zero (succ x) -> bottom
+zeroNotSucc : {x : Nat} -> Path zero (succ x) -> Bottom
 zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where
   fun : Nat -> Type
   fun = \case
     zero -> Nat
-    succ x -> bottom
+    succ x -> Bottom
 
 succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y
 succInj p i = pred (p i) where
@@ -1051,6 +1051,9 @@ sixteen = multInt four four
 isProp : Type -> Type
 isProp A = (x : A) (y : A) -> Path x y
 
+Prop : Type
+Prop = (A : Type) * isProp A
+
 data Sq (A : Type) : Type where
   inc : A -> Sq A
   sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ]
@@ -1065,6 +1068,9 @@ isProp_isSet h {a} {b} p q j i =
         ])
     (inS a)
 
+isProp_isProp : {A : Type} -> isProp (isProp A)
+isProp_isProp f g i a b = isProp_isSet f {a} {b} (f a b) (g a b) i
+
 Sq_rec : {A : Type} {B : Type}
       -> isProp B
       -> (f : A -> B)

src/Elab/Eval.hs

@@ -197,7 +197,7 @@ eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (
 eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq)
 
 evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value
-evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
+evalCase env rng sc [] = VCase (getEnv env) (fun rng) sc []
 
 evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
 
@@ -639,8 +639,7 @@ applProj fun PProj1           = vProj1 fun
 applProj fun PProj2           = vProj2 fun
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
-vApp p (VLam p' k) arg
-  | p == p' = clCont k arg
+vApp _ (VLam _ k) arg = clCont k arg
 vApp p (VNe h sp) arg  = VNe h (sp Seq.:|> PApp p arg)
 vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
 vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)

src/Elab/WiredIn.hs

@@ -456,7 +456,8 @@ isEquiv :: NFSort -> NFSort -> Value -> Value
 isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
 
 equiv :: NFSort -> NFSort -> Value
-equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
+equiv a b = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f" (a ~> b) \f -> isEquiv a b f where
+  sp = Seq.fromList [ PApp P.Ex a, PApp P.Ex b ]
 
 pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
 pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where