module geometryOfConstancyHoTTUF2015 where {- The geometry of constancy ------------------------- Thierry Coquand & Martin Escardo April 2015, updated June to the new version of cubicaltt without regularity. This is in cubical type theory (ctt) https://github.com/mortberg/cubicaltt Some proofs are first given in HoTT style and then directly in ctt style. If we have a circle-indexed family of functions f : (x : S1) -> x = base -> A x such that f base is constant, then each of them factors through ||x=base||, that is, through 1. So we can define g : (x : S1) -> A x such that g x is the constant value of f x: f x p = g x for all p : x = base. This relies on the naturality of f on x and works by S1-induction on x. However, if for a fixed x0:S1 and some given type A we have a single constant function f:x0=base->A, then again we can find a point of A which is the constant value of f. This relies on both the above result and the use of a generalized circle S(-) to describe constant functions, defined by higher induction. Contents 0. Preliminaries 1. Factoring a family of constant functions on x = base. 2. Propositional truncation. 3. The generalized circle. 4. Factoring a single function on x0 = base. -} -- 0. Preliminaries. import prelude import circle -- We need based path induction with the second end-point fixed, which -- is reduced to the one with the first one fixed (J here): J' (A : U) (a : A) (C : (x : A) -> Id A x a -> U) (d : C a (refl A a)) (x : A) (p : Id A x a) : C x p = J A a (\(x:A) (q:Id A a x) -> C x (q@-i)) d x (p@-i) -- General facts, that could be in other modules: -- Any path in U from A to B gives a function A->B: transp (A B : U) (p : Id U A B) (a : A) : B = comp p a [] -- The function A->A corresponding to the identity path refl U A is -- pointwise equal to the identity function (but not judgementally -- equal): refl' (A:U) (a:A) : Id A (transp A A (refl U A) a) a = comp (refl U A) a [(i=1) -> refl A a] -- The "computation rule" for J doesn't hold judgementally, but it -- does hold as follows, which we use implicitly: Jcomputation (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (c : C a (refl A a)) : Id (C a (refl A a)) (J A a C c a (refl A a)) c = refl' (C a (refl A a)) c -- Heterogenous equality IdP can be expressed in terms of equality Id using transp: funDepTr (A:U) (P:A->U) (a0 :A) : (a1:A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) -> Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transp (P a0) (P a1) ( P (p@i)) u0) u1) = J A a0 C rem where C (a1:A) (p:Id A a0 a1) : U = (u0:P a0) (u1:P a1) -> Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transp (P a0) (P a1) ( P (p@i)) u0) u1) rem (u0 u1:P a0) : Id U (Id (P a0) u0 u1) (Id (P a0) (transp (P a0) (P a0) (refl U (P a0)) u0) u1) = Id (P a0) (refl' (P a0) u0@-i) u1 -- This should be in the circle module. -- Induction on the circle: S1Induction (A : S1->U) (b : A base) (l : Id (A base) (subst S1 A base base loop1 b) b) : (x : S1) -> A x = split base -> b loop @ i -> (transp (Id (A base) (subst S1 A base base loop1 b) b) (IdP ( A (loop1 @ j)) b b) (funDepTr S1 A base base loop1 b b@-j) l ) @ i -- The computation rule for induction holds judgementally: S1InductionBase (A : S1 -> U) (b : A base) (l : Id (A base) (subst S1 A base base loop1 b) b) : Id (A base) (S1Induction A b l base) b = refl (A base) b -- 1. Factoring a family of functions -- f x : x = base -> A x such that f base is constant through 1. -- We need a general lemma with any easy proof, which doesn't depend -- on the circle or the constancy of f x, with a direct proof by based -- path induction. -- -- We apply it with X=S^1 and b=b'=base, r = refl S1 base, and l=loop. crucialLemma (X : U) (A : X -> U) (b : X) (r : Id X b b) (f : (x : X) -> Id X x b -> A x) (b': X) (l : Id X b b') : (q : Id X b' b) * Id (A b') (subst X A b b' l (f b r)) (f b' q) = h b' l where C (x : X) (l : Id X b x) : U = (q : Id X x b) * Id (A x) (subst X A b x l (f b r)) (f x q) hBase : C b (refl X b) = (r, refl' (A b) (f b r)) -- refl worked in regular ctt. h : (x : X) (l : Id X b x) -> C x l = J X b C hBase -- The following is data rather than property. An element of the -- type constant X A f may be called a modulus of constancy of the -- function f:X->A. constant (X A : U) (f:X->A) : U = (x y : X) -> Id A (f x) (f y) -- And this is the main theorem/construction, given in HoTT style first: factorFamily (A : S1 -> U) (f : (x : S1) -> Id S1 x base -> A x) (k : constant (Id S1 base base) (A base) (f base)) : (g : (x : S1) -> A x) * (x : S1) (p : Id S1 x base) -> Id (A x) (g x) (f x p) = (g, c) where b : A base = f base (refl S1 base) qs : (q : Id S1 base base) * Id (A base) (subst S1 A base base loop1 b) (f base q) = crucialLemma S1 A base (refl S1 base) f base loop1 q : Id S1 base base = qs.1 s : Id (A base) (subst S1 A base base loop1 b) (f base q) = qs.2 t : Id (A base) (f base q) b = k q (refl S1 base) l : Id (A base) (subst S1 A base base loop1 b) b = compId (A base) (subst S1 A base base loop1 b) (f base q) b s t g : (x : S1) -> A x = S1Induction A b l C (x : S1) (p : Id S1 x base) : U = Id (A x) (g x) (f x p) cbase : C base (refl S1 base) = refl (A base) b c : (x : S1) (p : Id S1 x base) -> C x p = J' S1 base C cbase -- And now with a proof in ctt style: crucialLemma' (X : U) (A : X -> U) (y : X) (f : (x : X) -> Id X x y -> A x) (l : Id X y y) : (x : X) (p : Id X y x) -> (r : Id X x y) * IdP ( A (p@i)) (f y l) (f x r) = J X y C (l, refl (A y) (f y l)) where C (x : X) (p : Id X y x) : U = (r : Id X x y) * IdP ( A (p@i)) (f y l) (f x r) factorFamily' (A : S1 -> U) (f : (x : S1) -> Id S1 x base -> A x) (k : constant (Id S1 base base) (A base) (f base)) : (g : (x : S1) -> A x) * (x : S1) (p : Id S1 x base) -> Id (A x) (g x) (f x p) = (g, c) where b : A base = f base (refl S1 base) P : Id U (A base) (A base) = A (loop1 @i) rs : (r : Id S1 base base) * IdP P b (f base r) = crucialLemma' S1 A base f (refl S1 base) base loop1 r : Id S1 base base = rs.1 s : IdP P b (f base r) = rs.2 t : Id (A base) (f base r) b = k r (refl S1 base) l : IdP P b b = transp (IdP P b (f base r)) (IdP P b b) ( IdP P b (t@i)) s g : (x:S1) -> A x = split base -> b loop @ i -> l @ i C (x : S1) (p : Id S1 x base) : U = Id (A x) (g x) (f x p) c : (x : S1) (p : Id S1 x base) -> C x p = J' S1 base C (refl (A base) (g base)) -- 2. Propositional truncations. data inh (A : U) = inc (a : A) | squash (u v : inh A) [(i=0) -> u, (i=1) -> v] -- Redefine squash: squash' (A:U) (u v : inh A) : Id (inh A) u v = ((squash{inh A} u v)@i) inhIsProp : (A:U) -> prop (inh A) = squash' -- 3. The generalized circle. data S(X:U) = beta (x:X) | ell (x y:X) [(i=0) -> beta x, (i=1) -> beta y] -- Redefine beta and ell: beta' (X:U) (x : X) : S X = beta x ell' (X:U) : constant X (S X) (beta' X) = \(x y : X) -> ((ell{S X} x y)@i) -- The type of constant functions ... Const (X A : U) : U = (f:X->A) * constant X A f -- ... is equal to the function type S X -> A: phiS (X A : U) (fc : Const X A) : S X -> A = split beta x -> fc.1 x ell x y @ i -> (fc.2 x y) @ i psiS (X A : U) (g:S X -> A) : Const X A = (\(x:X) -> g (beta x), \(x y:X) -> (g ((ell' X x y)@i))) -- The above maps are mutually inverse: phipsi (X A : U) (g: S X -> A) : Id (S X -> A) (phiS X A (psiS X A g)) g = \(u:S X) -> (rem u) @ i where rem : (u : S X) -> Id A (phiS X A (psiS X A g) u) (g u) = split beta x -> refl A (g (beta x)) ell x y @ i -> refl A (g ((ell' X x y) @ i)) -- with one of the composites definitionally equal to the identity: psiphi (X A : U)(fc : Const X A) : Id (Const X A) (psiS X A (phiS X A fc)) fc = refl (Const X A) fc -- Using isoId we get a path connecting them: Suniversal (X A : U) : Id U (S X -> A) (Const X A) = isoId (S X -> A) (Const X A) (psiS X A) (phiS X A) (psiphi X A) (phipsi X A) -- The type S X is connected. We need three lemmas: lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a : A) : (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1 = J A a f rem where f (a1 : A) (p : Id A a a1) : U = (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1 rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a lemPropFib (X:U) (P:S X -> U) (pP:(u:S X) -> prop (P u)) (bP:(x:X) -> P(beta x)) : (u:S X) -> P u = split beta x -> bP x ell x y @ i -> (lemPropF (S X) P pP (beta x) (beta y) (ell' X x y) (bP x) (bP y)) @ i lemConnect (X : U) (x:X) : (v:S X) -> inh (Id (S X) (beta x) v) = lemPropFib X (\(v:S X) -> inh (Id (S X) (beta x) v)) pP1 bP1 where pP1 (v:S X) : prop (inh (Id (S X) (beta x) v)) = inhIsProp (Id (S X) (beta x) v) bP1 (y:X) : inh (Id (S X) (beta x) (beta y)) = inc (ell' X x y) connectS (X:U) : (u v:S X) -> inh (Id (S X) u v) = lemPropFib X (\(u:S X) -> (v:S X) -> inh (Id (S X) u v)) pP (lemConnect X) where pP (u:S X) : prop ((v:S X) -> inh (Id (S X) u v)) = propPi (S X) (\(v:S X) -> inh (Id (S X) u v)) (\(v:S X) -> inhIsProp (Id (S X) u v)) -- The unit beta of the universal property is a surjection: surjS (X:U) (u:S X) : inh ((x:X) * Id (S X) (beta x) u) = lemPropFib X P pP bP u where T (u : S X) : U = (x:X) * Id (S X) (beta x) u P (u : S X) : U = inh (T u) pP (u:S X) : prop (P u) = inhIsProp (T u) bP (x : X) : P (beta x) = inc (x,refl (S X) (beta x)) -- The unit squash : X -> inh X of the propositional truncation inh X, -- being constant, factors through S X: factorInhBeta (X : U) : S X -> inh X = split beta x -> inc x ell x y @ i -> (squash' X (inc x) (inc y)) @ i -- 4. Factoring a single constant function f:x0=base->A through 1. -- We consider a special case of of the family of functions beta: Beta (x : S1) (p : Id S1 x base) : S(Id S1 x base) = beta p -- We can factor it through 1 to get a family of function Beta': BetaFactor : (Beta' : (x : S1) -> S(Id S1 x base)) * (x : S1) (p : Id S1 x base) -> Id (S(Id S1 x base)) (Beta' x) (Beta x p) = factorFamily (\(x : S1) -> S(Id S1 x base)) Beta (\(x : S1) -> ell' (Id S1 x base)) -- We extract the two compotents of the pair: Beta' : (x : S1) -> S(Id S1 x base) = BetaFactor.1 BetaConstancy : (x : S1) (p : Id S1 x base) -> Id (S(Id S1 x base)) (Beta' x) (Beta x p) = BetaFactor.2 -- With this we can factor any constant function f:x0=base->A through -- the unit type 1, i.e. give a point of A that is the common value of -- f for all arguments: factorSingle (x0 : S1) (A : U) (f : Id S1 x0 base -> A) (k : constant (Id S1 x0 base) A f) : (a : A) * (p : Id S1 x0 base) -> Id A a (f p) = (a , c) where f': S(Id S1 x0 base) -> A = phiS (Id S1 x0 base) A (f , k) a : A = f'(Beta' x0) c (p : Id S1 x0 base) : Id A a (f'(Beta x0 p)) = mapOnPath (S(Id S1 x0 base)) A f' (Beta' x0) (Beta x0 p) (BetaConstancy x0 p) -- Simple-minded test for the moment: pt : S1 = transp S1 S1 (refl U S1) base test : bool = (factorSingle pt bool (\(x:Id S1 pt base) -> true) (\(x y:Id S1 pt base) -> true)).1