include proof of strong funext

3 years ago · 0a68d57f80
--- a/intro.tt
+++ b/intro.tt
@ -138,10 +138,6 @@ funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
 -> Path f g
 funext h i x = h x i

 happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
 -> (p : Path f g) -> (x : A) -> Path (f x) (g x)
 happly p x i = p i x

 -- The proposition associated with an element of the interval
 -------------------------------------------------------------

@ -520,42 +516,42 @@ IsoToEquiv {A} {B} iso =
 lemIso y x0 x1 p0 p1 =
 let
 rem0 : Path x0 (g y)
 rem0 i = hcomp {A} (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))
 rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))

 rem1 : Path x1 (g y)
 rem1 i = hcomp {A} (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))
 rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))

 p : Path x0 x1
 p i = hcomp {A} (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
 p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))

 fill0 : I -> I -> A
 fill0 i j = hcomp {A} (\k [ (i = i0) -> t x0 (iand j k)
 , (i = i1) -> g y
 , (j = i0) -> g (p0 i) 
 ])
 fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k)
  , (i = i1) -> g y
  , (j = i0) -> g (p0 i) 
  ])
 (inS (g (p0 i)))

 fill1 : I -> I -> A
 fill1 i j = hcomp {A} (\k [ (i = i0) -> t x1 (iand j k)
 fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k)
 , (i = i1) -> g y
 , (j = i0) -> g (p1 i) ])
 (inS (g (p1 i)))

 fill2 : I -> I -> A
 fill2 i j = hcomp {A} (\k [ (i = i0) -> rem0 (ior j (inot k))
 fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k))
 , (i = i1) -> rem1 (ior j (inot k))
 , (j = i1) -> g y ])
 (inS (g y))

 sq : I -> I -> A
 sq i j = hcomp {A} (\k [ (i = i0) -> fill0 j (inot k)
 sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k)
 , (i = i1) -> fill1 j (inot k)
 , (j = i1) -> g y
 , (j = i0) -> t (p i) (inot k) ])
 (inS (fill2 i j))

 sq1 : I -> I -> B
 sq1 i j = hcomp {B} (\k [ (i = i0) -> s (p0 j) k
 sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k
 , (i = i1) -> s (p1 j) k
 , (j = i0) -> s (f (p i)) k
 , (j = i1) -> s y k
@ -662,4 +658,33 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
 -- of false as the point x is just from the endpoints of trueNotFalse.

 universeNotSet : isHSet Type -> bottom
 universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)
 universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)

 -- Funext is an inverse of happly
 ---------------------------------
 --
 -- Above we proved function extensionality, namely, that functions
 -- pointwise equal everywhere are themselves equal.
 -- However, this formulation of the axiom is known as "weak" function
 -- extensionality. The strong version is as follows:

 Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type
 Hom {A} f g = (x : A) -> Path (f x) (g x)

 happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
 -> (p : Path f g) -> Hom f g
 happly p x i = p i x

 -- Strong function extensionality: happly is an equivalence.

 happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
 -> isIso {Path f g} {Hom f g} happly
 happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl)

 pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
 -> Path (Path f g) (Hom f g)
 pathIsHom {A} {B} {f} {g} =
 let
 theIso : Iso (Path f g) (Hom f g)
 theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
 in univalence (IsoToEquiv theIso)
--- a/src/Elab.hs
+++ b/src/Elab.hs
@ -10,6 +10,8 @@ import Control.Exception
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 import Data.Traversable
 import Data.Text (Text)
 import Data.Map (Map)
 import Data.Typeable
 import Data.Foldable

@ -24,8 +26,6 @@ import Prettyprinter

 import Syntax.Pretty
 import Syntax
 import Data.Map (Map)
 import Data.Text (Text)

 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
--- a/src/Elab/Monad.hs
+++ b/src/Elab/Monad.hs
@ -11,15 +11,15 @@ import Data.Text.Prettyprint.Doc.Render.Terminal (AnsiStyle)
 import qualified Data.Map.Strict as Map
 import Data.Text.Prettyprint.Doc
 import Data.Map.Strict (Map)
 import Data.Sequence (Seq)
 import Data.Text (Text)
 import Data.Set (Set)
 import Data.Typeable
 import Data.IORef

 import qualified Presyntax.Presyntax as P

 import Syntax
 import Data.IORef
 import Data.Sequence (Seq)

 data ElabEnv =
 ElabEnv { getEnv :: Map Name (NFType, Value)
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@ -209,7 +209,7 @@ ielim _line _left _right fn i =
 VI0 -> _left
 _ -> case x of
 VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i)
 VSystem (Map.toList -> []) -> VSystem (Map.fromList [])
 VSystem map -> VSystem (fmap (flip (ielim _line _left _right) i) map)
 _ -> error $ "can't ielim " ++ show fn

 outS :: NFSort -> NFEndp -> Value -> Value -> Value
@ -225,7 +225,7 @@ outS _ _ _ v = error $ "can't outS " ++ show v
 comp :: 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 "neutral composition") 0) of
 case force $ a @@ VVar (Bound (T.pack "i") 0) of
 VPi{} ->
 let
 plic i = let VPi p _ _ = force (a @@ i) in p
@ -235,7 +235,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
 y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
 ybar i y = y' (inot i) y
 in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
 comp (fun \i -> rng i (ybar i arg))
 comp (line \i -> rng i (ybar i arg))
 phi
 (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
 (VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
@ -257,7 +257,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
 v' i = let VPath _ _ thev = force (a @@ i) in thev
 in
 VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j ->
 comp (fun a')
 comp (fun \x -> a' x @@ x)
 (phi `ior` j `ior` inot j)
 (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
 , (j, v' i)
@ -321,7 +321,7 @@ system k = fun \i -> fun \isone -> k i isone

 fill :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
 fill a phi u a0 j =
 comp (fun \i -> a @@ (i `iand` j))
 comp (line \i -> a @@ (i `iand` j))
 (phi `ior` inot j)
 (fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
 , (inot j, a0)]))
@ -372,8 +372,8 @@ equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
 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
 pathT = VPath (fun (const (tyA VI1))) c1 c2
 c1 = comp (fun tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
 c2 = f VI1 @@ comp (fun tyT) phi (system \i u -> t i @@ u) t0
 c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
 c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0

 a0 = f VI0 @@ t0
 v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
@ -411,4 +411,4 @@ elimBool prop x y bool =
 case force bool of
 VTt -> x
 VFf -> y
 _ -> VIf prop x y bool
 _ -> VIf prop x y bool
--- a/src/Main.hs
+++ b/src/Main.hs
@ -13,9 +13,15 @@ import qualified Data.ByteString.Lazy as Bsl
 import qualified Data.Text.Encoding as T
 import qualified Data.Map.Strict as Map
 import qualified Data.Text.IO as T
 import qualified Data.Set as Set
 import qualified Data.Text as T
 import Data.Sequence (Seq)
 import Data.Text ( Text )
 import Data.Foldable
 import Data.Maybe
 import Data.IORef

 import Debug.Trace

 import Elab.Monad hiding (switch)
 import Elab.WiredIn
@ -26,6 +32,7 @@ import Options.Applicative

 import Presyntax.Presyntax (Posn(Posn))
 import Presyntax.Parser
 import Presyntax.Tokens
 import Presyntax.Lexer

 import Prettyprinter
@ -35,12 +42,6 @@ import Syntax

 import System.Console.Haskeline
 import System.Exit
 import qualified Data.Set as Set
 import Data.Maybe
 import Presyntax.Tokens
 import Debug.Trace
 import Data.IORef
 import Data.Sequence (Seq)

 main :: IO ()
 main = do
@ -131,7 +132,7 @@ displayAndDie lines e = do
 exitFailure

 displayExceptions :: Text -> [Handler ()]
 displayExceptions lines = 
 displayExceptions lines =
 [ Handler \(WhileChecking a b e) -> do
 T.putStrLn $ squiggleUnder a b lines
 displayExceptions' lines e
@ -177,7 +178,7 @@ reportUnsolved metas = do
 "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:"
 for_ p \p ->
 T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
 


 displayExceptions' :: Exception e => Text -> e -> IO ()
 displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure ()
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@ -6,9 +6,11 @@ import Control.Arrow (Arrow(first))

 import qualified Data.Map.Strict as Map
 import qualified Data.Text.Lazy as L
 import qualified Data.Set as Set
 import qualified Data.Text as T
 import Data.Map.Strict (Map)
 import Data.Text (Text)
 import Data.Set (Set)
 import Data.Generics

 import Presyntax.Presyntax (Plicity(..))
@ -43,8 +45,14 @@ prettyTm = prettyTm . everywhere (mkT beautify) where

 (al, bod) = unwindLam l

 prettyArgList (Ex, v) = pretty v
 prettyArgList (Im, v) = braces (pretty v)
 used = freeVars bod

 prettyArgList (Ex, v)
 | v `Set.member` used = pretty v
 | otherwise = pretty "_"
 prettyArgList (Im, v)
 | v `Set.member` used = braces $ pretty v
 | otherwise = pretty "_"

 prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
 prettyTm Type{} = keyword $ pretty "Type"
@ -140,3 +148,47 @@ showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm
 showFace :: Map Head Bool -> Doc AnsiStyle
 showFace = hsep . map go . Map.toList where
 go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")

 freeVars :: Term -> Set Name
 freeVars (Ref v) = Set.singleton v
 freeVars (App _ f x) = Set.union (freeVars f) (freeVars x)
 freeVars (Pi _ n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
 freeVars (Lam _ n x) = n `Set.delete` freeVars x
 freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where
 bound = Set.fromList (map (\(x, _, _) -> x) ns)
 freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns
 freeVars Meta{} = mempty
 freeVars Type{} = mempty
 freeVars Typeω{} = mempty
 freeVars I{} = mempty
 freeVars I0{} = mempty
 freeVars I1{} = mempty
 freeVars (Sigma n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
 freeVars (Pair x y) = Set.unions $ map freeVars [x, y]
 freeVars (Proj1 x) = Set.unions $ map freeVars [x]
 freeVars (Proj2 x) = Set.unions $ map freeVars [x]
 freeVars (IAnd x y) = Set.unions $ map freeVars [x, y]
 freeVars (IOr x y) = Set.unions $ map freeVars [x, y]
 freeVars (INot x) = Set.unions $ map freeVars [x]
 freeVars (PathP x y z) = Set.unions $ map freeVars [x, y, z]
 freeVars (IElim x y z a b) = Set.unions $ map freeVars [x, y, z, a, b]
 freeVars (PathIntro x y z a) = Set.unions $ map freeVars [x, y, z, a]
 freeVars (IsOne a) = Set.unions $ map freeVars [a]
 freeVars (IsOne1 a) = Set.unions $ map freeVars [a]
 freeVars (IsOne2 a) = Set.unions $ map freeVars [a]
 freeVars ItIsOne{} = mempty
 freeVars (Partial x y) = Set.unions $ map freeVars [x, y]
 freeVars (PartialP x y) = Set.unions $ map freeVars [x, y]
 freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty (Map.toList fs)

 freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z]
 freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z]
 freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a]
 freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a]
 freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a]
 freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c]
 freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c]
 freeVars Bool{} = mempty
 freeVars Tt{} = mempty
 freeVars Ff{} = mempty
 freeVars (If x y z a) = Set.unions $ map freeVars [x, y, z, a]