From 290fb3c5101cf2957596cd21dfc8c04f6c441ca2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 30 May 2017 12:35:57 +0200 Subject: [PATCH] fix typos --- lectures/lecture3.ctt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lectures/lecture3.ctt b/lectures/lecture3.ctt index 7465e59..584dc0d 100644 --- a/lectures/lecture3.ctt +++ b/lectures/lecture3.ctt @@ -40,7 +40,7 @@ ex (A : U) (a b : A) (p : Path A a b) : {- In the above example the k = 0 face of the cube was omitted. The -reason is because of "uniformity" of compisitions, this means that +reason is because of "uniformity" of compositions, this means that comp has to commute with substitutions (like any other operation in type theory). @@ -166,7 +166,7 @@ isProp (A : U) : U = (x y : A) -> Path A x y -- A type of h-level 2 is called a "set" and in such a type all of the --- equalities between elements are equal. This propoerty is usually +-- equalities between elements are equal. This property is usually -- called UIP, "uniqueness of identity types", and a very important -- theorem is Hedberg's theorem which says that types with decidable -- equality satisfy UIP (so nat, bool, etc. are all sets). -- 2.34.1