at least it works

library/data/equiv.anders

@@ -63,8 +63,14 @@ section
   hcomp (Glue A φ [(φ = 1) → e 1=1]) ψ (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀)
 end
 
+def transportε (A B : U) (p : PathP (<_> U) A B) : A → B :=
+λ (x : A), transp p 0 (transp (<_> A) 0 x)
+
+def transportεIsEquiv (A B : U) (p : PathP (<_> U) A B) : isEquiv A B (transportε A B p) :=
+(transp (<i> equiv A (p @ i)) 0 (idEquiv A)).2
+
 def idtoeqv (A B : U) (p : PathP (<_> U) A B) : equiv A B :=
-transp (<i> equiv A (p @ i)) 0 (idEquiv A)
+(transportε A B p, transportεIsEquiv A B p)
 
 def ua (A B : U) (e : equiv A B) : PathP (<_> U) A B :=
 <i> Glue B (∂ i) [(i = 0) → (A, e), (i = 1) → (B, idEquiv B)]
@@ -84,9 +90,10 @@ propPi B (λ (y : B), isContr (fiber A B f y))
 def idtoeqv→trans (A B : U) (p : PathP (<_> U) A B) : Path (A → B) (idtoeqv A B p).1 (trans A B p) :=
 <i> λ (a : A), transp p 0 (transp (<_> A) i a)
 
-def ideqv-compute (A B : U) (e : equiv A B) : Path (A → B) (idtoeqv A B (ua A B e)).1 e.1 :=
+def ideqv-compute (A B : U) (e : equiv A B) : Path (A → B) (transportε A B (ua A B e)) e.1 :=
 comp-Path (A → B) (idtoeqv A B (ua A B e)).1 (trans A B (ua A B e)) e.1 (idtoeqv→trans A B (ua A B e)) (ua-β A B e)
 
--- should “isEquiv” be opaque?
---def idtoeqv-ua (A B : U) (e : equiv A B) : Path (equiv A B) (idtoeqv A B (ua A B e)) e :=
---lemSig (A → B) (isEquiv A B) (isEquivProp A B) (idtoeqv A B (ua A B e)) e (ideqv-compute A B e)
+opaque transportεIsEquiv
+
+def idtoeqv-ua (A B : U) (e : equiv A B) : Path (equiv A B) (idtoeqv A B (ua A B e)) e :=
+lemSig (A → B) (isEquiv A B) (isEquivProp A B) (idtoeqv A B (ua A B e)) e (ideqv-compute A B e)

share/anders-vscode/syntaxes/anders.tmLanguage.json

@@ -14,7 +14,7 @@
             "name": "comment.line.double-dash.anders"
         },
         {
-            "match": "(?<=^|[\\s()\\[\\]])(token|unsafe|macro|macrovariables|prefix|postfix|infix|infixr|infixl|#eval|#infer|#macroexpand|option|axiom|postulate|def|definition|theorem|lemma|corollary|proposition|import|with|begin|section|end|variables|let|in)(?=$|[\\s()\\[\\]])",
+            "match": "(?<=^|[\\s()\\[\\]])(token|unsafe|macro|macrovariables|prefix|postfix|infix|infixr|infixl|#eval|#infer|#macroexpand|option|opaque|axiom|postulate|def|definition|theorem|lemma|corollary|proposition|import|with|begin|section|end|variables|let|in)(?=$|[\\s()\\[\\]])",
             "name": "keyword.other.anders"
         },
         {

src/frontend/decl.ml

@@ -45,6 +45,7 @@ let rec checkLine conf = function
   | Infer e -> Printf.printf "INFER: %s\n" (Prettyprinter.showExp (infer e)); flush_all (); conf
   | Eval e -> Printf.printf "EVAL: %s\n" (Prettyprinter.showExp (eval e)); flush_all (); conf
   | Operator (op, prec, is) -> List.iter (fun i -> Parser.operators := Dict.add i (op, prec) !Parser.operators) is; conf
+  | Opaque x -> opaque x; conf
   | Decl d ->
     if !Prefs.verbose then begin
       Printf.printf "Checking: %s\n" (getDeclName d); flush_all ()

src/frontend/module.ml

@@ -13,29 +13,28 @@ type command =
   | Command of string * exp
 
 type decl =
-  | Def of string * exp option * exp
-  | Ext of string * exp * string
+  | Def   of string * exp option * exp
+  | Ext   of string * exp * string
   | Axiom of string * exp
 
 type associativity = Left | Right | Neither
 type operator = Infix of associativity | Prefix | Postfix
 
 type line =
-  | Operator of operator * float * string list
-  | Import of string list
-  | Plugin of string
-  | Option of string * string
-  | Variables of tele list
+  | Operator       of operator * float * string list
+  | Import         of string list
+  | Plugin         of string
+  | Option         of string * string
+  | Opaque         of string
+  | Variables      of tele list
   | Macrovariables of string list
-  | Token of string list
-  | Macro of bool * syntax * syntax
-  | Macroexpand of syntax
-  | Decl of decl
-  | Infer of exp
-  | Eval of exp
-  | Section | End
-  | Skip
-  | Eof
+  | Token          of string list
+  | Macro          of bool * syntax * syntax
+  | Macroexpand    of syntax
+  | Decl           of decl
+  | Infer          of exp
+  | Eval           of exp
+  | Section | End | Skip | Eof
 
 type content = line list
 type file = content
@@ -86,6 +85,7 @@ let showLine = function
   | Plugin p -> Printf.sprintf "plugin %s" p
   | Option (opt, value) -> Printf.sprintf "option %s %s" opt value
   | Decl d -> showDecl d
+  | Opaque x -> Printf.sprintf "opaque %s" x
   | Section -> "section" | End -> "end"
   | Variables xs -> Printf.sprintf "variables%s" (showTeles xs)
   | Macrovariables is -> Printf.sprintf "macrovariables %s" (String.concat " " is)

src/frontend/parser.ml

@@ -434,7 +434,7 @@ let ws       = str isWhitespace >> eps
 let nl       = str (fun c -> c = '\n' || c = '\r') >> eps
 let keywords = ["def"; "definition"; "theorem"; "lemma"; "proposition"; "macro"; "import";
                 "prefix"; "postfix"; "infixl"; "infixr"; "infix"; "postulate"; "axiom";
-                "macrovariables"; "option"; "unsafe"; "variables"; "section"; "end";
+                "macrovariables"; "option"; "opaque"; "unsafe"; "variables"; "section"; "end";
                 "token"; "#macroexpand"; "#infer"; "#eval"; "--"; "{-"; "-}"]
 let reserved = ['('; ')'; '['; ']'; '<'; '>'; '\n'; '\t'; '\r'; ' '; '.'; ',']
 
@@ -543,9 +543,10 @@ let tokens         = token "token" >> ws >> sepBy1 ws ident >>= fun is -> pure (
 let variables      = token "variables" >> ws >> binders >>= fun bs -> pure (Variables bs)
 let import         = token "import" >> ws >> sepBy1 ws ident >>= fun fs -> pure (Import fs)
 let options        = token "option" >> ws >> ident >>= fun i -> ws >> ident >>= fun v -> pure (Option (i, v))
+let opaque         = token "opaque" >> ws >> ident >>= fun x -> pure (Opaque x)
 let section        = (token "section" >> pure Section) <|> (token "end" >> pure End)
 
-let commands = import <|> variables <|> options <|> operator <|> macroexpand <|> infer <|> eval <|> macrovariables <|> tokens
+let commands = import <|> variables <|> options <|> opaque <|> operator <|> macroexpand <|> infer <|> eval <|> macrovariables <|> tokens
 let cmdeof   = eof >> pure Eof
 let cmdline  = def <|> axm <|> macro <|> commands <|> section <|> comment <|> cmdeof
 let cmd      = optional ws >> cmdline

src/frontend/radio.ml

@@ -78,6 +78,7 @@ let transmit mesg =
 let def p t e    = transmit (Def (p, t, e))
 let assign p t e = transmit (Assign (p, t, e))
 let assume p t   = transmit (Assume (p, t))
+let opaque x     = transmit (Opaque x)
 
 let set p x = transmit (Set (p, x))
 let wipe () = transmit Wipe

src/kernel/check.ml

@@ -364,16 +364,28 @@ and app (f, x) = match f, x with
 
 and evalSystem ctx = bimap (getDef ctx) (fun mu t -> eval (faceEnv mu ctx) t)
 
-and getType ctx x = match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with
+and evalTerm ctx = function
+  | Exp e   -> eval ctx e
+  | Value v -> v
+
+and getType ctx x =
+  match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with
   | Some (t, _), _ -> t
-  | _, Some (t, _) -> t
+  | _, Some t      -> evalTerm ctx t.typval
   | _, _           -> raise (Internal (VariableNotFound x))
 
-and getDef ctx x = match Env.find_opt x ctx.local, Env.find_opt x !(ctx.global) with
-  | Some (_, v), _       -> v
-  | _, Some (_, Value v) -> v
-  | _, Some (t, Exp e)   -> let v = eval ctx e in upGlobal ctx x t (Value v); v
-  | _, _                 -> raise (Internal (VariableNotFound x))
+and getGlobalDef ctx x =
+  match Env.find_opt x !(ctx.global) with
+  | None   -> raise (Internal (VariableNotFound x))
+  | Some t ->
+    if t.opaque then Var (x, evalTerm ctx t.typval)
+    else match t.defval with
+    | Value v -> v
+    | Exp   e -> let v = eval ctx e in upGlobal ctx x { t with defval = Value v }; v
+
+and getDef ctx x = match Env.find_opt x ctx.local with
+  | Some (_, v) -> v
+  | None        -> getGlobalDef ctx x
 
 and appFormulaE ctx e i = eval ctx (EAppFormula (e, i))
 

src/kernel/chm.ml

@@ -32,13 +32,17 @@ let proto : req -> resp = function
   | Def (x, t0, e0)    -> promote (fun () ->
     let t = freshExp t0 in let e = freshExp e0 in
     isType (infer ctx t); let t' = eval ctx t in
-    check ctx e t'; assign ctx x t' (getTerm e); OK)
+    check ctx e t'; assign ctx x (Value t') (getTerm e); OK)
+  | Opaque x -> let y = ident x in
+    promote (fun () -> match Env.find_opt y !(ctx.global) with
+    | Some t -> upGlobal ctx y { t with opaque = true }; OK
+    | None   -> Error (VariableNotFound y))
   | Assign (x, t0, e0) -> promote (fun () ->
     let t = freshExp t0 in isType (infer ctx t);
-    assign ctx x (eval ctx t) (getTerm (freshExp e0)); OK)
+    assign ctx x (Value (eval ctx t)) (getTerm (freshExp e0)); OK)
   | Assume (x, t0)     -> promote (fun () -> let t = freshExp t0 in
     isType (infer ctx t); let t' = eval ctx t in
-    assign ctx x t' (Value (Var (ident x, t'))); OK)
+    assign ctx x (Value t') (Value (Var (ident x, t'))); OK)
   | Erase x            -> ctx.global := Env.remove (ident x) !(ctx.global); OK
   | Wipe               -> ctx.global := Env.empty; OK
   | Set (p, x)         ->

src/kernel/term.ml

@@ -74,9 +74,11 @@ and clos = ident * (value -> value)
 
 type term = Exp of exp | Value of value
 
+type decl = { typval : term; defval : term; opaque : bool }
+
 type ctx =
   { local  : (value * value) Env.t;
-    global : (value * term) Env.t ref }
+    global : decl Env.t ref }
 
 (* Implementation *)
 
@@ -103,12 +105,12 @@ exception IncompatibleFaces
 
 let upVar p x ctx = match p with Irrefutable -> ctx | _ -> Env.add p x ctx
 let upLocal ctx p t v = { ctx with local = upVar p (t, v) ctx.local }
-let upGlobal ctx p t v = ctx.global := upVar p (t, v) !(ctx.global)
+let upGlobal ctx p t = ctx.global := upVar p t !(ctx.global)
 
 let assign ctx x t e =
   if Env.mem (ident x) !(ctx.global)
   then raise (Internal (AlreadyDeclared x))
-  else upGlobal ctx (ident x) t e
+  else upGlobal ctx (ident x) { typval = t; defval = e; opaque = false }
 
 let freshVar ns n = match Env.find_opt n ns with Some x -> x | None -> n
 let mapFace fn phi = Env.fold (fun p d -> Env.add (fn p) d) phi Env.empty

src/language/decode.ml

@@ -144,7 +144,8 @@ struct
     | '\x21' -> let x = string () in let (t, e) = exp2 () in Assign (x, t, e)
     | '\x22' -> let x = string () in let t = exp () in Assume (x, t)
     | '\x23' -> Erase (string ())
-    | '\x24' -> Wipe
+    | '\x24' -> Opaque (string ())
+    | '\x25' -> Wipe
     | '\x30' -> let p = string () in let x = string () in Set (p, x)
     | '\x31' -> Version
     | '\x32' -> Ping

src/language/encode.ml

@@ -133,7 +133,8 @@ struct
     | Assign (x, t, e) -> W.put '\x21'; string x; exp2 t e
     | Assume (x, t)    -> W.put '\x22'; string x; exp t
     | Erase x          -> W.put '\x23'; string x
-    | Wipe             -> W.put '\x24'
+    | Opaque x         -> W.put '\x24'; string x
+    | Wipe             -> W.put '\x25'
     | Set (p, x)       -> W.put '\x30'; string p; string x
     | Version          -> W.put '\x31'
     | Ping             -> W.put '\x32'

src/language/spec.ml

@@ -119,6 +119,7 @@ type req =
   | Assign of string * exp * exp
   | Assume of string * exp
   | Erase  of string
+  | Opaque of string
   | Wipe
   (* configuration *)
   | Set    of string * string