From 3c0f974fd4aac4cfac289516aa33502376139676 Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Sat, 17 Aug 2024 17:40:51 +0200
Subject: [PATCH 1/6] Add a configuration for building with dune

---
 2017-12-Birmingham/dune  | 11 +++++++++++
 2019-04-Birmingham/dune  | 11 +++++++++++
 2019-07-Columbus/dune    | 11 +++++++++++
 2022-07-Cortona/dune     | 11 +++++++++++
 2024-07-Minneapolis/dune | 11 +++++++++++
 dune-project             |  3 +++
 6 files changed, 58 insertions(+)
 create mode 100644 2017-12-Birmingham/dune
 create mode 100644 2019-04-Birmingham/dune
 create mode 100644 2019-07-Columbus/dune
 create mode 100644 2022-07-Cortona/dune
 create mode 100644 2024-07-Minneapolis/dune
 create mode 100644 dune-project

diff --git a/2017-12-Birmingham/dune b/2017-12-Birmingham/dune
new file mode 100644
index 0000000..8449ebd
--- /dev/null
+++ b/2017-12-Birmingham/dune
@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Birmingham2017)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+
diff --git a/2019-04-Birmingham/dune b/2019-04-Birmingham/dune
new file mode 100644
index 0000000..8b8eb17
--- /dev/null
+++ b/2019-04-Birmingham/dune
@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Birmingham2019)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+
diff --git a/2019-07-Columbus/dune b/2019-07-Columbus/dune
new file mode 100644
index 0000000..6f205ff
--- /dev/null
+++ b/2019-07-Columbus/dune
@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Columbus2019)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+
diff --git a/2022-07-Cortona/dune b/2022-07-Cortona/dune
new file mode 100644
index 0000000..e5d3608
--- /dev/null
+++ b/2022-07-Cortona/dune
@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Cortona2022)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+
diff --git a/2024-07-Minneapolis/dune b/2024-07-Minneapolis/dune
new file mode 100644
index 0000000..f9fff14
--- /dev/null
+++ b/2024-07-Minneapolis/dune
@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Minneapolis2024)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..e950e14
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.5)
+(using coq 0.6)
+(name Schools)

From f4d49a9b8f3bbe25a8288d3436eeba6f60cd50aa Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Sat, 17 Aug 2024 17:50:22 +0200
Subject: [PATCH 2/6] Add a CI build script

---
 .github/workflows/build-schools.yml | 59 ++++++++++++++++++++++-------
 1 file changed, 45 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml
index 90a9672..fa506cf 100644
--- a/.github/workflows/build-schools.yml
+++ b/.github/workflows/build-schools.yml
@@ -2,7 +2,7 @@
 
 name: CI
 
-# Controls when the action will run. 
+# Controls when the action will run.
 on:
   # Triggers the workflow on push or pull request events but only for the master branch
   push:
@@ -10,28 +10,59 @@ on:
   pull_request:
     branches: [ master ]
 
+  schedule:
+    # Run this workflow at 02:15 UTC every Tuesday to keep the cache from being
+    # evicted. A typical run with everything cached should take less than 10
+    # minutes.
+    - cron: 15 2 * * TUE
+
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 
+env:
+  # Set this to the version of Coq that should be used.
+  coq-version: 8.20.0
+  dune-version: 3.5.0
+  DUNE_CACHE_STORAGE_MODE: copy
+
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
   # This workflow contains a single job called "build"
   build:
+    name: Build Schools
     # The type of runner that the job will run on
     runs-on: ubuntu-latest
 
     # Steps represent a sequence of tasks that will be executed as part of the job
     steps:
-      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
-      - uses: actions/checkout@v2
-
-      
-      # Install everything needed for building UniMath (and more)
-      - name: Install build dependencies
-        run: sudo apt-get install build-essential git ocaml ocaml-nox ocaml-native-compilers camlp5 libgtk2.0 libgtksourceview2.0 liblablgtk-extras-ocaml-dev ocaml-findlib libnum-ocaml-dev emacs
-
-      # Change into UniMath directory and build UniMath
-      - name: Build UniMath and Schools files
-        run: |
-          cd $GITHUB_WORKSPACE
-          time make 
+      # Checkout UniMath into the working directory
+      - name: Checkout UniMath.
+        uses: actions/checkout@v3
+        with:
+          repository: UniMath/UniMath
+          clean: false
+          path: .
+
+      # Checkout the current branch into Schools/
+      - name: Checkout Schools.
+        uses: actions/checkout@v3
+        with:
+          path: Schools
+
+      # Ideally we would use docker-coq. A setup currently takes about 7min
+      # before it starts compiling, with OCaml cached.
+      - name: Install OCaml.
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda
+          dune-cache: true
+          opam-disable-sandboxing: true
+
+      - name: Install Dune
+        run: opam pin add dune ${{ env.dune-version }}
+      - name: Install Coq
+        run: opam pin add coq ${{ env.coq-version }}
+
+      # Schools is built using the flags specified in code/dune.
+      - name: Compile SetHITs.
+        run: opam exec -- dune build SetHITs --display=short --error-reporting=twice

From 60ace1f93de635feda32171f21b2d79101703a2e Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Sat, 17 Aug 2024 18:03:12 +0200
Subject: [PATCH 3/6] Revert to the newest existing version of coq: 8.19.0,
 instead of the future 8.20.0

---
 .github/workflows/build-schools.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml
index fa506cf..24b632e 100644
--- a/.github/workflows/build-schools.yml
+++ b/.github/workflows/build-schools.yml
@@ -21,7 +21,7 @@ on:
 
 env:
   # Set this to the version of Coq that should be used.
-  coq-version: 8.20.0
+  coq-version: 8.19.0
   dune-version: 3.5.0
   DUNE_CACHE_STORAGE_MODE: copy
 

From a8c8c86ff84ac91007ab4ae88aaf679d11714527 Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Sat, 17 Aug 2024 18:51:55 +0200
Subject: [PATCH 4/6] Build Schools instead of SetHITs

---
 .github/workflows/build-schools.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml
index 24b632e..0bcbdfa 100644
--- a/.github/workflows/build-schools.yml
+++ b/.github/workflows/build-schools.yml
@@ -64,5 +64,5 @@ jobs:
         run: opam pin add coq ${{ env.coq-version }}
 
       # Schools is built using the flags specified in code/dune.
-      - name: Compile SetHITs.
-        run: opam exec -- dune build SetHITs --display=short --error-reporting=twice
+      - name: Compile Schools.
+        run: opam exec -- dune build Schools --display=short --error-reporting=twice

From 9f462477619d2483434bdb71c86beac4ba103424 Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Sat, 17 Aug 2024 19:42:18 +0200
Subject: [PATCH 5/6] Increase dune to version 3.8

---
 .github/workflows/build-schools.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml
index 0bcbdfa..79c0c34 100644
--- a/.github/workflows/build-schools.yml
+++ b/.github/workflows/build-schools.yml
@@ -22,7 +22,7 @@ on:
 env:
   # Set this to the version of Coq that should be used.
   coq-version: 8.19.0
-  dune-version: 3.5.0
+  dune-version: 3.8.0
   DUNE_CACHE_STORAGE_MODE: copy
 
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel

From f507d9b21dc0f5e5471bc6ab0061c4763084300b Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Mon, 19 Aug 2024 09:20:42 +0200
Subject: [PATCH 6/6] Make sure that CI succeeds again for the exercises and
 solutions (and disable Search statements, because of clutter)

---
 .../Part4_Tactics_UniMath/lecture_tactics.v   | 12 ++--
 .../lecture_tactics_long_version.v            | 18 +++---
 .../category_theory_exercises.v               | 19 ++++---
 .../category_theory_solutions.v               | 19 ++++---
 .../fundamentals_lecture.v                    |  2 +-
 .../truncation_exercices.v                    |  4 +-
 .../Part4_Tactics_UniMath/lecture_tactics.v   | 12 ++--
 .../lecture_tactics_long_version.v            | 18 +++---
 .../weq_exercises_with_solutions.v            |  5 +-
 .../Part6_Category_Theory/category_theory.v   | 21 ++++---
 .../category_theory_exercises.v               | 22 +++++---
 .../category_theory_solutions.v               | 56 +++++++++----------
 .../Part7_Paradoxes/RussellsParadox.v         | 15 ++---
 .../2_Fundamentals-Coq/coq_exercises.v        |  2 +-
 .../2_Fundamentals-Coq/fundamentals_lecture.v |  2 +-
 .../4_Tactics-UniMath/lecture_tactics.v       | 12 ++--
 .../lecture_tactics_long_version.v            | 22 ++++----
 .../weq_exercises_with_solutions.v            |  3 +-
 .../6_Category_Theory/category_theory.v       |  6 +-
 .../category_theory_exercises.v               | 18 +++---
 .../category_theory_solutions.v               | 46 +++++++--------
 .../Synthetic_Homotopy_Theory.v               | 42 +++++++-------
 .../2_Coq/fundamentals_lecture.v              |  2 +-
 .../4_Tactics/tactics_lecture.v               | 12 ++--
 .../4_Tactics/tactics_lecture_extended.v      | 18 +++---
 .../set_level_mathematics_exercises.v         |  4 +-
 .../set_level_mathematics_solutions.v         |  4 +-
 .../6_Category-theory-in-UF/category_theory.v |  6 +-
 .../category_theory_exercises.v               | 18 +++---
 .../category_theory_solutions.v               | 46 +++++++--------
 30 files changed, 246 insertions(+), 240 deletions(-)

diff --git a/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v b/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
index c2a2594..f37b3d0 100644
--- a/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
+++ b/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
@@ -47,10 +47,10 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you think there are too many hits and you only want to
       find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -62,14 +62,14 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.
 
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -101,7 +101,7 @@ Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one *)
@@ -404,7 +404,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    Search (_ × _).
+    (* Search (_ × _). *)
     (** No hope at all for our equation - we can only hope
         for weak equivalence. *)
 Abort.
diff --git a/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v b/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
index 31105e5..4db4730 100644
--- a/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
+++ b/2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
@@ -47,10 +47,10 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you think there are too many hits and you only want to
       find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -62,14 +62,14 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.
 
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -101,7 +101,7 @@ Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one *)
@@ -369,9 +369,9 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-SearchPattern (paths _ _).
+(* SearchPattern (paths _ _). *)
 (** Among the search results is [pathsinv0l] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -504,11 +504,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern(_ × _).
+    (* SearchPattern(_ × _). *)
     (** No hope at all - we can only hope for weak equivalence. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.
diff --git a/2017-12-Birmingham/Part6_Category_Theory/category_theory_exercises.v b/2017-12-Birmingham/Part6_Category_Theory/category_theory_exercises.v
index eab4da1..78b8fc4 100644
--- a/2017-12-Birmingham/Part6_Category_Theory/category_theory_exercises.v
+++ b/2017-12-Birmingham/Part6_Category_Theory/category_theory_exercises.v
@@ -6,15 +6,18 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 
diff --git a/2017-12-Birmingham/Part6_Category_Theory/category_theory_solutions.v b/2017-12-Birmingham/Part6_Category_Theory/category_theory_solutions.v
index 912a27a..fceeade 100644
--- a/2017-12-Birmingham/Part6_Category_Theory/category_theory_solutions.v
+++ b/2017-12-Birmingham/Part6_Category_Theory/category_theory_solutions.v
@@ -7,15 +7,18 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 
diff --git a/2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v b/2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v
index 78d1b33..59ee4ca 100644
--- a/2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v
+++ b/2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v
@@ -470,7 +470,7 @@ in UniMath it is very important to be able to search the library so
 that you don't do something someone else has already done. *)
 
 (** To find everything about nat type: *)
-Search nat.
+(* Search nat. *)
 
 (** To search for all lemmas involving the pattern *)
 (* Search _ (_ -> _ -> _). *)
diff --git a/2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v b/2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v
index 93bde48..e122d7c 100644
--- a/2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v
+++ b/2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v
@@ -69,8 +69,8 @@ Definition parity (n : nat) := nat_rect (fun _ => nat) 0 (fun _ b => flip b) n.
    notion of image in which we replace ∑ with ∃. *)
 Require Import UniMath.Foundations.Propositions.
 
-Definition image {A B : UU} (f : A → B) :
-  ∑ (y : B), ∃ (x : A), f x = y.
+Definition image {A B : UU} (f : A → B) : UU
+  := ∑ (y : B), ∃ (x : A), f x = y.
 
 (* Prove that the (univalent) image of partiy is equivalent to Bool. *)
 Theorem image_parity_equiv_bool :
diff --git a/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v b/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
index 4470fcf..696d76c 100644
--- a/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
+++ b/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v
@@ -48,9 +48,9 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -62,14 +62,14 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.
 
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -102,7 +102,7 @@ Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -395,7 +395,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    Search (_ × _).
+    (* Search (_ × _). *)
     (** No hope at all for our equation - we can only hope
         for weak equivalence. *)
 Abort.
diff --git a/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v b/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
index ee4f844..8f074a5 100644
--- a/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
+++ b/2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v
@@ -49,9 +49,9 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -65,7 +65,7 @@ Defined.
     verify it and to associate it with the given identifer, here [myfirsttruthvalue].
     This may go wrong for different reasons, including implementation errors of the Coq
     system - that will not affect trustworthiness of the library. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.
 (** [myfirsttruthvalue relies on an unsafe universe hierarchy] is output to indicate
@@ -74,7 +74,7 @@ Print myfirsttruthvalue.
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -107,7 +107,7 @@ Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -360,9 +360,9 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-SearchPattern (paths _ _).
+(* SearchPattern (paths _ _). *)
 (** Among the search results is [maponpathsinv0] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -500,11 +500,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern(_ × _).
+    (* SearchPattern(_ × _). *)
     (** No hope at all - we can only hope for weak equivalence. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.
diff --git a/2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises_with_solutions.v b/2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises_with_solutions.v
index 5adec2f..8df1898 100644
--- a/2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises_with_solutions.v
+++ b/2019-04-Birmingham/Part4_Tactics_UniMath/weq_exercises_with_solutions.v
@@ -38,8 +38,9 @@ Proof.
   - cbn.
     intro p.
     induction p as [x H].
-    unfold idfun in H.
-    rewrite H.
+    (* unfold idfun in H.
+    rewrite H. *)
+    induction H.
     apply idpath.
 Defined.
 
diff --git a/2019-04-Birmingham/Part6_Category_Theory/category_theory.v b/2019-04-Birmingham/Part6_Category_Theory/category_theory.v
index 88a238f..a725154 100644
--- a/2019-04-Birmingham/Part6_Category_Theory/category_theory.v
+++ b/2019-04-Birmingham/Part6_Category_Theory/category_theory.v
@@ -12,9 +12,12 @@ Require Import UniMath.CategoryTheory.Core.Univalence.
 Require Import UniMath.CategoryTheory.Core.Functors.
 Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
 Require Import UniMath.CategoryTheory.Core.Isos.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Total.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 
 Open Scope cat.
 
@@ -24,7 +27,7 @@ These definition are done in multiple steps. First we, define the data and then
  *)
 Definition maybe_data : functor_data SET SET.
 Proof.
-  use mk_functor_data.
+  use make_functor_data.
   - exact (λ X, setcoprod X unitset).
   - intros X Y f x.
     induction x as [x | y].
@@ -62,7 +65,7 @@ By combining these two, we get an actual functor from `SET` to `SET`.
  *)
 Definition maybe : SET ⟶ SET.
 Proof.
-  use mk_functor.
+  use make_functor.
   - exact maybe_data.
   - exact maybe_is_functor.
 Defined.
@@ -82,10 +85,10 @@ Proof.
   intros X Y f.
   apply idpath.
 Qed.
-  
+
 Definition pure : functor_identity SET ⟹ maybe.
 Proof.
-  use mk_nat_trans.
+  use make_nat_trans.
   - exact pure_data.
   - exact pure_is_nat_trans.
 Defined.
@@ -104,7 +107,7 @@ A displayed morphism over `f : X → Y` from `x` to `y` is a path `f x = y`.
 Definition pointed_disp_ob_mor
   : disp_cat_ob_mor SET.
 Proof.
-  use mk_disp_cat_ob_mor.
+  use make_disp_cat_ob_mor.
   - intro X.
     apply X.
   - exact (λ X Y x y f, f x = y).
@@ -148,7 +151,7 @@ Definition pointed_disp_cat_axioms
 Proof.
   repeat split.
   - intros X Y f x y p.
-    apply transportf_transpose.
+    apply transportf_transpose_right.
     apply transportf_comp_lemma_hset.
     { apply homset_property. }
     cbn in *.
@@ -210,7 +213,7 @@ Proof.
   - apply X.
   - apply isaproptotal2.
     + intro.
-      apply isaprop_is_iso_disp.
+      apply isaprop_is_z_iso_disp.
     + intros p q r₁ r₂.
       apply X.
 Defined.
@@ -224,4 +227,4 @@ Proof.
   apply is_univalent_total_category.
   - exact is_univalent_HSET.
   - exact is_univalent_pointed_disp_cat.
-Defined.
\ No newline at end of file
+Defined.
diff --git a/2019-04-Birmingham/Part6_Category_Theory/category_theory_exercises.v b/2019-04-Birmingham/Part6_Category_Theory/category_theory_exercises.v
index 92aeaee..6938c86 100644
--- a/2019-04-Birmingham/Part6_Category_Theory/category_theory_exercises.v
+++ b/2019-04-Birmingham/Part6_Category_Theory/category_theory_exercises.v
@@ -6,19 +6,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Total.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+
+Local Open Scope cat.
 
 (* NOTE: some of these exercises (or parts of them) are straightforward, while other parts are intended to be quite difficult.  So I don’t recomment aiming to complete them in order — if stuck on a difficult part, move on and come back for another attempt later!
 
diff --git a/2019-04-Birmingham/Part6_Category_Theory/category_theory_solutions.v b/2019-04-Birmingham/Part6_Category_Theory/category_theory_solutions.v
index 0315c30..a6b57fa 100644
--- a/2019-04-Birmingham/Part6_Category_Theory/category_theory_solutions.v
+++ b/2019-04-Birmingham/Part6_Category_Theory/category_theory_solutions.v
@@ -11,20 +11,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
+Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 
 (* NOTE: some of these exercises (or parts of them) are straightforward, while other parts are intended to be quite difficult.  So I don’t recomment aiming to complete them in order — if stuck on a difficult part, move on and come back for another attempt later!
@@ -36,18 +39,17 @@ Section Exercise_0.
 
   Show that in any univalent category, the type of objects has h-level 3 *)
 
-  Proposition isofhlevel3_ob_of_univalent_cat (C : category) (H : is_univalent C)
+  Proposition isofhlevel3_ob_of_univalent_cat (C : category) (univ : is_univalent C)
     : isofhlevel 3 (ob C).
   Proof.
     intros a b.
-    induction H as [univ homsets].
     apply (isofhlevelweqb 2 (make_weq idtoiso (univ a b))).
     unfold iso.
     apply isofhleveltotal2.
-    - apply homsets.
+    - apply homset_property.
     - intro f.
       apply isasetaprop.
-      apply isaprop_is_iso.
+      apply isaprop_is_z_isomorphism.
   Qed.
 End Exercise_0.
 
@@ -120,20 +122,17 @@ Section Exercise_1.
 
   Proposition nat_category_not_univalent : ¬ (is_univalent nat_category).
   Proof.
-    intros [univ_nat homsets].
+    intros univ_nat.
     set (equiv22 := univ_nat 2 2).
     assert (isaprop_id : isaprop (2 = 2)).
     { apply isasetnat. }
     set (isaprop_iso := isofhlevelweqf 1 (make_weq idtoiso equiv22) isaprop_id).
     set (zero := stnel (2,0)).
     set (one := stnel (2,1)).
-    set (f := @identity nat_category_data 2).
-    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%Cat).
-    set (fiso := identity_is_iso nat_category 2).
-    assert (giso : is_iso g).
+    set (f := identity_z_iso (C := nat_category) 2).
+    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%cat).
+    assert (giso : is_inverse_in_precat g g).
     {
-      apply (@is_iso_from_is_z_iso nat_category 2 2).
-      exists g.
       unfold is_inverse_in_precat. split.
       - apply funextfun.
         unfold homot.
@@ -146,15 +145,14 @@ Section Exercise_1.
         + apply idpath.
         + apply idpath.
     }
-    set (f' := make_iso _ fiso).
-    set (g' := @make_iso nat_category 2 2 g giso).
+    set (g' := make_z_iso g g giso).
     set (proofirr_iso := proofirrelevance _ isaprop_iso).
-    set (f'eqg' := proofirr_iso f' g').
+    set (f'eqg' := proofirr_iso f g').
     assert (nonsense : stnel (2,0) = stnel (2,1)).
     {
-      change (stnpr 0) with (f (stnpr 0)).
+      change (stnpr 0) with (z_iso_mor f (stnpr 0)).
       change (stnpr 1) with (g (stnpr 0)).
-      apply (@eqtohomot _ _ f g).
+      apply (@eqtohomot _ _ (z_iso_mor f) g).
       exact (maponpaths pr1 f'eqg').
     }
     apply (negpaths0sx 0).
@@ -265,7 +263,7 @@ Section Exercise_2.
     - apply X.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         apply X.
   Defined.
@@ -287,7 +285,7 @@ Section Exercise_2.
       apply isaset_set_fun_space.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         simpl in p, q.
         use funextsec.
@@ -309,7 +307,7 @@ Section Exercise_2.
     : is_univalent pointed_operation_set.
   Proof.
     apply is_univalent_total_category.
-    - Search HSET.
+    - (* Search HSET. *)
       exact is_univalent_HSET.
     - exact pointed_operation_is_univalent_disp.
   Defined.
@@ -392,7 +390,7 @@ Section Exercise_3.
     use total2_paths_f.
     - apply isotoid.
       + apply univalent_category_is_univalent.
-      + exact (iso_Initials aInit bInit).
+      + exact (ziso_Initials aInit bInit).
     - apply proofirrelevance.
       unfold isInitial.
       apply impred_isaprop.
diff --git a/2019-04-Birmingham/Part7_Paradoxes/RussellsParadox.v b/2019-04-Birmingham/Part7_Paradoxes/RussellsParadox.v
index c45e9a8..2d4af73 100644
--- a/2019-04-Birmingham/Part7_Paradoxes/RussellsParadox.v
+++ b/2019-04-Birmingham/Part7_Paradoxes/RussellsParadox.v
@@ -8,6 +8,8 @@
 
 **)
 
+Require Import UniMath.Foundations.All.
+
 Section russell.
 
 Set Implicit Arguments.
@@ -16,14 +18,13 @@ Set Implicit Arguments.
     which contains names for all sets.
 *)
 
-Variable set : Set.
-Variable name : Set -> set.
-Variable El : set -> Set.
-Axiom reflect : forall A:Set,A = El (name A).
-
-
-Lemma paradox : False.
+Variable set : hSet.
+Variable name : hSet → set.
+Variable El : set → hSet.
+Axiom reflect : ∏ A:hSet, A = El (name A).
 
+Lemma paradox : ∅.
+Abort.
 
 End russell.
 
diff --git a/2022-07-Cortona/2_Fundamentals-Coq/coq_exercises.v b/2022-07-Cortona/2_Fundamentals-Coq/coq_exercises.v
index 3e53973..e3254d4 100644
--- a/2022-07-Cortona/2_Fundamentals-Coq/coq_exercises.v
+++ b/2022-07-Cortona/2_Fundamentals-Coq/coq_exercises.v
@@ -67,7 +67,7 @@ this is already used. *)
 
 (* Check that negbool' uses ifbool by disabling printing of notations *)
 (* Command palette Display All Basic Low-level Contents. *)
-Print negbool'.
+(* Print negbool'. *)
 (* Command palette Display All Basic Low-level Contents. *)
 
 (* This should satisfy:
diff --git a/2022-07-Cortona/2_Fundamentals-Coq/fundamentals_lecture.v b/2022-07-Cortona/2_Fundamentals-Coq/fundamentals_lecture.v
index ea2887c..d5371df 100644
--- a/2022-07-Cortona/2_Fundamentals-Coq/fundamentals_lecture.v
+++ b/2022-07-Cortona/2_Fundamentals-Coq/fundamentals_lecture.v
@@ -526,7 +526,7 @@ in UniMath it is very important to be able to search the library so
 that you don't do something someone else has already done. *)
 
 (** To find everything about nat type: *)
-Search nat.
+(* Search nat. *)
 
 (** To search for all lemmas involving the pattern *)
 (* Search _ (_ -> _ -> _). *)
diff --git a/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.v b/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.v
index 0b4c52d..fcd6946 100644
--- a/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.v
+++ b/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics.v
@@ -57,9 +57,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -71,7 +71,7 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -79,7 +79,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -112,7 +112,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -399,7 +399,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern (_ × _ =  _ × _).
+    (* SearchPattern (_ × _ =  _ × _). *)
     (** Nothing for our equation - we can only hope for weak equivalence ≃,
         see the exercises. *)
 Abort.
diff --git a/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.v b/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.v
index a784c57..8641136 100644
--- a/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.v
+++ b/2022-07-Cortona/4_Tactics-UniMath/lecture_tactics_long_version.v
@@ -10,7 +10,7 @@
     and for exploring the UniMath library.
 
     The material is based on the extended version of the
-    presentation at the UniMath schools 2017 and 2019 in 
+    presentation at the UniMath schools 2017 and 2019 in
     Birmingham, but updated to fit with the changes in (the
     practice of) UniMath.
 
@@ -60,9 +60,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -76,7 +76,7 @@ Defined.
     verify it and to associate it with the given identifer, here [myfirsttruthvalue].
     This may go wrong for different reasons, including implementation errors of the Coq
     system - that will not affect trustworthiness of the library. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -87,7 +87,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -120,7 +120,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -370,9 +370,9 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-SearchPattern (paths _ _).
+(* SearchPattern (paths _ _). *)
 (** Among the search results is [pathsinv0r] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -507,11 +507,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern (_ × _ =  _ × _).
+    (* SearchPattern (_ × _ =  _ × _). *)
     (** Nothing for our equation - we can only hope for weak equivalence ≃. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.
@@ -770,7 +770,7 @@ Proof.
 Defined.
 
 (** The sequential composition is written by (infix) semicolon,
-    and the two branches reated by [split] are treated in the 
+    and the two branches reated by [split] are treated in the
     |-separated list of arguments to the brackets. *)
 
 (** Why would we want to do such compositions? There are at least four good reasons:
diff --git a/2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v b/2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v
index d17355f..d2d6154 100644
--- a/2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v
+++ b/2022-07-Cortona/4_Tactics-UniMath/weq_exercises_with_solutions.v
@@ -40,7 +40,8 @@ Proof.
   - cbn.
     intro p.
     induction p as [x H].
-    rewrite H.
+    (* rewrite H. *)
+    induction H.
     apply idpath.
 Defined.
 
diff --git a/2022-07-Cortona/6_Category_Theory/category_theory.v b/2022-07-Cortona/6_Category_Theory/category_theory.v
index 0164ca1..8398380 100644
--- a/2022-07-Cortona/6_Category_Theory/category_theory.v
+++ b/2022-07-Cortona/6_Category_Theory/category_theory.v
@@ -12,7 +12,7 @@ Require Import UniMath.CategoryTheory.Core.Univalence.
 Require Import UniMath.CategoryTheory.Core.Functors.
 Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
 Require Import UniMath.CategoryTheory.Core.Isos.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
@@ -85,7 +85,7 @@ Proof.
   intros X Y f.
   apply idpath.
 Qed.
-  
+
 Definition pure : functor_identity SET ⟹ maybe.
 Proof.
   use make_nat_trans.
@@ -213,7 +213,7 @@ Proof.
   - apply X.
   - apply isaproptotal2.
     + intro.
-      apply isaprop_is_iso_disp.
+      apply isaprop_is_z_iso_disp.
     + intros p q r₁ r₂.
       apply X.
 Defined.
diff --git a/2022-07-Cortona/6_Category_Theory/category_theory_exercises.v b/2022-07-Cortona/6_Category_Theory/category_theory_exercises.v
index 39e5ca6..3ea8714 100644
--- a/2022-07-Cortona/6_Category_Theory/category_theory_exercises.v
+++ b/2022-07-Cortona/6_Category_Theory/category_theory_exercises.v
@@ -6,23 +6,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 Local Open Scope cat.
 
diff --git a/2022-07-Cortona/6_Category_Theory/category_theory_solutions.v b/2022-07-Cortona/6_Category_Theory/category_theory_solutions.v
index 39561b4..a8e7434 100644
--- a/2022-07-Cortona/6_Category_Theory/category_theory_solutions.v
+++ b/2022-07-Cortona/6_Category_Theory/category_theory_solutions.v
@@ -11,23 +11,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 Local Open Scope cat.
 
@@ -52,7 +52,7 @@ Section Exercise_0.
     - apply homset_property.
     - intro f.
       apply isasetaprop.
-      apply isaprop_is_iso.
+      apply isaprop_is_z_isomorphism.
   Qed.
 End Exercise_0.
 
@@ -133,13 +133,10 @@ Section Exercise_1.
     set (isaprop_iso := isofhlevelweqf 1 (make_weq idtoiso equiv22) isaprop_id).
     set (zero := stnel (2,0)).
     set (one := stnel (2,1)).
-    set (f := @identity nat_category_data 2).
-    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%Cat).
-    set (fiso := identity_is_iso nat_category 2).
-    assert (giso : is_iso g).
+    set (f := identity_z_iso (C := nat_category) 2).
+    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%cat).
+    assert (giso : is_inverse_in_precat g g).
     {
-      apply (@is_iso_from_is_z_iso nat_category 2 2).
-      exists g.
       unfold is_inverse_in_precat. split.
       - apply funextfun.
         unfold homot.
@@ -152,15 +149,14 @@ Section Exercise_1.
         + apply idpath.
         + apply idpath.
     }
-    set (f' := make_iso _ fiso).
-    set (g' := @make_iso nat_category 2 2 g giso).
+    set (g' := make_z_iso g g giso).
     set (proofirr_iso := proofirrelevance _ isaprop_iso).
-    set (f'eqg' := proofirr_iso f' g').
+    set (f'eqg' := proofirr_iso f g').
     assert (nonsense : stnel (2,0) = stnel (2,1)).
     {
-      change (stnpr 0) with (f (stnpr 0)).
+      change (stnpr 0) with (z_iso_mor f (stnpr 0)).
       change (stnpr 1) with (g (stnpr 0)).
-      apply (@eqtohomot _ _ f g).
+      apply (@eqtohomot _ _ (z_iso_mor f) g).
       exact (maponpaths pr1 f'eqg').
     }
     apply (negpaths0sx 0).
@@ -271,7 +267,7 @@ Section Exercise_2.
     - apply X.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         apply X.
   Defined.
@@ -293,7 +289,7 @@ Section Exercise_2.
       apply isaset_set_fun_space.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         simpl in p, q.
         use funextsec.
@@ -315,7 +311,7 @@ Section Exercise_2.
     : is_univalent pointed_operation_set.
   Proof.
     apply is_univalent_total_category.
-    - Search HSET.
+    - (* Search HSET. *)
       exact is_univalent_HSET.
     - exact pointed_operation_is_univalent_disp.
   Defined.
@@ -399,7 +395,7 @@ Section Exercise_3.
     use total2_paths_f.
     - apply isotoid.
       + apply univalent_category_is_univalent.
-      + exact (iso_Initials aInit bInit).
+      + exact (ziso_Initials aInit bInit).
     - apply proofirrelevance.
       unfold isInitial.
       apply impred_isaprop.
diff --git a/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v b/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v
index 06589a9..ab93cb9 100644
--- a/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v
+++ b/2022-07-Cortona/7_Synthetic-Homotopy-Theory/Synthetic_Homotopy_Theory.v
@@ -8,7 +8,7 @@ https://unimath.github.io/cortona2022/
 
 The goal is to remove as many “Admitted” as possible in the code below.  The exercises should range from straightforward to very challenging.
 
-The exercises are divided into 8 groups, each forming a roughly self-contained story.  In earlier groups, all statements and most definitions are given, only proofs are missing; in later groups, less is given, and more is left for the student.  Apart from the core definitions in group 0, most later groups don’t depend essentially on earlier groups.  
+The exercises are divided into 8 groups, each forming a roughly self-contained story.  In earlier groups, all statements and most definitions are given, only proofs are missing; in later groups, less is given, and more is left for the student.  Apart from the core definitions in group 0, most later groups don’t depend essentially on earlier groups.
 
 The biggest and most interesting part is group 4 — showing the fundamental group of the circle is the integers.  Groups 1–3 can largely be seen as warm-up exercises for this.  Depending on taste, I recommend either tackling the file roughly in order, or jumping straight to group 4 and looking back to earlier exercises as necessary.
 
@@ -22,13 +22,13 @@ A few exercises are marked “off-topic”, when their difficulty is not really
 - Group 5: Being a circle is a proposition
 - Group 6: The recursor is equivalent to the universal mapping property.
 - Group 7: Is the circle’s computation rule necessary?
-- Group 8: Implementing the circle using Z-torsors 
+- Group 8: Implementing the circle using Z-torsors
 
 *)
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.NumberSystems.All.
+Require Import UniMath.NumberSystems.Integers.
 
 
 (** * Auxiliary functions
@@ -56,7 +56,7 @@ Section Circle_Structure.
   Definition circle_rec_structure {S : UU} {b : S} (l : b = b) : UU
   := ∏ (Y : S -> UU) (y_b : Y b) (y_l : transportf _ l y_b = y_b),
      ∑ (f : ∏ x:S, Y x)
-       (e_b : f b = y_b), 
+       (e_b : f b = y_b),
          maponpaths_dep f l
        = maponpaths _ e_b @ y_l @ !e_b.
   (** The third component (the “computation rule” on the loop) is a bit complicated: the idea is just [maponpaths_dep f l = y_l], but that is only well-typed modulo via the “computation rule” for the basepoint, [e_b : f b = y_b]. *)
@@ -86,7 +86,7 @@ Section Circle_Structure.
   Admitted.
 
   (** An alternative formulation of the universal property of the circle:
-  maps out of it correspond to loops. 
+  maps out of it correspond to loops.
 
   “UMP” stands for the “universal mapping property” (a term category theorists love) *)
   Definition circle_ump_structure {S : UU} {b : S} (l : b = b) : UU
@@ -171,7 +171,7 @@ Section Circle_non_trivial.
   Proposition circle_trivial_implies_loops_trivial
     : iscontr S -> ∏ (X:UU) (x:X) (l : x=x), l = idpath x.
   Admitted.
-  
+
   Proposition loops_trivial_implies_isaset {X:UU}
     : (∏ (x:X) (l : x=x), l = idpath x) -> isaset X.
   Admitted.
@@ -218,7 +218,7 @@ Section Fundamental_Group.
 
   (** Outline:
   - (1) the identity-types Id_A(a,x) form the free A-indexed family generated by a single element at a; in particular, Id_S(b,x) are the free S-indexed family generated by an element at b
-  - (2) by univalence, a family over a circle (S,b,l) corresponds to a single type equipped with an auto-equivalence 
+  - (2) by univalence, a family over a circle (S,b,l) corresponds to a single type equipped with an auto-equivalence
   - (3) so Id_S(b,b) is the free type-with-auto-equivalence generated by a single element
   - (4) (Z,succ) is the free type-with-auto-equivalence generated by a single element
   - (5) so they have the same universal peroperty, so are equivalent.
@@ -227,7 +227,7 @@ Section Fundamental_Group.
 
   (** Step (1) is nothing specifically to do with the circle,
   just a particular formulation of the universal property of path-types *)
- 
+
   Section Family_Maps_From_Path_Types.
 
     Context {X:UU} (x0:X).
@@ -247,7 +247,7 @@ Section Fundamental_Group.
 
     Definition auto_type_pr1 : auto_type -> UU := pr1.
     Coercion auto_type_pr1 : auto_type >-> UU.
-    
+
     Definition auto_type_auto { X : auto_type } : X ≃ X
       := pr2 X.
 
@@ -260,7 +260,7 @@ Section Fundamental_Group.
 
     Definition ptd_auto_type_pr1 : ptd_auto_type -> auto_type := pr1.
     Coercion ptd_auto_type_pr1 : ptd_auto_type >-> auto_type.
-    
+
     Definition ptd_auto_type_pt ( X : ptd_auto_type ) : X
       := pr2 X.
 
@@ -272,7 +272,7 @@ Section Fundamental_Group.
   Local Definition s {X : auto_type} := @auto_type_auto X.
   Local Definition pt {X : ptd_auto_type} := @ptd_auto_type_pt X.
 
-  (** We define “freeness” in a category-theoretic style, using a universal mapping property: *) 
+  (** We define “freeness” in a category-theoretic style, using a universal mapping property: *)
   Definition free_ptd_auto_type_ump_structure (X : ptd_auto_type) : UU
   := ∏ (Y : ptd_auto_type),
       iscontr (∑ (f : ∑ (f : X -> Y), f ∘ s = s ∘ f), (pr1 f pt = pt)).
@@ -284,7 +284,7 @@ Section Fundamental_Group.
 
   (* It might be helpful to bundle “ptd-auto-preserving maps” as a structure following how we bundled ptd-auto-types. *)
 
-  (** Step (2): families over circle correspond to types-with-automorphisms. 
+  (** Step (2): families over circle correspond to types-with-automorphisms.
 
   We don’t give a very complete form of this “correspondence” — just as is needed in later steps of the proof. *)
 
@@ -310,7 +310,7 @@ Section Fundamental_Group.
     Definition weq_family_maps_auto_type_maps {X Y : Circle -> UU}
       : (∏ p:Circle, X p -> Y p)
         ≃ (∑ (f : auto_type_of_circle_family X
-                  -> auto_type_of_circle_family Y), 
+                  -> auto_type_of_circle_family Y),
             (f ∘ s = s ∘ f)).
     Proof.
       (* look for library lemmas for building equivalences between dependent sum types,
@@ -319,7 +319,7 @@ Section Fundamental_Group.
 
   End Families_Over_Circle.
 
-  (** Step (3): [ loop = loop ] is a _free_ pointed-type-with-auto-equivalence.  *) 
+  (** Step (3): [ loop = loop ] is a _free_ pointed-type-with-auto-equivalence.  *)
   Section Circle_Loops_Free.
 
     Definition circle_ptd_auto : ptd_auto_type.
@@ -342,7 +342,7 @@ Section Fundamental_Group.
 
   End Circle_Loops_Free.
 
-  (** Step (4): the integers (with successor and zero) are also a free pointed-auto-type. 
+  (** Step (4): the integers (with successor and zero) are also a free pointed-auto-type.
 
   This section involves no homotopy theory — it’s almost entirely old-fashioned set-level mathematics.  The “almost” is because the universal property we want involves mapping into arbitrary _types_, not just sets. *)
 
@@ -365,7 +365,7 @@ Section Fundamental_Group.
 
   End Integers_Free.
 
-  (** Step (5): we’ve shown that the integers and the loop space of the circle are each a “free pointed auto-type”. Now we use that to show they’re equivalent. *) 
+  (** Step (5): we’ve shown that the integers and the loop space of the circle are each a “free pointed auto-type”. Now we use that to show they’re equivalent. *)
   Section Free_Ptd_Auto_Type_Unique.
 
     Definition weq_free_ptd_auto_type_unique
@@ -392,7 +392,7 @@ End Fundamental_Group.
 
 Precisely: for a given type, basepoint, and loop [l], [circle_rec_structure l] is a proposition. *)
 Section Circle_Rec_Structure_Unique.
-  
+
   Context {S : UU} {b : S} (l : b = b).
 
   Definition isaprop_circle_rec_conclusion
@@ -400,7 +400,7 @@ Section Circle_Rec_Structure_Unique.
     -> ∏ (Y : S -> UU) (y_b : Y b) (y_l : transportf _ l y_b = y_b),
       isaprop
       ( ∑ (f : ∏ x:S, Y x)
-        (e_b : f b = y_b), 
+        (e_b : f b = y_b),
           maponpaths_dep f l
         = maponpaths _ e_b @ y_l @ !e_b).
   (* hint: if you attack this directly by hand, it’s quite nasty;
@@ -459,9 +459,9 @@ Section Comp_Rule_Redundant.
 
 End Comp_Rule_Redundant.
 
-(** * Group 8: Implementing the circle using Z-torsors 
+(** * Group 8: Implementing the circle using Z-torsors
 
-The goal of the type is to give an implementation of the circle: we define “Z-torsors”, and show that the type of Z-torsors is a circle. 
+The goal of the type is to give an implementation of the circle: we define “Z-torsors”, and show that the type of Z-torsors is a circle.
 
 The proof is only very roughly outlined — fleshing out the structure of the section is entirely left for the student. *)
 Section Z_torsors.
@@ -481,7 +481,7 @@ Section Z_torsors.
 
   Local Definition loop : base = base.
   Admitted.
-  
+
   Theorem Z_torsors_circle : circle_rec_structure loop.
   Proof.
   (* quite long, and quite mathematically substantial! *)
diff --git a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v
index 6e07cf1..f5cb2a8 100644
--- a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v
+++ b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v
@@ -572,7 +572,7 @@ in UniMath it is very important to be able to search the library so
 that you don't do something someone else has already done. *)
 
 (** To find everything about nat type: *)
-Search nat.
+(* Search nat. *)
 
 (** To search for all lemmas involving the pattern *)
 (* Search _ (_ -> _ -> _). *)
diff --git a/2024-07-Minneapolis/4_Tactics/tactics_lecture.v b/2024-07-Minneapolis/4_Tactics/tactics_lecture.v
index 3e6661c..cce9bc6 100644
--- a/2024-07-Minneapolis/4_Tactics/tactics_lecture.v
+++ b/2024-07-Minneapolis/4_Tactics/tactics_lecture.v
@@ -42,9 +42,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -56,7 +56,7 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -64,7 +64,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -97,7 +97,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -384,7 +384,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern (_ × _ =  _ × _).
+    (* SearchPattern (_ × _ =  _ × _). *)
     (** Nothing for our equation - we can only hope for weak equivalence ≃,
         see the exercises. *)
 Abort.
diff --git a/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v b/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v
index 535e500..2d4e8e8 100644
--- a/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v
+++ b/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v
@@ -49,9 +49,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you only want to find library elements that *yield* booleans, then try *)
-  SearchPattern bool.
+  (* SearchPattern bool. *)
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -65,7 +65,7 @@ Defined.
     verify it and to associate it with the given identifer, here [myfirsttruthvalue].
     This may go wrong for different reasons, including implementation errors of the Coq
     system - that will not affect trustworthiness of the library. *)
-Search bool.
+(* Search bool. *)
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -76,7 +76,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -109,7 +109,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  Search bool.
+  (* Search bool. *)
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -359,9 +359,9 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-SearchPattern (paths _ _).
+(* SearchPattern (paths _ _). *)
 (** Among the search results is [pathsinv0r] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -496,11 +496,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    SearchPattern (_ × _ =  _ × _).
+    (* SearchPattern (_ × _ =  _ × _). *)
     (** Nothing for our equation - we can only hope for weak equivalence ≃. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.
diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
index 6bb77e5..e159212 100644
--- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
+++ b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
@@ -194,7 +194,7 @@ Admitted.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + Search ( (_ = _) ≃ ( _ ≃ _)).
+  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
     (* Solve this goal. *)
     admit.
   + (* Solve this goal. *)
@@ -277,7 +277,7 @@ Proof.
   unfold monoidiso'.
   unfold monoidiso.
   (* Observe that this is just an reassociation of Sigma-types. *)
-  Search ( (∑ _ , _ ) ≃ _ ).
+  (* Search ( (∑ _ , _ ) ≃ _ ). *)
   admit.
 Admitted.
 
diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
index 7b76166..e8a2786 100644
--- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
+++ b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
@@ -217,7 +217,7 @@ Defined.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + Search ( (_ = _) ≃ ( _ ≃ _)).
+  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
     use hSet_univalence.
   + intro p.
     induction X as [X x].
@@ -257,7 +257,7 @@ Local Open Scope multmonoid.
 Notation "x * y" := (op x y) : multmonoid.
 Notation "1" := (unel _) : multmonoid.
 
-Search monoid.
+(* Search monoid. *)
 
 (*
   Construct the following chain of equivalences
diff --git a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory.v b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory.v
index 0164ca1..8398380 100644
--- a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory.v
+++ b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory.v
@@ -12,7 +12,7 @@ Require Import UniMath.CategoryTheory.Core.Univalence.
 Require Import UniMath.CategoryTheory.Core.Functors.
 Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
 Require Import UniMath.CategoryTheory.Core.Isos.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
@@ -85,7 +85,7 @@ Proof.
   intros X Y f.
   apply idpath.
 Qed.
-  
+
 Definition pure : functor_identity SET ⟹ maybe.
 Proof.
   use make_nat_trans.
@@ -213,7 +213,7 @@ Proof.
   - apply X.
   - apply isaproptotal2.
     + intro.
-      apply isaprop_is_iso_disp.
+      apply isaprop_is_z_iso_disp.
     + intros p q r₁ r₂.
       apply X.
 Defined.
diff --git a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v
index 39e5ca6..3ea8714 100644
--- a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v
+++ b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_exercises.v
@@ -6,23 +6,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 Local Open Scope cat.
 
diff --git a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v
index 39561b4..da5ee3f 100644
--- a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v
+++ b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v
@@ -11,23 +11,23 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 Local Open Scope cat.
 
@@ -52,7 +52,7 @@ Section Exercise_0.
     - apply homset_property.
     - intro f.
       apply isasetaprop.
-      apply isaprop_is_iso.
+      apply isaprop_is_z_isomorphism.
   Qed.
 End Exercise_0.
 
@@ -133,13 +133,10 @@ Section Exercise_1.
     set (isaprop_iso := isofhlevelweqf 1 (make_weq idtoiso equiv22) isaprop_id).
     set (zero := stnel (2,0)).
     set (one := stnel (2,1)).
-    set (f := @identity nat_category_data 2).
-    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%Cat).
-    set (fiso := identity_is_iso nat_category 2).
-    assert (giso : is_iso g).
+    set (f := @identity_z_iso nat_category 2).
+    set (g := two_rec one zero : (nat_category_data ⟦ 2, 2 ⟧)%cat).
+    assert (giso : is_inverse_in_precat g g).
     {
-      apply (@is_iso_from_is_z_iso nat_category 2 2).
-      exists g.
       unfold is_inverse_in_precat. split.
       - apply funextfun.
         unfold homot.
@@ -152,15 +149,14 @@ Section Exercise_1.
         + apply idpath.
         + apply idpath.
     }
-    set (f' := make_iso _ fiso).
-    set (g' := @make_iso nat_category 2 2 g giso).
+    set (g' := (@make_z_iso nat_category 2 2 g g giso)).
     set (proofirr_iso := proofirrelevance _ isaprop_iso).
-    set (f'eqg' := proofirr_iso f' g').
+    set (f'eqg' := proofirr_iso f g').
     assert (nonsense : stnel (2,0) = stnel (2,1)).
     {
-      change (stnpr 0) with (f (stnpr 0)).
+      change (stnpr 0) with (z_iso_mor f (stnpr 0)).
       change (stnpr 1) with (g (stnpr 0)).
-      apply (@eqtohomot _ _ f g).
+      apply (@eqtohomot _ _ (z_iso_mor f) g).
       exact (maponpaths pr1 f'eqg').
     }
     apply (negpaths0sx 0).
@@ -271,7 +267,7 @@ Section Exercise_2.
     - apply X.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         apply X.
   Defined.
@@ -293,7 +289,7 @@ Section Exercise_2.
       apply isaset_set_fun_space.
     - apply isaproptotal2.
       + intro.
-        apply isaprop_is_iso_disp.
+        apply isaprop_is_z_iso_disp.
       + intros p q r₁ r₂.
         simpl in p, q.
         use funextsec.
@@ -315,7 +311,7 @@ Section Exercise_2.
     : is_univalent pointed_operation_set.
   Proof.
     apply is_univalent_total_category.
-    - Search HSET.
+    - (* Search HSET. *)
       exact is_univalent_HSET.
     - exact pointed_operation_is_univalent_disp.
   Defined.
@@ -399,7 +395,7 @@ Section Exercise_3.
     use total2_paths_f.
     - apply isotoid.
       + apply univalent_category_is_univalent.
-      + exact (iso_Initials aInit bInit).
+      + exact (ziso_Initials aInit bInit).
     - apply proofirrelevance.
       unfold isInitial.
       apply impred_isaprop.