Update Lean version

Katydid/Conal/Language.lean

@@ -19,6 +19,11 @@ namespace Lang
 -- variable α should be implicit to make sure examples do not need to also provide the parameter of α when constructing char, or, concat, since it usually can be inferred to be Char.
 variable {α : Type u}
 
+-- TODO: Why are these definitions open, instead of in an inductive family, like
+-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20relevance/near/419702213
+-- One reason is that with not operator, which run into the strictly positive limitation, but we don't have the not operator in the Agda paper.
+-- TODO: Ask Conal if there is another reason.
+
 -- ∅ : Lang
 -- ∅ w = ⊥
 def emptySet : Lang α :=
@@ -79,7 +84,10 @@ def star (P : Lang α) : Lang α :=
   fun (w : List α) =>
     Σ' (ws : List (List α)), (_pws: All P ws) ×' w = (List.join ws)
 
-#print star
+-- TODO: What does proof relevance even mean for the `not` operator?
+def not (P: Lang α) : Lang α :=
+  fun (w: List α) =>
+    P w -> Empty
 
 -- attribute [simp] allows these definitions to be unfolded when using the simp tactic.
 attribute [simp] universal emptySet emptyStr char scalar or and concat star

Katydid/Std/Tipe.lean

@@ -47,7 +47,7 @@ def eq_of_teq {α : Type u} {a a' : α} (h : TEq a a') : Eq a a' :=
       h₁.rec (fun _ => rfl)
   this α α a a' h rfl
 
--- TODO: Find out if this is legal
+-- This is legal because TEq is a sub singleton, it has one of fewer ways to be constructed.
 def teq_of_eq {α : Type u} {a a' : α} (h : Eq a a') : TEq a a' :=
   have : (α β : Type u) → (a b: α) → Eq a b → (h : TEq α β) → TEq a b :=
     fun _ _ _ _ h₁ =>
@@ -121,21 +121,6 @@ structure TIff (a b : Type) : Type where
   /-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/
   mpr : b → a
 
-infix:19 " <-> " => TIff
-
-structure Tiso (a b : Type) : Type where
-  intro ::
-  f : a → b
-  f' : b → a
-  ff' : ∀ x, f (f' x) ≡ x
-  f'f : ∀ x, f' (f x) ≡ x
-
-infix:19 " ↔ " => Tiso -- slash <->
-
-def Teso {w : α} (P : α -> Type) (Q : α -> Type) := Tiso (P w) (Q w)
-
-infix:19 " ⟷ " => Teso -- slash <-->
-
 theorem t : 1 ≡ 2 -> False := by
   intro x
   contradiction

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.5.0