diff --git a/Lecture5.typ b/Lecture5.typ
index f013e95..8fb2643 100644
--- a/Lecture5.typ
+++ b/Lecture5.typ
@@ -130,7 +130,7 @@ This type will have the nice equality property that we want if $MonoidAxioms$ is
 Question: what happens if you just truncate the axioms? \
 Answer: you could only map truncations out into propositions, instead of mapping the axioms out to anything. Also it won't form a category.
 
-#let MonoidM = $bold(M)$
+#let MonoidM = $bold("M")$
 
 *Definition( monoid isomorphism).* between two monoids is an isomorphism of sets $f : MonoidM tilde.equiv MonoidM'$ that sends one unit to other unit and one multiplication to the other.
 
diff --git a/Lecture6.typ b/Lecture6.typ
new file mode 100644
index 0000000..83015ba
--- /dev/null
+++ b/Lecture6.typ
@@ -0,0 +1,143 @@
+#import "prooftree.typ": *
+#import "@preview/showybox:2.0.1": showybox
+#import "@preview/commute:0.2.0": node, arr, commutative-diagram
+#import "@preview/cetz:0.2.2": *
+#set page(width: 5.6in, height: 9in, margin: 0.4in)
+
+#let isofhlevel = $sans("isofhlevel")$
+#let idtoeqv = $sans("idtoeqv")$
+#let idtoiso = $sans("idtoiso")$
+#let Nat = $sans("Nat")$
+#let Vect = $sans("Vect")$
+#let Bool = $sans("Bool")$
+#let carrier = $sans("carrier")$
+#let iseqclass = $sans("iseqclass")$
+#let isInjective = $sans("isInjective")$
+#let Type = $sans("Type")$
+#let reflexive = $sans("reflexive")$
+#let Even = $sans("Even")$
+#let isEven = $sans("isEven")$
+#let Prop = $sans("Prop")$
+#let isProp = $sans("isProp")$
+#let Set = $sans("Set")$
+#let isContr = $sans("isContr")$
+#let isIso = $sans("isIso")$
+#let isEquiv = $sans("isEquiv")$
+#let isSet = $sans("isSet")$
+#let zero = $sans("zero")$
+#let suc = $sans("suc")$
+#let Monoid = $sans("Monoid")$
+#let MonoidStr = $sans("MonoidStr")$
+#let MonoidAxioms = $sans("MonoidAxioms")$
+#let refl = $sans("refl")$
+#let defeq = $equiv$
+#let propeq = $=$
+
+= Category Theory in UniMath
+
+== Introduction
+
+*Definition (precategory).*
+
+This is the most straightforward translation from category into type theory.
+
+#let CC = $cal(C)$
+
+A precategory $CC$ consists of:
+
+- a type $CC_0$ of objects
+- For $x, y : CC_0$ , a type $CC_1 (x, y)$ of morphisms
+- For $x : CC_0$ an identity morphism $id_x : CC_1 (x, x)$
+- For $x,y,z:CC_0$ and $f:CC_1 (x,y) $ and $g : CC_1(y,z)$  a composition $f dot g : CC_1 (x ,z)$
+
+such that
+
+- $f dot id_x propeq f$
+- $id_y dot f propeq f$
+- $f dot (g dot h) propeq (f dot g) dot h$
+
+This is not what you want in a category in UF. This is because there are higher structures on the paths. There's too much structure.
+
+We want the equality of morphisms to be trivial. We can use the notion of sets to re-define this:
+
+*Definition (category).*
+
+- a type $CC_0$ of objects
+- For $x, y : CC_0$ , a *set* $CC_1 (x, y)$ of morphisms
+- For $x : CC_0$ an identity morphism $id_x : CC_1 (x, x)$
+- For $x,y,z:CC_0$ and $f:CC_1 (x,y) $ and $g : CC_1(y,z)$  a composition $f dot g : CC_1 (x ,z)$
+
+Examples of categories:
+
+#let SET = $bold("SET")$
+
+- The category $SET$ of sets and functions
+  - This is a category because we can compose functions and have identity functions
+- Category of pointed sets and point preserving maps
+  - Example of a set with additional structure. A morphism is a function that preserves the structure
+  - Defined: #[
+    Pointed set $(X : Set), (x : X)$. Morphism from $(X, x)$ to $(Y, y)$, give $f : X -> Y$ such that $f(x) equiv y$
+  ]
+- Category of monoids and homomorphisms
+
+== Isomorphisms
+
+We actually want something stronger than morphisms. There are several definitions of isomorphisms.
+
+*Definition.* A morphism $f : CC_1 (x, y)$ is an isomorphism if the map $lambda (g : CC_1 (y,z)).  f dot g$ is an equivalence for every $z : CC_0$
+
+This might seem strange. This is strange because it was developed in a way that it works with precategories. The statement says "precomposition is an equivalence".
+
+The one you might actually want is that you have an inverse map such as both of their compositions is the identity. This is more standard. However, this is only well-behaved if they are sets. Otherwise we can't guarantee there is a unique proof of isomorphism without further coherences.
+
+(UniMath: `z_iso`)
+
+== Univalent categories
+
+*Definition (univalence).* For all types $X, Y$ we have a map $ idtoeqv(X, Y) : X propeq Y -> X tilde.eq Y $
+
+The _univalence axiom_ says that this map is an equivalence.
+
+For categories we can copy-paste this definition.
+
+*Definition (univalent categories).* Let $CC$ be a category. 
+For all objects $x, y$ we have a map $ idtoiso_(x, y) : x propeq y -> x tilde.equiv y $
+
+A category $CC$ is _univalent_ if for all $x, y : CC_0$ the map is an equivalence.
+
+Question: are the two different definitions of a category equivalent? \
+Answer: yes.
+
+We don't have a category of all types. We are restricting ourselves to 1-categories, no interesting structure higher than morphisms.
+
+== Why is this good?
+
+Most important reason is that in category theory, we view objects up to isomorphism. Objects should have the same properties if they are isomorphic.
+
+In set-theoretic foundations, you would have to prove that the properties hold under isomorphism manually. With univalent categories, you would get this for free.
+
+In set theory, uniqueness also means unique up to isomorphism. In univalent categories, this uniqueness becomes "real" uniqueness. We can say things like "the type of initial objects is a proposition".
+
+There's also a semantic aspect. If we just stayed in categories without univalence, we would not get something that corresponds to ...
+
+== $SET$ is univalent
+
+How to prove $SET$ is univalent: we can factor $idtoiso$
+
+#align(center)[#commutative-diagram(
+  node((0,-1),$x propeq y$),
+  node((0,1),$x tilde.equiv y$),
+  node((1,0), $x tilde.eq y$),
+  arr($x propeq y$, $x tilde.equiv y$, $idtoiso_(x,y)$),
+  arr($x propeq y$, $x tilde.eq y$, $tilde.eq$),
+  arr($x tilde.eq y$, $x tilde.equiv y$, $tilde.eq$)
+)]
+
+This way, $idtoiso$ is equal to an equivalence.
+
+In univalence, equivalence is related to isomorphism. This is related to SIP: equality is the same as isomorphism.
+
+Monoids have more complicated structure, so we need something else to help us do the proofs.
+
+== Displayed categories
+
diff --git a/Lol.agda b/Lol.agda
index d21fff4..dc32a92 100644
--- a/Lol.agda
+++ b/Lol.agda
@@ -1,112 +1,7 @@
+open import category-theory.categories
 open import Agda.Primitive
 
-private
-  variable
-    l : Level
+variable
+  l1 l2 : Level
 
-data _≡_ {A : Set l} : A → A → Set l where
-  refl : {x : A} → x ≡ x
-
-data ⊥ : Set where
-data ⊤ : Set where
-  tt : ⊤
-
-result2 : (B : Set) → ((A : Set) → (B → A) → A) → B
-result2 B x = 
-  let
-    y = x B λ x → x
-  in y 
-
-data N : Set where
-  zero : N
-  suc : N -> N
-{-# BUILTIN NATURAL N #-}
-
-data Bool : Set where
-  true : Bool
-  false : Bool
-
-ifbool : {A : Set} (x y : A) -> Bool -> A
-ifbool {A} x y true = x 
-ifbool {A} x y false = y
-
-negbool : Bool -> Bool
-negbool true = false
-negbool false = true
-
-pred : N -> N
-pred zero = zero
-pred (suc x) = x
-
-isZero : N -> Bool
-isZero zero = true
-isZero (suc x) = false
-
-iter : (A : Set) (a : A) (f : A -> A) -> N -> A
-iter A a f zero = a
-iter A a f (suc x) = iter A (f a) f x
-
-_^_ : {A : Set} → (A → A) → N → A → A
-_^_ = λ f n → (λ x → iter _ x f n)
-
-sub : N -> N -> N
-sub x y = (pred ^ y) x
-
-lt1 : N -> N -> Bool
-lt1 m n = negbool (isZero (sub m n))
-
-lt2 : N -> N -> Bool
-lt2 m n = isZero (sub (suc m) n)
-
-postulate
-  funExt : {A : Set} {B : A → Set} {f g : (x : A) → B x}
-    → ((x : A) → f x ≡ g x) → f ≡ g
-
-ap : {A B : Set l} (f : A → B) {x y : A} (p : x ≡ y) → f x ≡ f y
-ap f refl = refl
-
-trans : {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-trans refl refl = refl
-
-module ≡-Reasoning where
-  infix 1 begin_
-  begin_ : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → (x ≡ y)
-  begin x = x
-
-  _≡⟨⟩_ : {l : Level} {A : Set l} (x {y} : A) → x ≡ y → x ≡ y
-  _ ≡⟨⟩ x≡y = x≡y
-
-  infixr 2 _≡⟨⟩_ step-≡
-  step-≡ : {l : Level} {A : Set l} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
-  step-≡ _ y≡z x≡y = trans x≡y y≡z
-  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
-
-  infix 3 _∎
-  _∎ : {l : Level} {A : Set l} (x : A) → (x ≡ x)
-  _ ∎ = refl
-open ≡-Reasoning
-
----
-
-sub-zero-zero : (y : N) -> sub zero y ≡ zero
-sub-zero-zero zero = refl
-sub-zero-zero (suc y) = sub-zero-zero y
-  -- sub zero (suc y) ≡⟨⟩
-  -- (pred ^ (suc y)) zero ≡⟨⟩
-  -- iter _ zero pred (suc y) ≡⟨⟩
-  -- iter _ (pred zero) pred y ≡⟨⟩
-  -- iter _ zero pred y ≡⟨⟩
-  -- (pred ^ y) zero ≡⟨⟩
-  -- sub zero y ≡⟨ sub-zero-zero y ⟩
-  -- zero ∎
-
-f : (x y : N) -> lt1 x y ≡ lt2 x y
-f zero zero = refl
-f zero (suc y) =
-  lt1 zero (suc y) ≡⟨⟩
-  negbool (isZero (sub zero (suc y))) ≡⟨ {!   !} ⟩
-  lt2 zero (suc y) ∎ 
-f (suc x) y = {!   !}
-  
-prop : lt1 ≡ lt2 
-prop = funExt λ x → funExt λ y → f x y
\ No newline at end of file
+thm : (C : Category l1 l2) → {!   !}
\ No newline at end of file
diff --git a/category_theory_exercises.v b/category_theory_exercises.v
new file mode 100644
index 0000000..5ffad4d
--- /dev/null
+++ b/category_theory_exercises.v
@@ -0,0 +1,289 @@
+(* Exercises on Category Theory in UniMath *)
+(* for lecture by Peter LeFanu Lumsdaine, Thu 2017-12-14 *)
+(* School and Workshop on Univalent Maths, Birmingham 2017 *)
+(* https://unimath.github.io/bham2017/ *)
+
+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.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.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Monads.Monads.
+Require Import UniMath.Combinatorics.StandardFiniteSets.
+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!
+
+Skeleton solutions and hints are provided, to exhibit good tools and techniques for working with categories.  However, you may well want to add extra definitions/lemmas besides the ones suggested in the skeleton. *)
+
+Section Exercise_0.
+(** Univalent categories
+
+  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)
+    : isofhlevel 3 (ob C).
+  Proof.
+    unfold isofhlevel. intros x y.
+    unfold is_univalent in H.
+    induction C as [PC HS]. unfold has_homsets in HS.
+    enough (H2 : isaset (x = y)). apply H2.
+    set (eq := idtoiso ,, H x y).
+    apply (isofhlevelweqb 2 eq).
+    apply isofhleveltotal2.
+    { apply HS. }
+    { intros f. apply isofhleveltotal2.
+      { apply HS. }
+      { intros g. apply isofhleveltotal2.
+        { apply isasetaprop. apply HS. }
+        { intros p. apply isasetaprop. apply HS. }
+      }
+    }
+  Defined.
+
+End Exercise_0.
+
+Section Exercise_1.
+(** Non-univalent categories
+
+  Problem: Construct the category with objects the natural numbers, and with maps m->n all functions {1,…,m}->{1,…,n}.  Show that this is a set-category, and that it is NOT univalent.
+
+  Hint: for defining categories (and other large multi-component structures), it’s usually better to define them a few components at a time, following the structure of the definition, as the following skeleton suggests.
+
+  An alternative approach is to go directly for the total structure [Definition nat_category : category], then begin with [use makecategory.] and construct the whole thing in a single interactive proof.  This approach can be good for first finding a proof/construction; but it often causes speed issues down the line, because the resulting term is very large. *)
+
+  Definition nat_category_ob_mor : precategory_ob_mor.
+  Proof.
+    unfold precategory_ob_mor. use tpair.
+    { exact nat. }
+    { simpl. intros x y. exact (stn x -> stn y). }
+  Defined.
+
+  Definition nat_category_data : precategory_data.
+  Proof.
+    unfold precategory_data. use tpair.
+    { unfold precategory_ob_mor. use tpair.
+      { exact nat. }
+      { simpl. intros x y. exact (stn x -> stn y). }
+    }
+    { simpl. unfold precategory_id_comp. use tpair.
+      { intros.   }
+    }
+  Admitted.
+
+  Definition nat_category_is_precategory : is_precategory nat_category_data.
+  Proof.
+  Admitted.
+
+  Definition nat_category : category.
+  Proof.
+  Admitted.
+
+  Definition nat_setcategory : setcategory.
+  Proof.
+  Admitted.
+
+  Proposition nat_category_not_univalent : ¬ (is_univalent nat_category).
+  Proof.
+  Admitted.
+
+End Exercise_1.
+
+Section Exercise_2.
+  (* Exercise 2.1: Define `pointed_disp_cat` with `disp_struct`. *)
+  Definition pointed_disp_cat
+    : disp_cat SET.
+  Proof.
+  Admitted.
+
+  (* Exercise 2.2: Define a displayed category on sets of a binary operation on them.
+     The displayed objects over `X` are maps `X × X → X` and the displayed morphisms over `f` are proofs that `f` preserves the operation.
+   *)
+  Definition operation_disp_cat
+    : disp_cat SET.
+  Proof.
+  Admitted.
+
+  (* Using the product of displayed categories, we now define *)
+  Definition pointed_operation_disp_cat
+    : disp_cat SET.
+  Proof.
+    use dirprod_disp_cat.
+    - exact pointed_disp_cat.
+    - exact operation_disp_cat.
+  Defined.
+
+  (* This gives rise to a total category *)
+  Definition pointed_operation_set
+    : category
+    := total_category pointed_operation_disp_cat.
+
+  (* For convenience, we define some projection to access the structure *)
+  Definition carrier
+             (X : pointed_operation_set)
+    : hSet
+    := pr1 X.
+
+  Definition unit_el
+             (X : pointed_operation_set)
+    : carrier X.
+  Proof.
+  Admitted.
+  (* Once defined, the following should type check. *)
+  (* := pr12 X. *)
+
+  Definition mul
+             (X : pointed_operation_set)
+    : carrier X → carrier X → carrier X.
+  Admitted.
+  (* Once defined, the following should type check. *)
+  (* := λ x y, pr22 X (x ,, y). *)
+
+  (* Exercise 2.3: Define the category of monoid displayed category.
+     Hint: use `disp_full_sub`.
+   *)
+  Definition monoid_laws_disp_cat
+    : disp_cat pointed_operation_set.
+  Proof.
+  Admitted.
+
+  Definition monoids
+    : category
+    := total_category monoid_laws_disp_cat.
+
+  (* During the lecture, we already showed that pointed sets are univalent as follows *)
+  Definition pointed_is_univalent_disp
+    : is_univalent_disp pointed_disp_cat.
+  Proof.
+  Admitted.
+  (* Once everything is in place, the following proof should work. *)
+  (*
+    apply is_univalent_disp_from_fibers.
+    intros X x₁ x₂.
+    use isweqimplimpl.
+    - intros f.
+      apply f.
+    - apply X.
+    - apply isaproptotal2.
+      + intro.
+        apply isaprop_is_iso_disp.
+      + intros p q r₁ r₂.
+        apply X.
+  Defined.
+   *)
+
+  (* Exercise 2.4: Show that each part gives rise to a displayed univalent category and conclude that the total category is univalent.
+     Hint: adapt the proof from the lecture notes.
+   *)
+  Definition operation_is_univalent_disp
+    : is_univalent_disp operation_disp_cat.
+  Proof.
+    apply is_univalent_disp_from_fibers.
+  Admitted.
+
+  (* Now we conclude *)
+  Definition pointed_operation_is_univalent_disp
+    : is_univalent_disp pointed_operation_disp_cat.
+  Proof.
+    use dirprod_disp_cat_is_univalent.
+    - exact pointed_is_univalent_disp.
+    - exact operation_is_univalent_disp.
+  Defined.
+
+  Definition pointed_operation_is_univalent
+    : is_univalent pointed_operation_set.
+  Proof.
+    apply is_univalent_total_category.
+    - exact is_univalent_HSET.
+    - exact pointed_operation_is_univalent_disp.
+  Defined.
+
+  (* Exercise 2.5: conclude that the category of monoids is univalent. *)
+  Definition monoid_is_univalent_disp
+    : is_univalent_disp monoid_laws_disp_cat.
+  Proof.
+  Admitted.
+
+  Definition monoids_is_univalent
+    : is_univalent monoids.
+  Proof.
+    apply is_univalent_total_category.
+    - exact pointed_operation_is_univalent.
+    - exact monoid_is_univalent_disp.
+  Defined.
+End Exercise_2.
+
+
+Section Exercise_3.
+(** Limits and colimits.
+
+  1. Define the empty graph and empty diagram, and show that any limit of the empty diagram is a terminal object in the directly-defined sense.
+*)
+
+  Definition empty_graph : graph.
+  Proof.
+  Admitted.
+
+  Definition empty_diagram (C : category) : diagram empty_graph C.
+  Proof.
+  Admitted.
+
+  Definition isTerminal_limit_of_empty_diagram
+      {C} (L : LimCone (empty_diagram C))
+    : isTerminal _ (lim L).
+  Proof.
+  Admitted.
+
+  (* 2. Show that for a univalent category, “having an initial object” is a property. *)
+  Definition isaprop_initial_obs_of_univalent_category
+      {C : univalent_category}
+    : isaprop (Initial C).
+  Proof.
+  Admitted.
+
+  (* 3. Show that if a category has equalisers and finite products, then it has pullbacks *)
+  Definition pullbacks_from_equalizers_and_products {C : category}
+    : Equalizers C -> BinProducts C -> Pullbacks C.
+  Proof.
+  Admitted.
+
+End Exercise_3.
+
+Section Exercise_4.
+(** Functors and natural transformations / monads and adjunctions
+
+Prove that an adjunction induces a monad.  Construct the Kleisli category of a monad.  Show that the Kleisli construction does not preserve univalence: that is, give an example of a monad on a univalent category whose Kleisli category is not univalent. *)
+
+  (* Hint: as usual, it may be helpful to break out parts of these multi-component structures as separate definitions. *)
+
+  Definition monad_from_adjunction {C D : category}
+      (F : functor C D) (G : functor D C) (A : are_adjoints F G)
+    : Monad C.
+  Proof.
+  Admitted.
+
+  Definition kleisli_cat {C : category} (T : Monad C) : category.
+  Proof.
+    (* see <https://en.wikipedia.org/wiki/Kleisli_category> *)
+  Admitted.
+
+  Theorem kleisli_breaks_univalence
+    : ∑ (C : univalent_category) (T : Monad C), ¬ is_univalent (kleisli_cat T).
+  Proof.
+  Admitted.
+
+End Exercise_4.
diff --git a/set_level_mathematics_exercises.v b/set_level_mathematics_exercises.v
new file mode 100644
index 0000000..90caa23
--- /dev/null
+++ b/set_level_mathematics_exercises.v
@@ -0,0 +1,591 @@
+(** Imports *)
+
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
+Require Import UniMath.Algebra.BinaryOperations.
+Require Import UniMath.Algebra.Monoids.
+
+
+Axiom fill_me : forall {X : UU}, X. (* Remove this line when you are finished. *)
+
+
+
+(** * The type of sets i.e. of types of h-level 2 in [UU] *)
+
+Definition hSet : UU := ∑ X : UU, isaset X.
+Definition hSetpair (X : UU) (i : isaset X) := tpair isaset X i : hSet.
+Definition pr1hSet : hSet -> UU := @pr1 UU (λ X : UU, isaset X).
+Coercion pr1hSet: hSet >-> UU.
+
+Definition setproperty (X : hSet) := pr2 X.
+
+(** * Applications of Hedberg's theorem *)
+
+(** Define a map from [bool] to [UU] that maps
+    [true] to [unit] (the one-element type) and
+    [false] to [empty] (the empty type).
+*)
+Definition bool_to_type : bool -> UU
+  := bool_rect (λ _ : bool, UU) unit empty.
+
+(** Show that there is no path from [true] to [false]. *)
+Theorem no_path_from_true_to_false : true != false.
+Proof.
+  apply fill_me.
+Defined.
+
+(** Show that there is no path from [false] to [true]. *)
+Theorem no_path_from_false_to_true : false != true.
+Proof.
+  apply fill_me.
+Defined.
+
+(** Construct decidable equality on [bool]. *)
+Theorem isdeceqbool : isdeceq bool.
+Proof.
+  unfold isdeceq. intros x' x. induction x.
+  - induction x'.
+    + unfold decidable. apply ii1. auto.
+    + unfold decidable. apply ii2. apply no_path_from_false_to_true.
+  - induction x'.
+    + unfold decidable. apply ii2. apply no_path_from_true_to_false.
+    + unfold decidable. apply ii1. auto.
+Defined.
+
+Check isasetifdeceq.
+
+Theorem isaset_bool : isaset bool.
+Proof.
+  apply isasetifdeceq.
+  apply isdeceqbool.
+Defined.
+
+(** * [nat] is a set *)
+
+(** Define a map from [nat] to [UU] that maps
+    [0] to the singleton type and
+    [S n] to the empty type for any [n].
+*)
+Definition nat_to_type : nat -> UU
+  := nat_rect _ unit (fun _ _ => empty).
+
+Lemma no_path_from_zero_to_successor (x : nat) : 0 != S x.
+Proof.
+  apply fill_me.
+Defined.
+
+Lemma no_path_from_successor_to_zero (x : nat) : S x != 0.
+Proof.
+  apply fill_me.
+Defined.
+
+(** Define a predecessor function on [nat]:
+    [0] is mapped to [0]
+    [S m] is mapped to [m]
+ *)
+Definition predecessor : nat -> nat
+  := nat_rect _ 0 (fun m (r : nat) => m).
+
+Lemma invmaponpathsS (n m : nat) : S n = S m -> n = m.
+Proof.
+  intros.
+  induction n.
+  {
+    induction m.
+    { auto. }
+    {   }
+  }
+Defined.
+
+(** The following constant will be useful for the next lemma. *)
+Check @negf.
+
+Lemma noeqinjS (x x' : nat) : x != x' -> S x != S x'.
+Proof.
+  apply fill_me.
+Defined.
+
+Theorem isdeceqnat : isdeceq nat.
+Proof.
+  apply fill_me.
+Defined.
+
+Lemma isasetnat : isaset nat.
+Proof.
+  apply fill_me.
+Defined.
+
+(** * Functions in sets *)
+
+Definition is_injective {X Y : hSet} (f : X -> Y) : UU
+  := ∏ (x x': X), f x = f x' -> x = x'.
+
+(* This is a useful lemma for checking that dependent function types are propositions or sets *)
+Check impred.
+
+Lemma isaprop_is_injective {X Y : hSet} (f : X -> Y)
+  : isaprop (is_injective f).
+Proof.
+  apply fill_me.
+Defined.
+(** Question: does the above proof need both X and Y to be sets? *)
+
+(** * The universe is not a set *)
+(** The next result requires univalence *)
+
+Require Import UniMath.Foundations.UnivalenceAxiom.
+
+Module universe_is_not_a_set.
+
+  (* We will show that bool has a weak equivalence besides the identity. *)
+
+  Lemma isweq_negb : isweq negb.
+  Proof.
+    use gradth.
+    - exact negb.
+    - intro x. induction x; apply idpath.
+    - intro x; induction x; apply idpath.
+  Defined.
+
+  Definition weq_negb : bool ≃ bool := make_weq negb isweq_negb.
+
+  (* Show that negb is not equal to the identity.
+     It suffices, using toforallpaths, to show that they differ on some element. *)
+  Check toforallpaths.
+
+  Lemma no_path_weq_negb_idweq : weq_negb != idweq bool.
+  Proof.
+    apply fill_me.
+  Defined.
+
+  (* Using Univalence, we can show that if the universe were a set, then
+     negb would have to be equal to the identity. *)
+
+  Definition isaset_UU_gives_path_weq_negb_idweq
+    : isaset UU → weq_negb = idweq bool.
+  Proof.
+    intro H.
+    set (H':= H bool bool).
+    set (T:= invmaponpathsweq (invweq (make_weq _ (univalenceAxiom bool bool)))).
+    apply T.
+    apply H'.
+  Defined.
+
+  Definition not_isaset_UU : ¬ isaset UU.
+  Proof.
+    apply fill_me.
+  Defined.
+
+End universe_is_not_a_set.
+
+
+
+
+
+Section Pointed.
+
+Definition ptdset : UU := ∑ A : hSet, A.
+Coercion ptdset_to_set (X : ptdset) : hSet := pr1 X.
+Definition ptd (X : ptdset) : X := pr2 X.
+Definition ptdset_iso (X Y : ptdset) : UU := ∑ f : X ≃ Y, f (ptd X) = ptd Y.
+
+Definition id_weq (X Y : ptdset) : (X = Y) ≃ (X ╝ Y).
+Proof.
+  admit.
+  (* replace tactic "admit." by a real construction *)
+Admitted.
+(* Once the goals are solved, replace "Admitted" by "Defined" *)
+(* Defined. *)
+
+Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
+Proof.
+  use weqtotal2.
+  + Search ( (_ = _) ≃ ( _ ≃ _)).
+    (* Solve this goal. *)
+    admit.
+  + (* Solve this goal. *)
+    admit.
+Admitted.
+(* Once the goals are solved, replace "Admitted" by "Defined" *)
+(* Defined. *)
+
+Definition sip_for_ptdset : ∏ (X Y : ptdset), (X = Y) ≃ ptdset_iso X Y.
+Proof.
+  intros X Y.
+  eapply weqcomp.
+  - admit. (* use the construction above *)
+  - admit. (* use the construction above *)
+Admitted.
+(* Once the goals are solved, replace "Admitted" by "Defined" *)
+(* Defined. *)
+
+Definition transportf_ptdset :
+  ∏ (P : ptdset → UU) (X Y : ptdset), ptdset_iso X Y → P X → P Y.
+Proof.
+  admit.
+Admitted.
+
+
+End Pointed.
+
+
+
+Section Monoid.
+
+Local Open Scope multmonoid.
+
+Notation "x * y" := (op x y) : multmonoid.
+Notation "1" := (unel _) : multmonoid.
+
+(**
+
+The goal is to show the univalence principle (aka structure identity principle)
+for monoids:
+for monoids X and Y,
+ (X = Y) ≃ (monoidiso X Y)
+
+
+   The idea here is to use the following composition
+
+                           (X = Y) ≃ (X ╝ Y)
+                                   ≃ (monoidiso' X Y)
+                                   ≃ (monoidiso X Y).
+
+   The reason why we use monoidiso' is that then we can use univalence for sets with binops,
+   [setwithbinop_univalence]. See [monoid_univalence_weq2].
+ *)
+
+
+Definition monoidiso' (X Y : monoid) : UU :=
+  ∑ g : (∑ f : X ≃ Y, isbinopfun f), (pr1 g) 1 = 1.
+
+Definition monoid_univalence_weq1 (X Y : monoid) : (X = Y) ≃ (X ╝ Y).
+Proof.
+  admit.
+  (* Hint: use your search skills. *)
+Admitted.
+
+Definition monoid_univalence_weq2 (X Y : monoid) : (X ╝ Y) ≃ (monoidiso' X Y).
+Proof.
+  use weqbandf.
+  - admit.
+    (* Hint: use "exact foo." where you find a suitable foo using the search function. *)
+  - intros e. cbn. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e.
+    cbn. induction e. use weqimplimpl.
+    + intros i. use proofirrelevance. use isapropismonoidop.
+    + intros i. admit.
+    + admit.
+    + admit.
+Admitted.
+
+Definition monoid_univalence_weq3 (X Y : monoid) : (monoidiso' X Y) ≃ (monoidiso X Y).
+Proof.
+  unfold monoidiso'.
+  unfold monoidiso.
+  (* Observe that this is just an reassociation of Sigma-types. *)
+  Search ( (∑ _ , _ ) ≃ _ ).
+  admit.
+Admitted.
+
+
+Definition monoid_univalence_map (X Y : monoid) : X = Y → monoidiso X Y.
+Proof.
+  admit.
+Admitted.
+
+Lemma monoid_univalence_isweq (X Y : monoid) :
+  isweq (monoid_univalence_map X Y).
+Proof.
+  use isweqhomot.
+  - exact (weqcomp (monoid_univalence_weq1 X Y)
+                   (weqcomp (monoid_univalence_weq2 X Y) (monoid_univalence_weq3 X Y))).
+  - intros e. induction e.
+    refine (weqcomp_to_funcomp_app @ _).
+    admit.
+    (* use weqcomp_to_funcomp_app. *)
+  - use weqproperty.
+Admitted.
+
+
+Definition monoid_univalence (X Y : monoid) : (X = Y) ≃ (monoidiso X Y)
+  := make_weq
+    (monoid_univalence_map X Y)
+    (monoid_univalence_isweq X Y).
+
+End Monoid.
+
+
+
+
+
+
+
+
+
+
+
+
+(** * Relations *)
+
+(** ** Definitions *)
+
+Definition hrel (X : UU) : UU := X -> X -> hProp.
+
+Definition isrefl {X : UU} (R : hrel X) : UU
+  := ∏ x : X, R x x.
+Definition istrans {X : UU} (R : hrel X) : UU := fill_me.
+Definition issymm {X : UU} (R : hrel X) : UU := fill_me.
+
+Definition ispreorder {X : UU} (R : hrel X) : UU := istrans R × isrefl R.
+
+Definition iseqrel {X : UU} (R : hrel X) : UU := ispreorder R × issymm R.
+
+Definition iseqrelconstr {X : UU} {R : hrel X}
+           (trans0 : istrans R)
+           (refl0 : isrefl R)
+           (symm0 : issymm R)
+  : iseqrel R
+  := make_dirprod (make_dirprod trans0 refl0) symm0.
+
+(** ** Eqivalence relations *)
+
+Definition eqrel (X : UU) : UU
+  := ∑ R : hrel X, iseqrel R.
+Definition eqrelpair {X : UU} (R : hrel X) (is : iseqrel R)
+  : eqrel X
+  := tpair (λ R : hrel X, iseqrel R) R is.
+Definition eqrelconstr {X : UU} (R : hrel X)
+           (is1 : istrans R) (is2 : isrefl R) (is3 : issymm R) : eqrel X
+  := eqrelpair R (make_dirprod (make_dirprod is1 is2) is3).
+
+Definition pr1eqrel (X : UU) : eqrel X -> (X -> (X -> hProp)) := @pr1 _ _.
+Coercion pr1eqrel : eqrel >-> Funclass.
+
+Definition eqreltrans {X : UU} (R : eqrel X) : istrans R := pr1 (pr1 (pr2 R)).
+Definition eqrelrefl {X : UU} (R : eqrel X) : isrefl R := pr2 (pr1 (pr2 R)).
+Definition eqrelsymm {X : UU} (R : eqrel X) : issymm R := pr2 (pr2 R).
+
+(** * The type of subtypes of a given type *)
+
+Definition hsubtype (X : UU) : UU := X -> hProp.
+
+(** The carrier of a subtype *)
+Definition carrier {X : UU} (A : hsubtype X) : UU := ∑ x : X, A x.
+
+Check isasethProp.
+Check (impred 2).
+
+Lemma isasethsubtype (X : UU) : isaset (hsubtype X).
+Proof.
+  apply fill_me.
+Defined.
+
+(** ** A subtype with paths between any two elements is an [hProp]. *)
+
+Lemma isapropsubtype {X : UU} (A : hsubtype X)
+      (is : ∏ (x1 x2 : X), A x1 -> A x2 -> x1 = x2)
+  : isaprop (carrier A).
+Proof.
+  apply invproofirrelevance.
+  intros x x'.
+  assert (X0 : isincl (@pr1 _ A)).
+  {
+    apply isinclpr1.
+    intro x0.
+    apply (pr2 (A x0)).
+  }
+  apply (invmaponpathsincl (@pr1 _ A) X0).
+  induction x as [ x0 is0 ].
+  induction x' as [ x0' is0' ].
+  simpl.
+  apply (is x0 x0' is0 is0').
+Defined.
+
+(** ** Equivalence classes with respect to a given relation *)
+
+Definition iseqclass {X : UU} (R : hrel X) (A : hsubtype X) : UU
+  :=
+    ∥ carrier A ∥ (* is non-empty *)
+      ×
+      ((∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2)
+         ×
+         (∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2)).
+
+Definition iseqclassconstr {X : UU} (R : hrel X) {A : hsubtype X}
+           (ax0 : ishinh (carrier A))
+           (ax1 : ∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2)
+           (ax2 : ∏ x1 x2 : X, A x1 ->  A x2 -> R x1 x2)
+  : iseqclass R A
+  := make_dirprod ax0 (make_dirprod ax1 ax2).
+
+Definition eqax0 {X : UU} {R : hrel X} {A : hsubtype X}
+  : iseqclass R A -> ishinh (carrier A)
+  := λ is : iseqclass R A, pr1 is.
+Definition eqax1 {X : UU} {R : hrel X} {A : hsubtype X}
+  : iseqclass R A -> ∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2
+  := λ is : iseqclass R A, pr1 (pr2 is).
+Definition eqax2 {X : UU} {R : hrel X} {A : hsubtype X}
+  : iseqclass R A -> ∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2
+  := λ is : iseqclass R A, pr2 (pr2 is).
+
+Lemma isapropiseqclass {X : UU} (R : hrel X) (A : hsubtype X)
+  : isaprop (iseqclass R A).
+Proof.
+  apply isofhleveldirprod.
+  - apply propproperty.
+  - apply fill_me.
+Defined.
+
+(** ** Setquotient defined in terms of equivalence classes *)
+
+Definition setquot {X : UU} (R : hrel X) : UU
+  := ∑ A : hsubtype X, iseqclass R A.
+
+Definition setquotpair {X : UU} (R : hrel X) (A : hsubtype X)
+           (is : iseqclass R A)
+  : setquot R
+  := A ,, is.
+
+Definition pr1setquot {X : UU} (R : hrel X)
+  : setquot R -> hsubtype X
+  := @pr1 _ (λ A : _, iseqclass R A).
+Coercion pr1setquot : setquot >-> hsubtype.
+
+Lemma isinclpr1setquot {X : UU} (R : hrel X) : isincl (pr1setquot R).
+Proof.
+  apply isinclpr1.
+  intro x0.
+  apply isapropiseqclass.
+Defined.
+
+Definition setquottouu0 {X : UU} (R : hrel X) (a : setquot R)
+  := carrier (pr1 a).
+Coercion setquottouu0 : setquot >-> UU.
+
+Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R).
+Proof.
+  apply (isasetsubset (@pr1 _ _) (isasethsubtype X)).
+  apply isinclpr1setquot.
+Defined.
+
+Theorem setquotpr {X : UU} (R : eqrel X) : X -> setquot R.
+Proof.
+  intro x.
+  set (rax := eqrelrefl R).
+  set (sax := eqrelsymm R).
+  set (tax := eqreltrans R).
+  apply (tpair _ (λ x0 : X, R x x0)).
+  split.
+  - exact (hinhpr (tpair _ x (rax x))).
+  - split; intros x1 x2 X1 X2.
+    + exact fill_me.
+    + exact fill_me.
+Defined.
+
+Lemma setquotl0 {X : UU} (R : eqrel X) (c : setquot R) (x : c) :
+  setquotpr R (pr1 x) = c.
+Proof.
+  Set Printing Coercions.
+  apply (invmaponpathsincl _ (isinclpr1setquot R)).
+  Unset Printing Coercions.
+  apply funextsec; intro x0.
+  apply hPropUnivalence; intro r.
+  - exact fill_me.
+  - exact fill_me.
+Defined.
+
+Theorem issurjsetquotpr {X : UU} (R : eqrel X) : issurjective (setquotpr R).
+Proof.
+  unfold issurjective.
+  intro c. apply (@hinhuniv (carrier c)).
+  - intro x. apply hinhpr.
+    use tpair.
+    + exact (pr1 x).
+    + apply setquotl0.
+  - apply (eqax0 (pr2 c)).
+Defined.
+
+Lemma iscompsetquotpr {X : UU} (R : eqrel X) (x x' : X)
+  : R x x' -> setquotpr R x = setquotpr R x'.
+Proof.
+  intro r.
+  Set Printing Coercions.
+  apply (invmaponpathsincl _ (isinclpr1setquot R)).
+  Unset Printing Coercions.
+  simpl. apply funextsec.
+  intro x0. apply hPropUnivalence.
+  - intro r0. exact fill_me.
+  - intro x0'. exact fill_me.
+Defined.
+
+(** *** Universal property of [seqtquot R] for functions to sets satisfying compatibility condition [iscomprelfun] *)
+
+Definition iscomprelfun {X Y : UU} (R : hrel X) (f : X -> Y) : UU
+  := ∏ x x' : X, R x x' -> f x = f x'.
+
+Lemma isapropimeqclass {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y)
+      (is : iscomprelfun R f) (c : setquot R) :
+  isaprop (image (λ x : c, f (pr1 x))).
+Proof.
+  apply isapropsubtype.
+  intros y1 y2. simpl.
+  apply (@hinhuniv2 _ _ (make_hProp (y1 = y2) (pr2 Y y1 y2))).
+  intros x1 x2. simpl.
+  destruct c as [ A iseq ].
+  destruct x1 as [ x1 is1 ]. destruct x2 as [ x2 is2 ].
+  destruct x1 as [ x1 is1' ]. destruct x2 as [ x2 is2' ].
+  simpl in is1. simpl in is2. simpl in is1'. simpl in is2'.
+  assert (r : R x1 x2) by apply (eqax2 iseq _ _ is1' is2').
+  apply ( !is1 @  (is _ _ r) @ is2).
+Defined.
+
+Definition setquotuniv {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y)
+        (is : iscomprelfun R f) (c : setquot R) : Y.
+Proof.
+  apply (pr1image (λ x : c, f (pr1 x))).
+  apply (@squash_to_prop (carrier c)).
+  - apply (eqax0 (pr2 c)).
+  - apply isapropimeqclass. apply is.
+  - unfold carrier. apply prtoimage.
+Defined.
+
+(** Note : the axioms rax, sax and trans are not used in the proof of
+  setquotuniv. If we consider a relation which is not an equivalence relation
+  then setquot will still be the set of subsets which are equivalence classes.
+  Now however such subsets need not to cover all of the type. In fact their set
+  can be empty. Nevertheless setquotuniv will apply. *)
+
+Theorem setquotunivcomm {X : UU} (R : eqrel X) (Y : hSet) (f : X -> Y)
+        (is : iscomprelfun R f) :
+  ∏ x : X, setquotuniv R Y f is (setquotpr R x) = f x.
+Proof.
+  intros.
+  apply idpath.
+Defined.
+
+Lemma setquotpr_eq_eqrel {X : UU} (R : eqrel X) (x x' : X)
+  : setquotpr R x = setquotpr R x' → R x x'.
+Proof.
+  intro e.
+  set (e' := maponpaths (pr1setquot R) e). simpl in e'.
+  set (e'' := maponpaths (λ f : _, f x') e'). simpl in e''.
+  rewrite e''.
+  apply eqrelrefl.
+Defined.
+
+Theorem weqpathsinsetquot {X : UU} (R : eqrel X) (x x' : X) :
+  R x x' ≃ setquotpr R x = setquotpr R x'.
+Proof.
+  intros.
+  exists (iscompsetquotpr R x x').
+  apply isweqimplimpl.
+  - intro e.
+    set (e' := maponpaths (pr1setquot R) e). simpl in e'.
+    set (e'' := maponpaths (λ f : _, f x') e'). simpl in e''.
+    rewrite e''.
+    apply eqrelrefl.
+  - apply propproperty.
+  - apply isasetsetquot.
+Defined.
+
+(* End of file *)
diff --git a/tactics_lecture_extended.v b/tactics_lecture_extended.v
new file mode 100644
index 0000000..535e500
--- /dev/null
+++ b/tactics_lecture_extended.v
@@ -0,0 +1,1008 @@
+(** * Lecture 4: Tactics in UniMath *)
+(** based on material prepared by Ralph Matthes *)
+
+(** This is the extended version of a presentation at the
+    School on Univalent Mathematics 2024 in Cortona, meant for self-study
+    and for exploring the UniMath library.
+*)
+
+
+(** Compiles with the command
+[[
+coqc -type-in-type tactics_lecture_extended.v
+]]
+when Coq is set up according to the instructions for this school and the associated coqc executable
+has priority in the path. However, you do not need to compile this file. The option is crucial, and
+also your own developments will need the Coq options configured through the installation instructions,
+most notably the present one. *)
+
+(** Can be transformed into HTML documentation with the command
+[[
+coqdoc -utf8 tactics_lecture_extended.v
+]]
+    (If internal links in the generated lecture_tactics_long_version.html are desired,
+     compilation with coqc is needed.)
+*)
+
+(** In Coq, one can define concepts by directly giving well-typed
+    terms (see Part 2), but one can also be helped in the construction by the
+    interactive mode.
+*)
+
+Require Import UniMath.Foundations.Preamble.
+(* Require Import UniMath.CategoryTheory.All. *)
+
+(** ** define a concept interactively: *)
+
+Locate bool.  (** a separate definition - [Init.Datatypes.bool] is in the Coq library,
+                  not available for UniMath *)
+
+Definition myfirsttruthvalue: bool.
+  (** only the identifier and its type given, not the definiens *)
+
+  (** This opens the interactive mode.
+
+      The #<a href="https://github.com/UniMath/UniMath/tree/master/UniMath/README.md##unimath-coding-style">#UniMath
+      style guide#</a># asks us to start what follows with [Proof.] in a separate line.
+      In vanilla Coq, this would be optional (it is anyway a "nop"). *)
+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.
+  (** If you only want to find library elements that *yield* booleans, then try *)
+  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
+      finish the current goal with that term. *)
+
+  (** We see in the response buffer: "No more subgoals."
+      Hence, there is nothing more to do, except for leaving the proof mode properly. *)
+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].
+    This may go wrong for different reasons, including implementation errors of the Coq
+    system - that will not affect trustworthiness of the library. *)
+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 *)
+
+(** [myfirsttruthvalue relies on an unsafe universe hierarchy] is output to indicate
+    that we are using Coq with option [-type-in-type]. *)
+
+(** *** a more compelling example *)
+Definition mysecondtruthvalue: bool.
+Proof.
+  Search bool.
+  apply negb.
+  (** applies the function [negb] to obtain the required boolean,
+      thus the system has to ask for its argument *)
+  exact myfirsttruthvalue.
+Defined.
+
+Print mysecondtruthvalue.
+(**
+[[
+mysecondtruthvalue = negb myfirsttruthvalue
+     : bool
+]]
+*)
+
+(** the definition is "as is", evaluation can be done subsequently: *)
+Eval compute in mysecondtruthvalue.
+(**
+[[
+     = false
+     : bool
+]]
+*)
+
+(** Again, not much has been gained by the interactive mode. *)
+
+(** Here, we see a copy of the definition from the Coq library: *)
+Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
+(** only for illustration purposes - it would be better to define
+    it according to UniMath style *)
+
+Definition mythirdtruthvalue: bool.
+Proof.
+  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. *)
+
+  (** This follows the proof pattern of "backward chaining" that tries to
+      attack goals instead of building up evidence. In the course of action,
+      more goals can be generated. The proof effort is over when no more
+      goal remains. *)
+
+  (** UniMath coding style asks you to use proof structuring syntax,
+      while vanilla Coq would allow you to write formally verified
+      "spaghetti code". *)
+
+  (** We tell Coq that we start working on the first subgoal. *)
+  -
+    (** only the "focused" subgoal is now on display *)
+    apply andb.
+    (** this again spawns two subgoals *)
+
+    (** we tell Coq that we start working on the first subgoal *)
+    +
+      (** normally, one would not leave the "bullet symbol" isolated in a line *)
+      exact mysecondtruthvalue.
+    + exact myfirsttruthvalue.
+      (** The response buffer signals:
+[[
+There are unfocused goals.
+]]
+          ProofGeneral would give more precise instructions as how to proceed.
+          But we know what we are doing...
+       *)
+  - exact true.
+Defined.
+
+(** The usual "UniMath bullet order" is -, +, *, --, ++, **, ---, +++, ***,
+    and so on (all the ones shown are being used).
+
+    Coq does not impose any order, so one can start with, e.g., *****,
+    if need be for the sake of experimenting with a proof.
+
+    Reuse of bullets even on one branch is possible by enclosing subproofs
+    in curly braces {}.
+*)
+
+Print mythirdtruthvalue.
+Eval compute in mythirdtruthvalue.
+
+(** You only saw the tactics [exact] and [apply] at work, and there was no context. *)
+
+(** ** doing Curry-Howard logic *)
+
+(** Interactive mode is more wide-spread when it comes to carrying out proofs
+    (the command [Proof.] is reminiscent of that). *)
+
+(** Disclaimer: this section has a logical flavour, but the "connectives"
+    are not confined to the world of propositional or predicate logic.
+    In particular, there is no reference to the sort Prop of Coq.
+    Prop is not used at all in UniMath!
+
+    On first reading, it is useful to focus on the logical meaning. *)
+
+
+Locate "->". (** non-dependent product, can be seen as implication *)
+Locate "∅".
+Print empty. (** an inductive type that has no constructor *)
+Locate "¬". (** we need to refer to the UniMath library more explicitly *)
+
+Require Import UniMath.Foundations.PartA.
+(** Do not write the import statements in the middle of a vernacular file.
+    Here, it is done to show the order of appearance, but this is only for
+    reasons of pedagogy.
+*)
+
+Locate "¬".
+Print neg.
+(** Negation is not a native concept; it is reduced to implication,
+    as is usual in constructive logic. *)
+
+Locate "×".
+Print dirprod.  (** non-dependent sum, can be seen as conjunction *)
+
+Definition combinatorS (A B C: UU): (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  (** how to infer an implication? *)
+  intro Hyp123.
+  set (Hyp1 := pr1 Hyp123).
+  (** This is already a bit of "forward chaining" which is a fact-building process. *)
+  set (Hyp23 := pr2 Hyp123).
+  cbn in Hyp23.
+  (** [cbn] simplifies a goal, and [cbn in H] does this for hypothesis [H];
+      note that [simpl] has the same high-level description but should better
+      be avoided in new developments.  *)
+  set (Hyp2 := pr1 Hyp23).
+  set (Hyp3 := pr2 Hyp23).
+  cbn in Hyp3.
+  apply Hyp1.
+  apply tpair. (** could be done with [split.] as well *)
+  - assumption. (** instruct Coq to look into the current context *)
+
+                (** this could be done with [exact Hyp3.] as well *)
+  - apply Hyp2.
+    assumption.
+Defined.
+
+Print combinatorS.
+Eval compute in combinatorS.
+
+Local Definition combinatorS_intro_pattern (A B C: UU):
+  (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  intros [Hyp1 [Hyp2 Hyp3]]. (** deconstruct the hypothesis at the time of introduction;
+                                 notice that [×] associates to the right;
+                                 [intros] can also introduce multiple hypotheses, see below *)
+  apply Hyp1.
+  split.
+  - assumption.
+  - apply Hyp2.
+    assumption.
+Defined.
+
+Print combinatorS_intro_pattern.
+
+(** the two definitions are even convertible: *)
+Eval compute in combinatorS_intro_pattern.
+
+Local Lemma combinatorS_intro_pattern_is_the_same:
+  combinatorS = combinatorS_intro_pattern.
+Proof.
+  apply idpath.
+Defined.
+
+(** In late 2017, [combinatorS_intro_pattern] would have contained [match] constructs,
+    but now, the introduction patterns use less overhead when possible. The UniMath
+    style guide still does not want them to be used with square brackets. *)
+
+(** another style to make life easier: *)
+Local Definition combinatorS_destruct (A B C: UU):
+  (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  intro Hyp123.
+  destruct Hyp123 as [Hyp1 Hyp23]. (** deconstruct the hypothesis when needed *)
+  apply Hyp1.
+  destruct Hyp23 as [Hyp2 Hyp3]. (** deconstruct the hypothesis when needed *)
+  split.
+  - assumption.
+  - apply Hyp2.
+    assumption.
+Defined.
+
+Print combinatorS_destruct.
+
+(** Again, the definition is definitionally equal to the first one: *)
+Eval compute in combinatorS_destruct.
+
+Local Lemma combinatorS_destruct_is_the_same: combinatorS = combinatorS_destruct.
+Proof.
+  apply idpath.
+Defined.
+
+(** In late 2017, [combinatorS_destruct] would also have contained [match] constructs,
+    which is why [destruct] is forbidden in the UniMath style guide. Now, this is fine
+    in our example. *)
+
+(** The (hitherto) preferred idiom: *)
+Definition combinatorS_induction (A B C: UU): (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  intro Hyp123.
+  induction Hyp123 as [Hyp1 Hyp23].
+  apply Hyp1.
+  induction Hyp23 as [Hyp2 Hyp3].
+  split.
+  - assumption.
+  - apply Hyp2.
+    assumption.
+Defined.
+
+Print combinatorS_induction.
+Eval compute in combinatorS_induction.
+(** the comfort for the user does not change the normal form of the constructed proof *)
+
+Definition combinatorS_curried (A B C: UU): (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  (** use [intro] three times or rather [intros] once; reasonable coding style
+      gives names to all hypotheses that are not already present
+      in the goal formula, see also the next definition *)
+  intros H1 H2 H3.
+  apply H1.
+  - assumption.
+  - set (proofofB := H2 H3).
+    (** set up abbreviations that can make use of the current context;
+        will be considered as an extra element of the context: *)
+    assumption.
+Defined.
+
+Print combinatorS_curried.
+(** We see that [set] gives rise to [let]-expressions that are known
+    from functional programming languages, in other words: the use of
+    [set] is not a "macro" facility to ease typing. *)
+
+(** [let]-bindings disappear when computing the normal form of a term: *)
+Eval compute in combinatorS_curried.
+
+(** [set] can only be used if the term of the desired type is provided,
+    but we can also work interactively as follows: *)
+Definition combinatorS_curried_with_assert (A B C: UU):
+  (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  intros H1 H2 H3.
+  (** we can momentarily forget about our goal and build up knowledge: *)
+  assert (proofofB : B).
+  (** the current goal [C] becomes the second sub-goal, and the new current goal is [B] *)
+
+  (** It is not wise to handle this situation by "bullets" since many assertions
+      can appear in a linearly thought argument. It would pretend a tree structure
+      although it would rather be a comb. The proof of the assertion should
+      be packaged by enclosing it in curly braces like so: *)
+  { apply H2.
+    assumption.
+  }
+  (** Now, [proofofB] is in the context with type [B]. *)
+  apply H1.
+  - assumption.
+  - assumption.
+Defined.
+
+(** the wildcard [?] for [intros] *)
+Definition combinatorS_curried_variant (A B C: UU):
+  (A -> B -> C) -> (A -> B) -> forall H7: A, C.
+Proof.
+  intros H1 H2 ?.
+(** a question mark instructs Coq to use the corresponding identifier
+    from the goal formula *)
+  exact (H1 H7 (H2 H7)).
+Defined.
+(** the wildcard [_] for [intros] forgets the respective hypothesis *)
+
+Locate "⨿". (** this symbol is typed as \amalg when the recommended extension
+                packages for VSCode are loaded *)
+Print coprod. (** defined in UniMath preamble as inductive type,
+  can be seen as disjunction *)
+
+Locate "∏".
+
+Locate "=". (** the identity type of UniMath *)
+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 _ _).
+(** Among the search results is [pathsinv0r] that has [idpath] in its conclusion. *)
+SearchRewrite idpath.
+(** No result! *)
+
+(** *** How to decompose formulas *)
+
+(** In "Coq in a Hurry", Yves Bertot gives recipes for decomposing the usual logical
+    connectives. Crucially, one has to distinguish between decomposition of the goal
+    or decomposition of a hypothesis in the context.
+
+    Here, we do it alike.
+*)
+
+(** **** Decomposition of goal formulas:
+
+    A1,...,An -> B: tactic [intro] or [intros]
+
+    [¬ A]: idem (negation is defined through implication)
+
+    Π-type: idem (implication is a special case of product)
+
+    [×]: [apply dirprodpair], less specifically [apply tpair] or [split]
+
+    Σ-type: [use tpair] or [exists] or [split with], see explanations below
+
+    [A ⨿ B]: [apply ii1] or [apply ii2], but this constitutes a choice
+             of which way to go
+
+    [A = B]: [apply idpath], however this only works when the expressions
+             are convertible
+
+    [nat]: [exact 1000], for example (a logical reading is not
+         useful for this type); beware that UniMath knows only 27 numerals,
+         [Goal nat. Fail exact 2022.] leads to
+[[
+The command has indeed failed with message: No interpretation for number "2022".
+]]
+*)
+
+(** **** Decomposition of formula of hypothesis [H]:
+
+    [∅]: [induction H]
+
+         This terminates a goal. (It corresponds to ex falso quodlibet.)
+
+         There is naturally no recipe for getting rid of [∅] in the conclusion.
+         But [apply fromempty] allows to replace any goal by [∅].
+
+    A1,...,An -> B: [apply H], but the formula has to fit with the goal
+
+
+    [×]: [induction H as [H1 H2]]
+
+         As seen above, this introduces names of hypotheses for the two components.
+
+    Σ-type: idem, but rather more asymmetric as [induction H as [x H']]
+
+    [A ⨿ B]: [induction H as [H1 | H2]]
+
+              This introduces names for the hypotheses in the two branches.
+
+    [A = B]: [induction H]
+
+             The supposedly equal [A] and [B] become the same [A] in the goal.
+
+             This is the least intuitive rule for the non-expert in type theory.
+
+    [nat]: [induction n as [ | n IH]]
+
+           Here, we assume that the hypothesis has the name [n] which
+           is more idiomatic than [H], and there is no extra name in
+           the base case, while in the step case, the preceding number
+           is now given the name [n] and the induction hypothesis is
+           named [IH].
+*)
+
+(** ** Handling unfinished proofs *)
+
+(** In the middle of a proof effort - not in the UniMath library - you can use
+    [admit] to abandon the current goal. *)
+Local Lemma badex1 (A: UU): ∅ × (A -> A).
+Proof.
+  split.
+  - (** seems difficult in the current context *)
+    admit.
+
+    (** we continue with decent proof work: *)
+  - intro H.
+    assumption.
+Admitted.
+
+(** This is strictly forbidden to commit to UniMath! [admit] allows to pursue the other goals,
+    while [Admitted.] makes the lemma available for further proofs. A warning is shown that
+    [badex1] has been assumed as axiom. *)
+
+(** An alternative to interrupt work on a proof: *)
+Lemma badex2 (A: UU): ∅ × (A -> A).
+Proof.
+  split.
+  -
+Abort.
+(** [badex2] is not in the symbol table. *)
+
+(** [Abort.] is a way of documenting a problem with proving a result.
+    At least, Coq can check the partial proof up to the [Abort.] command. *)
+
+(** ** Working with holes in proofs *)
+
+(** Our previous proofs were particularly clear because the goal formulas
+    and all hypotheses were fully given by the system.
+*)
+
+Print pathscomp0.
+(** This is the UniMath proof of transitivity of equality. *)
+
+(** The salient feature of transitivity is that the intermediate
+    expression cannot be deduced from the equation to be proven. *)
+Lemma badex3 (A B C D: UU) : ((A × B) × (C × D)) = (A × (B × C) × D).
+(** Notice that the outermost parentheses are needed here. *)
+Proof.
+  Fail apply pathscomp0.
+(**
+[[
+The command has indeed failed with message:
+Cannot infer the implicit parameter b of pathscomp0 whose type is
+"Type" in environment:
+A, B, C, D : UU
+]]
+
+[Fail] announces failure and therefore allows to continue with
+the interpretation of the vernacular file.
+
+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 (_ × _ =  _ × _).
+    (** Nothing for our equation - we can only hope for weak equivalence ≃. *)
+Abort.
+
+SearchPattern(_ ≃ _).
+Print weqcomp.
+Print weqdirprodasstor.
+Print weqdirprodasstol.
+Print weqdirprodf.
+Print idweq.
+
+Lemma assocex (A B C D: UU) : ((A × B) × (C × D)) ≃ (A × (B × C) × D).
+Proof.
+  Fail apply weqcomp.
+  eapply weqcomp.
+(** [eapply] generates "existential variables" for the expressions
+    it cannot infer from applying a lemma.
+
+    The further proof will narrow on those variables and finally
+    make them disappear - otherwise, the proof is not considered
+    completed.
+ *)
+  - (** We recall that on this side, only associativity was missing. *)
+    apply weqdirprodasstor.
+  - (** The subgoal is now fully given. *)
+
+    (** The missing link is associativity, but only on the
+        right-hand side of the top [×] symbol. *)
+    apply weqdirprodf.
+    + apply idweq.
+    + apply weqdirprodasstol.
+Defined.
+
+(** Warning: tactic [exact] does not work if there are existential
+    variables in the goal, but [eexact] can then be tried. *)
+
+Lemma sumex (A: UU) (P Q: A -> UU):
+  (∑ x: A, P x × Q x) -> (∑ x: A, P x) × ∑ x:A, Q x.
+Proof.
+  (** decompose the implication: *)
+  intro H.
+  (** decompose the Σ-type: *)
+  induction H as [x H'].
+  (** decompose the pair: *)
+  induction H' as [H1 H2].
+  (** decompose the pair in the goal *)
+  split.
+  - Fail split.
+    (**
+[[
+The command has indeed failed with message:
+         Unable to find an instance for the variable pr1.
+]]
+     *)
+    Fail (apply tpair).
+    (** A simple way out, by providing the first component: *)
+    split with x. (** [exists x] does the same *)
+    assumption.
+  - (** or use [eapply] and create an existential variable: *)
+    eapply tpair.
+    Fail assumption. (** the assumption [H2] does not agree with the goal *)
+    eexact H2.
+Defined.
+(** Notice that [eapply tpair] is not used in the UniMath library,
+    since [use tpair] normally comes in handier, see below. *)
+
+(** *** Warning on existential variables *)
+(** It may happen that the process of instantiating existential variables
+    is not completed when all goals have been treated.
+ *)
+
+(** an example adapted from one by Arnaud Spiwack, ~2007 *)
+
+About unit. (** from the UniMath preamble *)
+
+Local Definition P (x:nat) := unit.
+
+Lemma uninstex: unit.
+Proof.
+  refine ((fun x:P _ => _) _).
+  (** [refine] is like [exact], but one can leave holes with the wildcard "_".
+      This tactic should hardly be needed since most uses in UniMath
+      can be replaced by a use of the "tactic" [use], see further down
+      on this tactic notation for an Ltac definition.
+
+      Still, [refine] can come to rescue in difficult situations,
+      in particular during proof development. Its simpler variant
+      [simple refine] is captured by the [use] "tactic".
+*)
+  - exact tt.
+  - exact tt.
+    (** Now, Coq presents a subgoal that pops up from the "shelved goals".
+
+       Still, no more "-" bullets can be used.
+
+[[ -
+Error: Wrong bullet - : No more subgoals.
+]]
+     *)
+
+Show Existentials.
+(** a natural number is still being asked for *)
+Unshelve.
+(** Like this, we can focus on the remaining goal. *)
+exact 0.
+Defined.
+
+(** one can also name the existential variables in [refine]: *)
+Lemma uninstexnamed: unit.
+  Proof.
+    refine ((fun x:P ?[n] => _) _).  (** give a name to the existential variable *)
+    - exact tt.
+    - exact tt.
+Show Existentials.
+Unshelve.
+instantiate (n := 0).  (** more symbols to type but better to grasp *)
+Defined.
+
+(** ** a bit more on equational reasoning *)
+
+Section homot.
+(** A section allows to introduce local variables/parameters
+    that will be bound outside of the section. *)
+
+Locate "~".
+(** printing ~ #~# *)
+
+Print homot. (** this is just pointwise equality *)
+Print idfun. (** the identity function *)
+Locate "∘". (** exchanges the arguments of [funcomp] *)
+Print funcomp.
+(** plain function composition in diagrammatic order, i.e.,
+    first the first argument, then the second argument;
+    the second argument may even have a dependent type *)
+
+Context (A B: UU).
+(** makes good sense in a section, can be put in curly braces to indicate
+    they will be implicit arguments for every construction in the section *)
+
+Definition interestingstatement : UU :=
+  ∏ (v w : A → B) (v' w' : B → A),
+  w ∘ w' ~ idfun B → v' ∘ v ~ idfun A → v' ~ w' → v ~ w.
+
+Check (isinjinvmap': interestingstatement).
+
+Lemma ourisinjinvmap': interestingstatement.
+Proof.
+  intros. (** is a nop since the formula structure is not analyzed *)
+  unfold interestingstatement. (** [unfold] unfolds a definition *)
+  intros ? ? ? ? homoth1 homoth2 hyp a.
+  (** the extra element [a] triggers Coq to unfold the formula further;
+      [unfold interestingstatement] was there only for illustration! *)
+
+  (** we want to use transitivity that is expressed by [pathscomp0] and
+      instruct Coq to take a specific intermediate term *)
+Print Ltac intermediate_path. (** not telling because implicit arg. is not shown *)
+  intermediate_path (w (w' (v a))).
+  - apply pathsinv0. (** apply symmetry of equality *)
+    unfold homot in homoth1.
+    unfold funcomp in homoth1.
+    unfold idfun in homoth1.
+    apply homoth1. (** all the [unfold] were only for illustration! *)
+  -
+    Print maponpaths.
+    apply maponpaths.
+    unfold homot in hyp.
+    (** we use the equation in [hyp] from right to left, i.e., backwards: *)
+    rewrite <- hyp.
+    (** remark: for a forward rewrite, use [rewrite] without directional
+        argument *)
+    (** beautify the current goal: *)
+    change ((v' ∘ v) a = idfun A a).
+    (** just for illustration of [change] that allows to replace the goal
+        by a convertible expression; also works for hypotheses, e.g.: *)
+    change (v' ~ w') in hyp.
+    (** since [hyp] was no longer necessary, we should rather have deleted it: *)
+    clear hyp.
+    apply homoth2.
+Defined.
+
+Context (v w: A -> B) (v' w': B → A).
+
+Eval compute in (ourisinjinvmap' v w v' w').
+
+Opaque ourisinjinvmap'.
+Eval compute in (ourisinjinvmap' v w v' w').
+(** [Opaque] made the definition opaque in the sense that the identifier
+    is still in the symbol table, together with its type, but that it does
+    not evaluate to anything but itself.
+
+    If inhabitants of a type are irrelevant (for example if it is known
+    that there is at most one inhabitant, and if one therefore is not interested
+    in computing with that inhabitant), then opaqueness is an asset to make
+    the subsequent proof process lighter.
+
+    [Opaque] can be undone with [Transparent]:
+ *)
+Transparent ourisinjinvmap'.
+Eval compute in (ourisinjinvmap' v w v' w').
+
+(** If one uses [Compute] in place of [Eval compute in], then [Opaque] has no effect. *)
+
+(** Full and irreversible opaqueness is obtained for a construction
+    in interactive mode by completing it with [Qed.] in place of [Defined.]
+
+    Using [Qed.] is discouraged by the UniMath style guide. In Coq,
+    most lemmas, theorems, etc. (nearly every assertion in [Prop]) are
+    made opaque in this way. In UniMath, many lemmas enter subsequent
+    computation, and one should have good reasons for not closing an
+    interactive construction with [Defined.]. More than 5kloc of the UniMath
+    library have [Qed.], so these good reasons do exist and are not rare.
+*)
+
+End homot.
+Check ourisinjinvmap'.
+(** The section parameters [A] and [B] are abstracted away after the end
+    of the section - only the relevant ones. *)
+
+(** [assert] is a "chameleon" w.r.t. to opaqueness: *)
+Definition combinatorS_curried_with_assert2 (A B C: UU):
+  (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  intros H1 H2 H3.
+  assert (proofofB : B).
+  { apply H2.
+    assumption.
+  }
+  (** [proofofB] is just an identifier and not associated to the
+      construction we gave. Hence, the proof is opaque for us. *)
+  apply H1.
+  - assumption.
+  - assumption.
+Defined.
+Print combinatorS_curried_with_assert2.
+(** We see that [proofofB] is there with its definition, so it is
+    transparent.
+
+    See much further below for [transparent assert] that is like
+    [assert], but consistently transparent.
+*)
+
+(** ** composing tactics *)
+
+(** Up to now, we "composed" tactics in two ways: we gave them sequentially,
+    separated by periods, or we introduced a tree structure through the
+    "bullet" notation. We did not think of these operations as composition
+    of tactics, in particular since we had to trigger each of them separately
+    in interactive mode. However, we can also explicitly compose them, like so:
+ *)
+Definition combinatorS_induction_in_one_step (A B C: UU):
+  (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  intro Hyp123;
+  induction Hyp123 as [Hyp1 Hyp23];
+  apply Hyp1;
+  induction Hyp23 as [Hyp2 Hyp3];
+  split;
+  [ assumption
+  | apply Hyp2;
+    assumption].
+Defined.
+
+(** The sequential composition is written by (infix) semicolon,
+    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:
+
+    (1) We indicate that the intermediate results are irrelevant for someone who
+        executes the script so as to understand how and why the construction /
+        the proof works.
+
+    (2) The same tactic (expression) can uniformly treat all sub-goals stemming
+        from the preceding tactic application, as will be shown next.
+ *)
+Definition combinatorS_curried_with_assert_in_one_step (A B C: UU):
+  (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  intros H1 H2 H3;
+  assert (proofofB : B) by
+  ( apply H2;
+    assumption
+  );
+  apply H1;
+  assumption.
+Defined.
+
+(** This illustrates the grouping of tactic expressions by parentheses, the variant
+    [assert by] of [assert] used when only one tactic expression forms the proof of
+    the assertion, and also point (2): the last line is simpler than the expected line
+[[
+[assumption | assumption].
+]]
+*)
+
+(** Why would we want to do such compositions (cont'd)?
+
+    (3) We want to capture recurring patterns of construction / proof by tactics into
+        reusable Ltac definitions, see below.
+
+    (4) We want to make use of the [abstract] facility, explained now.
+ *)
+
+Definition combinatorS_induction_with_abstract (A B C: UU):
+  (A × B -> C) × (A -> B) × A -> C.
+Proof.
+  intro Hyp123;
+  induction Hyp123 as [Hyp1 Hyp23];
+  apply Hyp1;
+  induction Hyp23 as [Hyp2 Hyp3].
+  (** Now imagine that the following proof was very complicated but had no computational
+      relevance, i.e., could also be packed into a lemma whose proof would be finished
+      by [Qed]. We can encapsulate it into [abstract]: *)
+  abstract (split;
+  [ assumption
+  | apply Hyp2;
+    assumption]).
+Defined.
+
+Print combinatorS_induction_with_abstract.
+(** The term features an occurrence of [combinatorS_induction_with_abstract_subproof]
+    that contains the abstracted part; using the latter name is forbidden by the
+    UniMath style guide. Note that [abstract] is used hundreds of times in the
+    UniMath library. *)
+
+(** *** Ltac language for defining tactics *)
+
+(** Disclaimer: Ltac can do more than that, in fact Ltac is the name of the
+    whole tactic language of Coq. *)
+
+(** Ltac definitions can associate identifiers for tactics with tactic expressions.
+
+    We have already used one such identifier: [intermediate_path] in the [Foundations]
+    package of UniMath. In file [PartA.v], we have the code
+[[
+Ltac intermediate_path x := apply (pathscomp0 (b := x)).
+]]
+*)
+Print Ltac intermediate_path.
+(** does not show the formal argument [x] in the right-hand side.
+    Remedy (in ProofGeneral but not in VSCode): *)
+Set Printing All.
+Print Ltac intermediate_path.
+Unset Printing All.
+(** The problem with these Ltac definitions is that they are barely typed, they
+    behave rather like LaTeX macros. *)
+Local Ltac intermediate_path_wrong x := apply (pathscomp0 (X := x)(b := x)).
+(** This definition confounds the type argument [X] and its element [b].
+    The soundness of Coq is not at stake here, but the errors only appear
+    at runtime, as we will see below. Normal printing output hides the difference
+    with the correct tactic definition: *)
+Print Ltac intermediate_path_wrong.
+
+Section homot2.
+Context (A B : UU).
+
+Lemma ourisinjinvmap'_failed_proof: interestingstatement A B.
+  Proof.
+  intros ? ? ? ? homoth1 homoth2 hyp a.
+  Fail intermediate_path_wrong (w (w' (v a))).
+  (** The message does not point to the problem that argument [x] appears
+      a second time in the Ltac definition with a different needed type. *)
+Abort.
+End homot2.
+(** See #<a href="https://github.com/UniMath/UniMath/blob/master/UniMath/PAdics/frac.v##L23">#[https://github.com/UniMath/UniMath/blob/master/UniMath/PAdics/frac.v#L23]#</a>#
+    for a huge Ltac definition in the UniMath library to appreciate the lack
+    of type information. *)
+
+(** The UniMath library provides some Ltac definitions for general use: *)
+Print Ltac etrans. (** no need to explain - rather an abbreviation *)
+Set Printing All.
+Print Ltac intermediate_weq. (** problem with VSCode analogous to [intermediate_path] *)
+Unset Printing All.
+
+(** for the next tactic *)
+Require Import UniMath.MoreFoundations.Tactics.
+
+Set Printing All.
+Print Ltac show_id_type.
+(** output with ProofGeneral (output with VSCode falls again short of crucial information)
+[[
+Ltac show_id_type :=
+       match goal with
+       | |- @paths ?ID _ _ => set (TYPE := ID); simpl in TYPE
+       end
+]]
+Hardly ever present in proofs in the library, but it can be an excellent tool
+while trying to prove an equation: it puts the index of the path space
+into the context. This index is invisible in the notation with an equals
+sign that one normally sees as the goal, and coercions can easily give a wrong
+impression about that index. *)
+Unset Printing All.
+
+(** **** The most useful Ltac definition of UniMath *)
+Print Ltac simple_rapply.
+(** It applies the [simple refine] tactic with zero up to fifteen unknown
+    arguments. *)
+
+(** This tactic must not be used in UniMath since a "tactic notation"
+    is favoured: [Foundations/Preamble.v] contains the definition
+[[
+Tactic Notation "use" uconstr(p) := simple_rapply p.
+]]
+
+Use of [use]:
+*)
+Lemma sumex_with_use (A: UU) (P Q: A -> UU):
+  (∑ x:A, P x × Q x) -> (∑ x:A, P x) × ∑ x:A, Q x.
+Proof.
+  intro H; induction H as [x H']; induction H' as [H1 H2].
+  split.
+  - use tpair.
+    + assumption.
+    + cbn. (** this is often necessary since [use] does as little as possible *)
+      assumption.
+  - (** to remind the version where the "witness" is given explicitly: *)
+    exists x; assumption.
+Defined.
+(** To conclude: [use tpair] is the right idiom for an interactive
+    construction of inhabitants of Σ-types. Note that the second
+    generated sub-goal may need [cbn] to make further tactics
+    applicable.
+
+    If the first component of the inhabitant is already at hand,
+    then the "exists" tactic yields a leaner proof script.
+
+    [use] is not confined to Σ-types. Whenever one would be
+    inclined to start trying to apply a lemma [H] with a varying
+    number of underscores, [use H] may be a better option.
+*)
+
+(** There is another recommendable tactic notation that is also by
+    Jason Gross:
+[[
+Tactic Notation "transparent" "assert"
+                "(" ident(name) ":" constr(type) ")" :=
+                simple refine (let name := (_ : type) in _).
+]]
+*)
+Definition combinatorS_curried_with_transparent_assert (A B C: UU):
+  (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  intros H1 H2 H3.
+  transparent assert (proofofB : B).
+  { apply H2; assumption. } (** There is no [transparent assert by]. *)
+
+  (** Now, [proofB] is present with the constructed proof of [B]. *)
+Abort.
+(** To conclude: [transparent assert] is a replacement for [assert]
+    if the construction of the assertion is needed in the rest of
+    the proof.
+*)
+
+(** ** a final word, just on searching the library *)
+
+(** [SearchPattern] searches for the given pattern in what the library
+    gives as *conclusions* of definitions, lemmas, etc., and the current
+    hypotheses.
+
+    [Search] searches in the (full) types of all the library elements (and
+    the current hypotheses). It may provide too many irrelevant result
+    for your question. At least, it will also show all the relevant ones.
+
+    Anyway, only the imported part of the library is searched. The quick
+    way for importing the whole UniMath library is
+[[
+Require Import UniMath.All.
+]]
+You may test it with
+[[
+SearchPattern (_ ≃ _).
+]]
+with very numerous results.
+*)
+
+(** ** List of tactics that were mentioned *)
+(**
+[[
+exact
+apply
+intro
+set
+cbn / cbn in (old but sometimes useful form: simpl / simpl in)
+assumption
+intros (with pattern, with wild cards)
+split / split with / exists
+destruct as --- not desirable in UniMath
+induction / induction as
+admit --- only during proof development
+eapply
+eexact
+refine --- first consider "use" instead
+instantiate
+unfold / unfold in
+intermediate_path (Ltac def.)
+rewrite / rewrite <-
+change / change in
+clear
+assert {} / assert by
+abstract
+etrans (Ltac def.)
+intermediate_weq (Ltac def.)
+show_id_type (Ltac def.)
+simple_rapply (Ltac def., not to be used)
+use (Ltac notation)
+transparent assert (Ltac notation)
+]]
+*)
+
+(* End of file *)