WIP: bump to Lean 4.31.0-rc1

HoTTLean.lean

@@ -1,5 +1,64 @@
-import HoTTLean.Groupoids.Sigma
-import HoTTLean.Groupoids.Pi
+import HoTTLean.Prelude
+import HoTTLean.Experiments
+import HoTTLean.ForMathlib.CategoryTheory.Bicategory.Grothendieck
+import HoTTLean.ForMathlib.CategoryTheory.Core
+import HoTTLean.ForMathlib.CategoryTheory.FreeGroupoid
+import HoTTLean.ForMathlib.CategoryTheory.Functor.IsPullback
+import HoTTLean.ForMathlib.CategoryTheory.Functor.Iso
+import HoTTLean.ForMathlib.CategoryTheory.Groupoid
+import HoTTLean.ForMathlib.CategoryTheory.Grpd
+import HoTTLean.ForMathlib.CategoryTheory.Localization.Predicate
+import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.Basic
+import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.WideSubcategory
+import HoTTLean.ForMathlib.CategoryTheory.NatTrans
+import HoTTLean.ForMathlib.CategoryTheory.RepPullbackCone
+import HoTTLean.ForMathlib.CategoryTheory.WeakPullback
+import HoTTLean.ForMathlib.CategoryTheory.Whiskering
+import HoTTLean.ForMathlib.CategoryTheory.Yoneda
+import HoTTLean.ForMathlib.Tactic.CategoryTheory.FunctorMap
+import HoTTLean.ForMathlib
+import HoTTLean.ForPoly
+import HoTTLean.Frontend.Checked
+import HoTTLean.Frontend.Commands
+import HoTTLean.Frontend.EnvExt
+import HoTTLean.Frontend.Translation
+import HoTTLean.Grothendieck.Groupoidal.Basic
+import HoTTLean.Grothendieck.Groupoidal.IsPullback
+import HoTTLean.Grothendieck.IsPullback
+import HoTTLean.Groupoids.Basic
+import HoTTLean.Groupoids.ClovenIsofibration
 import HoTTLean.Groupoids.Id
+import HoTTLean.Groupoids.IsPullback
+import HoTTLean.Groupoids.Pi
+import HoTTLean.Groupoids.Sigma
+import HoTTLean.Groupoids.UHom
+import HoTTLean.Groupoids.UnstructuredModel
+import HoTTLean.Model.Natural.Interpretation
+import HoTTLean.Model.Natural.NaturalModel
+import HoTTLean.Model.Natural.UHom
+import HoTTLean.Model.Unstructured.Hurewicz
 import HoTTLean.Model.Unstructured.Interpretation
-import HoTTLean.Frontend.Commands
+import HoTTLean.Model.Unstructured.UHom
+import HoTTLean.Model.Unstructured.UnstructuredUniverse
+import HoTTLean.Pointed.Basic
+import HoTTLean.Pointed.IsPullback
+import HoTTLean.Syntax.Autosubst
+import HoTTLean.Syntax.Axioms
+import HoTTLean.Syntax.Basic
+import HoTTLean.Syntax.EqCtx
+import HoTTLean.Syntax.GCongr
+import HoTTLean.Syntax.Injectivity
+import HoTTLean.Syntax.Inversion
+import HoTTLean.Syntax.InversionLemmas
+import HoTTLean.Syntax.Substitution
+import HoTTLean.Syntax.Synth
+import HoTTLean.Syntax.Typing
+import HoTTLean.Tactic.GrindCases
+import HoTTLean.Tactic.MutualInduction
+import HoTTLean.Typechecker.Cache
+import HoTTLean.Typechecker.Equate
+import HoTTLean.Typechecker.Evaluate
+import HoTTLean.Typechecker.Synth
+import HoTTLean.Typechecker.Util
+import HoTTLean.Typechecker.Value
+import HoTTLean.Typechecker.ValueInversion

HoTTLean/Experiments.lean

@@ -0,0 +1,30 @@
+import HoTTLean.Frontend.Commands
+
+namespace HoTTLean.Experiments
+
+declare_theory ab
+
+ab axiom add (X : Type) : X → X → X
+
+ab axiom zero (X : Type) : X
+
+-- I would like this to be stated as an equality `(add X a (add X b c)) = (add X (add X a b) c)`
+-- but that gives an error
+ab axiom assoc {X : Type} (a b c : X) : Identity (add X a (add X b c)) (add X (add X a b) c)
+
+-- I would also like this to be stated with `=`
+ab axiom comm' {X : Type} (a b : X) : Identity (add X a b) (add X b a)
+
+-- I would also like this to be stated with `=`
+ab axiom add_zero {X : Type} (a : X) : Identity (add X a (zero X)) a
+
+-- Now I want to state and prove the following theorem internally:
+-- `ab theorem zero_add {X : Type} (a : X) : Identity (add X (zero X) a) a := ...`
+
+-- And then I want to prove that any `X : Type` with `[AddCommGroup X]` is a model for the theory
+-- `ab` by proving that it satisfies all the axioms.
+
+-- Next, I want to prove that `zero_add` holds for any `X : Type` with `[AddCommGroup X]`
+-- by using the `ab` theorem `zero_add` (not relying on an existing mathlib proof).
+
+end HoTTLean.Experiments