lecture 5

Exercises1.agda

@@ -5,6 +5,7 @@ open import Agda.Primitive
 open import foundation-core.empty-types
 open import foundation-core.equivalences
 open import foundation-core.negation
+open import foundation.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.univalence
@@ -25,3 +26,5 @@ equal-to-zero {A} f = eq-equiv A ⊥ eqv
 
     eqv : A ≃ ⊥
     eqv = f , s , r
+
+asdf : 0 ≡ 1

Lecture1.typ

@@ -1,5 +1,6 @@
 #import "prooftree.typ": *
 #import "@preview/showybox:2.0.1": showybox
+#import "@preview/cetz:0.2.2": *
 #set page(width: 5.6in, height: 9in, margin: 0.4in)
 
 = Type theory crash course
@@ -340,3 +341,157 @@ $ not A :defeq A -> empty $
 *Solution.* Let $B :defeq rec_Bool (Type, unit, empty)$. Then $B(tru) defeq unit$ and $B(fls) defeq empty$. Then:
 
 $ lambda (p : Id(tru, fls)) . transport^B (p, tt) : Id(tru, fls) -> empty $
+
+== Univalent Foundations
+
+Voevodsky at HLF 2016:
+
+- Math is the study of structures on sets and their higher analogs.
+- Set-theoretic math is a subset of math that can be expressed in univalent foundations.
+- Classic math is a subset of univalent math consisting of results that require LEM / AC.
+
+=== Identities as paths
+
+Identity behaves like classic equality in these ways:
+
+- Reflexivity, symmetry, transitivity
+- $transport^B : B(x) times Id(x, y) -> B(y)$
+
+Identity also does _not_ behave like classic equality in these ways:
+
+- There can be two different identities $p, q : Id(x, y)$
+- There can be identities of identities $ a : Id_(Id(x, y)) (p, q) $
+  (but there don't have to be)
+
+So instead of treating them just as equality, we treat them kind of as homotopy, which is another notion of sameness coming from algebraic topology.
+
+// #canvas({
+//   import draw: *
+//   fill(black)
+//   circle((0, 0), radius: 0.1)
+//   circle((3, 0), radius: 0.1)
+//   line((0.25, 0), (2.75, 0))
+// })
+
+There's always a point $refl$ that stays at point $x$.
+
+=== Operations on paths
+
+#let pathto = $op(arrow.squiggly.r.long)$
+
+Symmetry: if we have $p : x pathto y$, then we have $sym(p) : y pathto x$
+
+Transport: transport sends a point $b : B(x)$ to a point $transport^B (p, b) : B(y)$.
+
+Functions map paths, not just points. If $p : x pathto y$, and $f : A -> B$, then $f(p) : f(x) pathto f(y)$
+
+=== Path concatenation
+
+Paths have
+
+- Associativity ($(p dot q) dot r pathto p dot (q dot r)$)
+- Identity ($p dot 1 pathto p$, $1 dot p pathto p$)
+- Inverse ($p dot p^-1 pathto 1$, $p^-1 dot p pathto 1$)
+
+*Theorem (Garner, van den Berg).* $(A, pathto_A, pathto_(pathto_A), ...)$  forms an $infinity$-groupoid (groupoid laws hold up to higher paths).
+
+=== Interpreting types as topological spaces
+
+There's an interpretation of univalent foundations into the category of _Kan complexes_.
+
+(cannot interpret in the category of topological spaces for some technical reasons, ignore and it's ok to use this for intuition only)
+
+=== Interpretation as simplicial sets
+
+#table(
+  columns: 2,
+  stroke: 0in,
+  [$(A, pathto_A, pathto_(pathto_A), ...)$], [Kan complex $A$],
+  [$a:A$], [$a in A_0$],
+  [$A times B$], [binary product],
+  [$A + B$], [binary coproduct],
+  [$A -> B$], [space of maps],
+  [$x : A tack.r B(x)$], [fibration $B -> A$ with fibers $B(x)$],
+  [$sum_(x : A) B(x)$], [total space of fibration $B -> A$],
+  [$product_(x : A) B(x)$], [space of sections of fibration $B -> A$],
+)
+
+Question: more intuition on fibration?
+
+- Fibration is something that has the transport property. A fibration is a _map_ in the category (i.e $B -> A$).
+
+  #image("fibration.jpeg", height: 3in)
+
+  Path lifting can be done over fibers in a fibration such as $B :defeq sum_(a : A) B(a)$
+
+=== Contractible types
+
+#let isContr = $sans("isContr")$
+
+*Definition (contractible).* A type $A$ is contractible if: $ isContr(A) :defeq sum_(x : A) product_(y : A) y pathto x $
+
+In homotopy theory, you can contract a space into a single point. This is also called a *singleton*. The specified point $a$ is called the "center" of contraction, and there are paths from any other $y : A$ to $x$.
+
+Question: do you have to give the point?
+
+- In constructive logic, you must explicitly give the point that it is contracted to, cannot just prove with contradiction.
+
+=== Equivalence
+#let isequiv = $sans("isequiv")$
+
+*Definition (equivalence).* A map $f : A -> B$ is an *equivalence* if it has contractible fibers.
+
+$ isequiv(f) :defeq product_(b : B) isContr(sum_(a : A) f(a) pathto b) $
+
+Fix $b$, the sigma is the preimage of the point $b$. For all $b$, all preimages are contractible.
+
+#let eqv = $tilde.eq$
+
+$ A eqv B :defeq sum_(f : A -> B) isequiv(f) $
+
+There are also other definitions of equivalence.
+
+*Exercise.* Show that 1 is contractible.
+
+*Exercise.* Let $A$ be a contractible type. Construct an equivalence $A eqv 1$
+
+For paths between pairs, in the dependent version, we have
+
+$ ((a, b) pathto (a' , b')) eqv sum_(p : a pathto a') transport^B (p, b) pathto b' $
+
+This is required because $b : B(a)$ but $b' : B(a')$, and we can't write paths between different types.
+So instead, we use transport to get back into the correct type: $transport^B (p, b) : B(a')$
+
+=== Path types of identity types
+
+Cannot show uniqueness of identity proofs (UIP): $ product_(a, b: A) product_(p, q : a pathto b) p pathto q $
+
+(Lean assumes UIP)
+
+=== Path types of the universe
+
+#let idtoequiv = $sans("idtoequiv")$
+
+$ idtoequiv : product_(A, B : Type) (A pathto B) -> (A eqv B) $
+
+*Definition (univalence).* $idtoequiv$ is an equivalence.
+
+- Question: What is the benefit of UIP over univalence?
+  - UIP gives set theory
+
+- Question: what if you had a path between $A pathto B$ and $A eqv B$?
+  - You can use univalence to get a path. But we shouldn't assume an equality without first using $idtoequiv$.
+
+=== Propositional truncation
+
+#let trunc(A) = [$bar.double$#A$bar.double$]
+
+#typeIntroTable(
+  [If $A$ is a type, then $trunc(A)$ is a type],
+  [If $a:A$, then $overline(a):trunc(A)$ and $ p(A) : product_(x, y: trunc(A)) x pathto y $],
+  [If $f:A->B$ and $B$ is a prop, then we have $overline(f) : trunc(A) -> B$],
+  [$overline(f)(overline(a)) defeq f(a)$],
+)
+
+- $p(A)$ turns $trunc(A)$ into a proposition
+- $trunc(A)$ is empty if $A$ is, and contractible if $A$ has one element.

Lecture3.typ

@@ -0,0 +1,3 @@
+#import "prooftree.typ": *
+#import "@preview/showybox:2.0.1": showybox
+#set page(width: 5.6in, height: 9in, margin: 0.4in)

Lecture5.typ

@@ -0,0 +1,246 @@
+#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)
+
+= Set-level mathematics
+
+#let isofhlevel = $sans("isofhlevel")$
+#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 = $=$
+
+$ isofhlevel& : Nat -> Type -> Type \  
+isofhlevel&(zero)(X) :defeq isContr(X) \
+isofhlevel&(suc(n))(X) :defeq product_(x,y:X) \
+isofhlevel& (n, x propeq y)$
+
+$ isSet(X) :defeq isofhlevel(2)(X) \
+Set :defeq sum_(X : Type) isSet(X) $
+
+Sets are the types that satisfy UIP. We don't have _all_ types satisfying UIP since it would contradict univalence.
+
+- If $p, q : x propeq y$  then $p propeq q$
+- Also, $p : x propeq x$ then $p propeq refl$
+
+Quite a lot of things are sets. What are some sets?
+
+== Decidable equality
+
+*Definition (decidable).* A type $X$ is _decidable_ if $X + not X$.
+
+*Definition (decidable equality).* A type $X$ has decidable equality if all of its path types are decidable.
+
+If a type $X$ has decidable equality, then $X$ is a set. (Hedberg's theorem.)
+
+*Exercise.* Prove that $Bool$ and $Nat$ have decidable equality
+
+Using this theorem you can prove $Bool$ and $Nat$ are sets. 
+
+=== Closure properties
+
+Sets also have a lot of closure properties:
+
+- $sum_(x : A) B(x)$ is a set if $A$ and all $B(x)$ are
+- $A times B$ is a set if $A$ and $B$ are
+- $product_(x : A) B(x)$ is a set if all $B(x)$ are
+- $A -> B$ is a set if $B$ is
+- $A$ is a set if its a proposition
+
+Example. $Bool$ is a set, so $Bool times Bool$ is a set. etc. What types are definitely _not_ a set?
+
+*Exercise.* Prove that $Prop :defeq sum_(X : Type) isProp(X)$ is a set. (this is not a trivial proof by one of the closure properties)
+
+- It's consistent to add global UIP to regular MLTT. 
+- If you add univalence, some types can be shown to _not_ be sets.
+- (UIP + univalence == inconsistent)
+
+You can prove that $Type$ is not a set, if it contains the type $Bool$ (not exactly just this, but some other types might be also able to satisfy this (true $eq.not$ false???))
+
+Notably, $Set$ is also not a set. (what h-level does it have?). This is different from working in a classic system with UIP.
+
+Why do we care about sets, h-levels and props? Some types are very "property"-like, and it's nice for them to be propositions. For example, if a natural number is even.
+
+$ Even :defeq sum_(n : Nat) isEven(n) $
+
+In dependent pairs, the second b condition requires a transport to express its identity. In the case that $B(x)$ is a proposition for all $x$, then $Even$s can have the "right" notion of equality.
+
+Sets are important because a lot of side conditions (i.e is even), are equational. You would like these to be propositions. By restricting to sets, you get this nice property.
+
+One example that's weird about univalence foundations, $f : X -> Y$
+
+$ isInjective(f) :defeq product_(x,x': X) f(x) propeq f(x') -> x propeq x' $
+
+This isn't a proposition in general, but if we make $X$ a set, this becomes a proposition. If $X$ isn't a set, then the actual proof of injectivity needs to be carried around and is relevant.
+
+Question: why does $Y$ not need to be a set here? \
+Answer: see exercises!
+
+You can also define it in a way that doesn't depend on what $X$ and $Y$ are (truncations?).
+
+Another example is isomorphism.
+
+*Warning.* Stating the univalence axiom with isomorphism instead of equivalence leads to inconsistency. (advanced exercise). But if $X$ and $Y$ are sets, then $isIso(f) tilde.eq isEquiv(f) $
+
+The space of proofs of equivalence is a proposition. But the space of isomorphisms may not be a proposition. So they are logically equivalence (there are functions in both directions) but there's no inverse laws because there may be more isomorphisms.
+
+== Applications: algebraic structures
+
+A *monoid* is a triple $(M, mu, e)$ of:
+
+- A set $M$
+- A multiplciation $mu : M times M -> M$
+- Unit $e in M$
+
+satisfying associativity, left / right neutrality. Exampls of these are natural numbers or integers with $mu = $ addition and $e = 0$.
+
+But in type theory, equations are just other types. So we need a 6-tuple instead of a 3-tuple that also contains the three properties (associativity, neutrality...). In particular, we want $M$ to be a $Set$ instead of a $Type$.
+
+This way we can have the axioms to be propositions. When comparing two monoids we would like the equality to really just involve the first three parts and not have to talk about equality between the proofs of the properties in the last 3.
+
+So we can re-group these into:
+
+$ Monoid :defeq sum_( M :Set) sum_(mu, e : MonoidStr(M)) MonoidAxioms(M, (mu,e)) $
+
+This type will have the nice equality property that we want if $MonoidAxioms$ is a proposition. And we will have this automatically if $M$ is a set.
+
+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)$
+
+*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.
+
+*Exercise.* The type of monoid equalities $MonoidM propeq MonoidM'$ is equivalent to the type of monoid isomorphisms $MonoidM tilde.equiv MonoidM'$.
+
+_Proof sketch._ First, discard the axioms since $M$ is a set. So split it apart into $M$ equality and then the equality of the $MonoidStr$ part, which requires a transport. With $M$ is a set, the transports go away.
+
+In fact, any property about monoids expressible in UF can be transported along isomorphism.
+
+$ (MonoidM tilde.equiv MonoidM') -> T(MonoidM) -> T(MonoidM') $
+
+*Example.* If $MonoidM$ is commutative, then $MonoidM'$ is also, regardless of what commutativity says.
+
+This is known as the _Structure Identity Principle_.
+
+#align(center)[
+  #quote[
+    Isomorphic mathematical structures are equal as structured types, and have all the same structural properties.
+  ]
+]
+(Coquand, Aczel)
+
+This holds for many algebraic structures. Isomorphic structures have *all* the same definable properties.
+
+https://ncatlab.org/nlab/show/structure+identity+principle
+
+Question: is this only true of sets? \
+Answer: this is normally stated for sets, but this is more general than that. The isomorphisms just become a bit more complicated.
+
+== Predicates on types
+
+A *subtype* $A$ of a type $X$ is a prop-valued predicate:
+
+$ A : X -> Prop $
+
+*Exercise.* Prove that the type of subtypes of $X$ is a set. (you can do this just with things from the slides)
+
+You might've thought that a subtype would be a type. But $A$ is a function. So you can create a type that carries it:
+
+$ carrier(A) :defeq sum_(x: X) A(x) $
+
+What about a binary relation?
+
+$ R : X -> X -> Prop $
+
+*Exercise.* Prove that the type of binary relations on $X$ is a set.
+
+These behave as you think. For example:
+
+$ reflexive(R) :defeq product_(x: X) R(x)(x) $
+
+(there can only be one proof of this because $R$ is prop-valued)
+
+Why are we talking about equivalence relations? Well, one important thing in math is to take the quotient of a set by an equivalence relation.
+
+The *quotient* of a type $X$ by an equivalence relation $R$ on $X$ is a pair $(X \/ R , p)$ of a type $X \/ R$ and a map $p : X -> X \/ R$ such that any $R$-compatible map $f$ into a set $Y$ factors uniquely via $p$. ($R$-compatible map is $product_(x,y:A) R(x,y) -> f(x) propeq f(y)$)
+
+You think of the quotient as the set of equivalence classes. $p$ sends each element of $X$ to its equivalence class.
+
+#align(center)[#commutative-diagram(
+  node((0, 0), $X$),
+  node((1, 0), $X\/R$),
+  node((1, 1), $Y$),
+  arr($X$, $X\/R$, $p$),
+  arr($X\/R$,$Y$, $exists ! f'$),
+  arr($X$, $Y$, $f$),
+)]
+
+MLTT normally doesn't have quotients. But in UF we can define them as the set of equivalence classes in $R$.
+
+(You could consider things like groupoid quotients too) (you can quotient the unit type into a circle) (the problem is if $Y$ is not a set, then $X \/ R$ also won't be a set) (Favonia: don't do this yet)
+
+== Quotient set
+
+*Definition.* A subtype $A : X -> Prop$ is an equivalence class of $R$ if 
+
+$ iseqclass(A, R) :defeq bar.double carrier(A) bar.double times (product_(x,y:X) R(x,y) -> A(x) -> A(y)) \
+times (product_(x,y:X) A(x) -> A(y) -> R(x, y )) $
+
+Then we define
+
+$ X \/ R :defeq sum_(A : X -> Prop) iseqclass(A, R) $
+
+The fact that $Prop$ is a set, that two $Prop$s are equal if they imply each other is a consequence of univalence. So you can't do this in plain MLTT.
+
+== Questions
+
+- #[
+  *Why is this not possible in MLTT?* \
+  Let's say you dropped the truncation. What happens? Then there are a lot of proofs of $iseqclass(A, R)$ (one for each $x : X$ telling how it got into $X \/ R$). Then $X \/ R$ will count as many elements as there are in $X$, so you haven't reduced the number of elements at all.
+]
+
+- #[
+  *What about MLTT with UIP?*
+  Lean has MLTT with UIP and also they have quotients. Even if you add UIP to a language, you don't get quotients. The c ool thing in UF is that you can just define quotients.
+]
+
+- #[
+  *Is it possible to use unimath for algebraic structures that can't be defined with equations? (i.e quasi-groups)* \
+  https://en.wikipedia.org/wiki/Quasigroup \
+  Benedikt: there are some other examples, i.e fields. In constructive math there's lots of definitions of a field.
+]
+
+- #[
+  *What does SIP have to do with univalence? Sounds true of base MLTT.* \
+  Univalence says the equality of two sets is an isomorphism. You can think of $Set$ as an algebraic structure that has a carrier and no operations. So you can kind of observe that univalence holds for $Set$ as kind of a trivial case. But the SIP still holds even if you add more operations.
+  
+  *Where did you use univalence in the proof sketch?*
+  Going from $p : MonoidM propeq MonoidM'$ to $f : MonoidM tilde.equiv MonoidM'$
+
+  *How does univalence imply this?*
+  $MonoidM$ and $MonoidM'$ are sets. This is true because of univalence.
+]

Lol.agda

@@ -1,39 +1,112 @@
-{-# OPTIONS --cubical #-}
+open import Agda.Primitive
 
-open import Cubical.Foundations.Prelude
+private
+  variable
+    l : Level
 
-data ℕ : Set where
-  zero : ℕ
-  suc : ℕ → ℕ
+data _≡_ {A : Set l} : A → A → Set l where
+  refl : {x : A} → x ≡ x
 
-add : ℕ → ℕ → ℕ
-add zero n = n
-add (suc m) n = add m (suc n)
+data ⊥ : Set where
+data ⊤ : Set where
+  tt : ⊤
 
-data ℤ₀ : Set where
-  pos : ℕ → ℤ₀
-  negsuc : ℕ → ℤ₀
+result2 : (B : Set) → ((A : Set) → (B → A) → A) → B
+result2 B x = 
+  let
+    y = x B λ x → x
+  in y 
 
-data ℤ : Set where
-  z : ℕ → ℕ → ℤ
-  p : (m n : ℕ) → z m n ≡ z (suc m) (suc n)
+data N : Set where
+  zero : N
+  suc : N -> N
+{-# BUILTIN NATURAL N #-}
 
-ℤ→ℤ₀ : ℤ → ℤ₀
-ℤ→ℤ₀ (z zero zero) = pos zero
-ℤ→ℤ₀ (z zero (suc x₁)) = negsuc x₁
-ℤ→ℤ₀ (z (suc x) zero) = pos (suc x)
-ℤ→ℤ₀ (z (suc x) (suc x₁)) = ℤ→ℤ₀ (z x x₁)
-ℤ→ℤ₀ (p m n i) = ℤ→ℤ₀ {!   !}
+data Bool : Set where
+  true : Bool
+  false : Bool
 
-ℤ₀→ℤ : ℤ₀ → ℤ
-ℤ₀→ℤ (pos x) = z x zero
-ℤ₀→ℤ (negsuc x) = z zero (suc x)
+ifbool : {A : Set} (x y : A) -> Bool -> A
+ifbool {A} x y true = x 
+ifbool {A} x y false = y
 
-ap : ∀ {A B x y} → (f : A → B) → (x ≡ y) → (f x ≡ f y)
-ap f x i = f (x i)
+negbool : Bool -> Bool
+negbool true = false
+negbool false = true
 
-add-ℤ : ℤ → ℤ → ℤ 
-add-ℤ (z x x₁) (z x₂ x₃) = z (add x x₂) (add x₁ x₃)
-add-ℤ (z x x₁) (p m n i) = z (add x {!   !}) {!   !}
-add-ℤ (p m n i) (z x x₁) = {!   !}    
-add-ℤ (p m n i) (p m₁ n₁ i₁) = {!   !}
+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

exercises_tactics.v

@@ -0,0 +1,209 @@
+(** Exercise sheet for lecture 4: Tactics in Coq.
+
+  prepared using material by Ralph Matthes
+ *)
+
+(** * Exercise 1
+Formalize the following types in UniMath and construct elements for them interactively -
+if they exist. Give a counter-example otherwise, i.e., give specific parameters and a
+proof of the negation of the statement.
+
+[[
+1.    A × (B + C) → A × B + A × C, given types A, B, C
+2.    (A → A) → (A → A), given type A (for extra credit, write down five elements of this type)
+3.    Id_nat (0, succ 0)
+4.    ∑ (A : Universe) (A → empty) → empty
+5.    ∏ (n : nat), ∑ (m : nat), Id_nat n (2 * m) + Id_nat n (2 * m + 1),
+      assuming you have got arithmetic
+6.    (∑ (x : A) B × P x) → B × ∑ (x : A) P x, given types A, B, and P : A → Universe
+7.    B → (B → A) → A, given types A and B
+8.    B → ∏ (A : Universe) (B → A) → A, given type B
+9.    (∏ (A : Universe) (B → A) → A) → B, given type B
+10.   x = y → y = x, for elements x and y of some type A
+11.   x = y → y = z → x = z, for elements x, y, and z of some type A
+]]
+
+More precise instructions and hints:
+
+1.  Use [⨿] in place of the + and pay attention to operator precedence.
+
+2.  Write a function that provides different elements for any natural number argument,
+    not just five elements; for extra credits: state correctly that they are different -
+    for a good choice of [A]; for more extra credits: prove that they are different.
+
+3.  An auxiliary function may be helpful (a well-known trick).
+
+4.  The symbol for Sigma-types is [∑], not [Σ].
+
+5.  Same as 1; and there is need for module [UniMath.Foundations.NaturalNumbers], e.g.,
+    for Lemma [natpluscomm].
+
+6.-9. no further particulars
+*)
+
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
+Require Import UniMath.Foundations.Preamble.
+Require Import UniMath.Foundations.PartA.
+Require Import UniMath.Foundations.NaturalNumbers.
+
+(* 1.    A × (B + C) → A × B + A × C, given types A, B, C *)
+Goal ∏ (A B C : UU), A × (B ⨿ C) -> (A × B) ⨿ (A × C).
+Proof.
+  intros.
+  induction X.
+  induction pr2.
+  - apply ii1. apply tpair. apply pr1. apply a. 
+  - apply ii2. apply tpair. apply pr1. apply b. 
+Defined.
+  
+(* 2.    (A → A) → (A → A), given type A (for extra credit, write down five elements of this type) *)
+Goal ∏ (A : UU), (A -> A) -> (A -> A).
+Proof.
+  intros.
+  apply X0.
+Defined.
+
+(* 3.    Id_nat (0, succ 0) *)
+Goal (O = S O) -> empty.
+Proof.
+  intros.
+  exact (transportf (fun c => match c with O => unit | S _ => empty end) X tt).
+Defined.
+
+Locate "∑".
+Print total2.
+
+(* 4.    ∑ (A : Universe) (A → empty) → empty *)
+Goal ∑ (A : UU), (A -> empty) -> empty.
+Proof.
+  use tpair.
+  - exact unit.
+  - simpl. intros. apply X. exact tt.
+Defined.
+
+(* 5.    ∏ (n : nat), ∑ (m : nat), Id_nat n (2 * m) + Id_nat n (2 * m + 1), *)
+      (* assuming you have got arithmetic *)
+Goal ∏ (n : nat), ∑ (m : nat), (paths n (2 * m)) ⨿ (paths n (1 + (2 * m))).
+Proof.
+  intros.
+  induction n.
+  - use tpair.
+    + exact 0.
+    + simpl. apply inl. reflexivity.
+  - induction IHn. induction pr2.
+    * use tpair. exact pr1. simpl. apply inr. rewrite a. reflexivity.
+    * use tpair. exact (S pr1). simpl. apply inl. rewrite b. simpl.
+      assert (S (pr1 + pr1) = S pr1 + pr1).
+      + reflexivity.
+      + rewrite X. rewrite natpluscomm. reflexivity.
+Defined.
+
+(* 6.    (∑ (x : A) B × P x) → B × ∑ (x : A) P x, given types A, B, and P : A → Universe *)
+Goal ∏ (A B : UU) (P : A -> UU), (∑ (x : A), B × P x) -> B × ∑ (x : A), P x.
+Proof.
+  intros.
+  induction X. induction pr2.
+  use tpair.
+  * exact pr0. 
+  * simpl. use tpair.
+    + exact pr1.
+    + simpl. exact pr2.
+Defined.  
+
+(* 7.    B → (B → A) → A, given types A and B *)
+Goal ∏ (A B : UU), B -> (B -> A) -> A.
+Proof.
+  intros.
+  apply X0. exact X.
+Defined.
+
+(* 8.    B → ∏ (A : Universe) (B → A) → A, given type B *)
+Goal ∏ (B : UU), B -> ∏ (A : UU), (B -> A) -> A.
+Proof.
+  intros.
+  apply X0. exact X.
+Defined.
+
+(* 9.    (∏ (A : Universe) (B → A) → A) → B, given type B *)
+Goal ∏ (B : UU), (∏ (A : UU), (B -> A) -> A) -> B.
+Proof.
+  intros.
+  exact (X B (fun x => x)).
+Defined.
+
+(* 10.   x = y → y = x, for elements x and y of some type A *)
+Goal ∏ (A : UU) (x y : A), x = y -> y = x.
+Proof.
+  intros.
+  induction X.
+  apply idpath.
+Defined.
+
+(* 11.   x = y → y = z → x = z, for elements x, y, and z of some type A *)
+Goal ∏ (A : UU) (x y z : A), x = y -> y = z -> x = z.
+Proof.
+  intros.
+  induction X. induction X0.
+  apply idpath.
+Defined.
+
+(** * Exercise 2
+Define two computable strict comparison operators for natural numbers based on the fact
+that [m < n] iff [n - m <> 0] iff [(m+1) - n = 0]. Prove that the two operators are
+equal (using function extensionality, i.e., [funextfunStatement] in the UniMath library).
+
+It may be helpful to use the definitions of the exercises for lecture 2.
+The following lemmas on substraction [sub] in the natural numbers may be
+useful:
+
+a) [sub n (S m) = pred (sub n m)]
+
+b) [sub 0 n = 0]
+
+c) [pred (sub 1 n) = 0]
+
+d) [sub (S n) (S m) = sub n m]
+
+*)
+
+
+(** from exercises to Lecture 2: *)
+Definition ifbool (A : UU) (x y : A) : bool -> A :=
+  bool_rect (λ _ : bool, A) x y.
+
+Definition negbool : bool -> bool := ifbool bool false true.
+
+Definition nat_rec (A : UU) (a : A) (f : nat -> A -> A) : nat -> A :=
+  nat_rect (λ _ : nat, A) a f.
+
+Definition pred : nat -> nat := nat_rec nat 0 (fun x _ => x).
+
+Definition is_zero : nat -> bool := nat_rec bool true (λ _ _, false).
+
+Definition iter (A : UU) (a : A) (f : A → A) : nat → A :=
+  nat_rec A a (λ _ y, f y).
+
+Notation "f ̂ n" := (λ x, iter _ x f n) (at level 10).
+
+Definition sub (m n : nat) : nat := pred ̂ n m.
+
+Definition lt1 (m n : nat) : bool := negb (is_zero (sub m n)).
+
+Definition lt2 (m n : nat) : bool := is_zero (sub (S m) n).
+
+Definition lt1_eq_lt2 : lt1 = lt2.
+Proof.
+  rewrite (funextfun lt1 lt2).
+  - apply idpath.
+  - intro x. rewrite (funextfun (lt1 x) (lt2 x)).
+    + apply idpath.
+    + intro y. unfold lt1. unfold lt2.
+      induction x.
+      induction y.
+      { auto. }
+      { 
+        assert (∏ (y : nat), sub 0 y = 0) as Sub0.
+        { intros. induction y0. { auto. } { simpl. unfold pred. rewrite IHy0. auto. } }
+        rewrite Sub0. cbn.
+      }