From: Anders Mörtberg Date: Tue, 30 May 2017 10:35:57 +0000 (+0200) Subject: fix typos X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=290fb3c5101cf2957596cd21dfc8c04f6c441ca2;p=cubicaltt.git fix typos --- 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).