Make sure that CI succeeds again for the exercises and solutions (and…

… disable Search statements, because of clutter)

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.

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.

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.
 

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.
 

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 _ (_ -> _ -> _). *)

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 :

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.

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.

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.
 

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.
+Defined.