Browse Source

Use GluedVl to improve printing of isEquiv

Amélia Liao 3 years ago
committed by Abigail Magalhães
parent
commit
0e27107e89
3 changed files with 30 additions and 24 deletions
  1. +26
    -20
      intro.tt
  2. +2
    -3
      src/Elab/Eval.hs
  3. +2
    -1
      src/Elab/WiredIn.hs

+ 26
- 20
intro.tt View File

@ -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)


+ 2
- 3
src/Elab/Eval.hs View File

@ -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)


+ 2
- 1
src/Elab/WiredIn.hs View File

@ -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


Loading…
Cancel
Save