2024-07-29 19:39:10 +00:00
|
|
|
|
Require Import UniMath.Foundations.All.
|
|
|
|
|
|
|
|
|
|
|
|
Inductive empty : Type := .
|
|
|
|
|
|
|
|
|
|
|
|
Definition slide16_exercise (t : empty): bool :=
|
|
|
|
|
|
match t with end.
|
|
|
|
|
|
|
|
|
|
|
|
Definition slide18_exercise (t : nat): bool :=
|
|
|
|
|
|
match t with
|
|
|
|
|
|
| O => true
|
|
|
|
|
|
| S _ => false
|
|
|
|
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
(* Slide 22, Exercise 1*)
|
|
|
|
|
|
|
|
|
|
|
|
Definition fst {A B : Type} (p : A × B): A.
|
|
|
|
|
|
Proof.
|
|
|
|
|
|
induction p.
|
|
|
|
|
|
apply pr1.
|
|
|
|
|
|
Defined.
|
|
|
|
|
|
(* Show Proof. *)
|
|
|
|
|
|
|
|
|
|
|
|
Definition snd {A B : Type} (p : A × B): B.
|
|
|
|
|
|
Proof.
|
|
|
|
|
|
induction p.
|
|
|
|
|
|
apply pr2.
|
|
|
|
|
|
Defined.
|
|
|
|
|
|
|
|
|
|
|
|
Definition swap {A B : Type} (p : A × B): B × A :=
|
|
|
|
|
|
match p with (a ,, b) => (b ,, a) end.
|
|
|
|
|
|
(* Definition swap {A B : Type} (p : A × B): B × A.
|
|
|
|
|
|
Proof.
|
|
|
|
|
|
induction p.
|
|
|
|
|
|
constructor.
|
|
|
|
|
|
- apply pr2.
|
|
|
|
|
|
- apply pr1.
|
|
|
|
|
|
Defined. *)
|
|
|
|
|
|
|
|
|
|
|
|
(* Slide 38, Exercise: transport *)
|
|
|
|
|
|
|
|
|
|
|
|
Definition transport {A : Type} {B : A -> Type}
|
|
|
|
|
|
{x y : A} (p : paths x y) (bx : B x): B y.
|
|
|
|
|
|
induction p.
|
|
|
|
|
|
apply bx.
|
|
|
|
|
|
Defined.
|
|
|
|
|
|
(* Show Proof. *)
|
|
|
|
|
|
|
|
|
|
|
|
(* Slide 39, Exercise: swap involutive *)
|
|
|
|
|
|
|
|
|
|
|
|
Definition slide39_exercise {A B : Type} (t : A × B) : paths (swap (swap t)) t.
|
|
|
|
|
|
reflexivity.
|
|
|
|
|
|
Show Proof.
|
|
|
|
|
|
|
|
|
|
|
|
(* Slide 44, Exercise: neg *)
|
|
|
|
|
|
|
2024-07-29 22:45:35 +00:00
|
|
|
|
(* Definition slide44_exercise {A : Type} : not *)
|
