From accbe8633bc133e5d444c70747b03a3229852739 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Tue, 6 Apr 2021 21:31:55 -0300 Subject: [PATCH] prettify equivalences by abusing gluedvl --- intro.tt | 46 +++++++++++++++++++++++++-------------------- src/Elab/Eval.hs | 5 ++--- src/Elab/WiredIn.hs | 3 ++- 3 files changed, 30 insertions(+), 24 deletions(-) diff --git a/intro.tt b/intro.tt index 2b55196..438f6b2 100644 --- a/intro.tt +++ b/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) diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index dced8ed..b9ea7a1 100644 --- a/src/Elab/Eval.hs +++ 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) diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index 60c06ed..deaf6ac 100644 --- a/src/Elab/WiredIn.hs +++ b/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