From: Sophie Bernard Date: Wed, 14 Jun 2017 09:30:31 +0000 (+0200) Subject: comments X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=15fc089e136782c92c7adfeb2286303c4ce101ca;p=cubicaltt.git comments --- diff --git a/examples/constcubes.ctt b/examples/constcubes.ctt index e7c87cb..adefa24 100644 --- a/examples/constcubes.ctt +++ b/examples/constcubes.ctt @@ -1,3 +1,6 @@ +-- This file contains types for 2D, 3D and 4D cubes, with examples of constant +-- cubes (the same value everywhere or the same path on each 2D edge) and a +-- small generalisation with different end points module constcubes where Path (A : U) (a b : A) : U = PathP ( A) a b @@ -73,6 +76,56 @@ Cube (A : U) (a0 b0 c0 d0 a1 b1 c1 d1 : A) PathP ( (Square A (pa @ i) (pb @ i) (pc @ i) (pd @ i) (sab @ i) (scd @ i) (sac @ i) (sbd @ i))) s0 s1 +Fd (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : + Square A a b b c p q p q = + comp (<_> A) (p @ i \/ j) + [ (i = 0) -> p @ j + , (i = 1) -> q @ k /\ j + , (j = 0) -> p @ i + , (j = 1) -> q @ k /\ i ] + + +B (A : U) (a b c d : A) (p : Path A a b) (q : Path A b c) (r : Path A c d) : + Cube A b b b b b c c d + (<_> b) (<_> b) (<_> b) (<_> b) q r q r + (<_> <_> b) (Fd A b c d q r) + (<_> b) q q ( (Fd A b c d q r @ i @ i)) + ( q @ i /\ j) ( ((Fd A b c d q r) @ i @ j /\ i)) + ( q @ i /\ j) ( ((Fd A b c d q r) @ i @ j /\ i)) = + (Fd A b c d q r) @ (i /\ j /\ k) @ (k /\ (i \/ j)) + +Bla (A : U) (a b c d : A) (p : Path A a b) (q : Path A b c) (r : Path A c d) : + Cube A a b b c b c c d + p q p q q r q r + (Fd A a b c p q) (Fd A b c d q r) + p q q r + (Fd A a b c p q) (Fd A b c d q r) + (Fd A a b c p q) (Fd A b c d q r) = + let Ab : Cube A a b b b a b b c + p (<_> b) p (<_> b) p q p q + ( p @ i \/ j) (Fd A a b c p q) + (<_> a) (<_> b) (<_> b) q + (<_> p) ( q @ i /\ j) + (<_> p) ( q @ i /\ j) = + (Fd A a b c p q) @ (i /\ j /\ k) @ (i \/ j) + + + + in comp (<_> A) (p @ i \/ j \/ k) + [ (k = 0) -> Ab @ l @ i @ j + , (k = 1) -> (Fd A b c d q r @ i /\ j /\ l @ l /\ (i \/ j)) + , (j = 0) -> Ab @ l @ i @ k + , (j = 1) -> (Fd A b c d q r @ i /\ k /\ l @ l /\ (i \/ k)) + , (i = 0) -> Ab @ l @ j @ k + , (i = 1) -> (Fd A b c d q r @ k /\ j /\ l @ l /\ (k \/ j))] + + + + + + + + -- Test : cube with only a everywhere Cubea (A : U) (a : A) : Cube A a a a a a a a a (<_> a) (<_> a) (<_> a) (<_> a) (<_> a) (<_> a) (<_> a) (<_> a) @@ -271,9 +324,24 @@ ct (A : U) (a : A) (p : Path A a a) : + + + + + + {- -General Constant Square +General Constant Squares + + q + b -----> c + ^ ^ + | | + p | | q + | | + a -----> b + p Suggested by José Grimm