From: Anders Mörtberg Date: Sat, 17 Jun 2017 14:46:52 +0000 (+0200) Subject: more explanations X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4077345624e324a61f02136d71ea85ca9ab79a54;p=cubicaltt.git more explanations --- diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt index 0debeda..ba7a308 100644 --- a/lectures/lecture2.ctt +++ b/lectures/lecture2.ctt @@ -82,7 +82,7 @@ do *not* hold (unless r is 0 or 1). This means that a De Morgan algebra is *not* a Boolean algebra. The intuition for why this has to be the case is that II should model the real interval [0,1] and there we of course cannot have min(1-r,r) = 0 or max(1-r,r) = 1 for a point -r in [0,1]. +r in [0,1] (unless r is 0 or 1). To test if two elements r and s in II are equal we first push the negations to the atoms and then compare their disjunctive normal forms @@ -221,6 +221,7 @@ define transport and do a lot of other things. Given p : Path A a b and q : Path A b c the composite of the two paths is obtained from a composition of this open square: +i : II |- a - - - - - - - - > c ^ ^ @@ -233,7 +234,13 @@ is obtained from a composition of this open square: a ----------------> b p @ i -The composition computes the dashed line at the top of the square. + +The composition is the dashed line at the top of the square. The +direction i goes left-to-right and j goes down-to-up. As we are +constructing a Path from a to c we have i : II in the context already +which is why we have to put p @ i as bottom (this is achieved by +writing the comp under a binder). The direction j that we are +doing the composition in is implicit, more about this below. -} trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =