From 4eb27da0bf4335ee87ac4d9d2c5e8a11d960fc99 Mon Sep 17 00:00:00 2001 From: Thierry Coquand Date: Wed, 27 Apr 2016 11:22:34 +0200 Subject: [PATCH] we should improve the evaluator --- examples/injective.ctt | 104 +++++++++++++++++++++++ examples/subset.ctt | 189 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 293 insertions(+) create mode 100644 examples/injective.ctt create mode 100644 examples/subset.ctt diff --git a/examples/injective.ctt b/examples/injective.ctt new file mode 100644 index 0000000..631051c --- /dev/null +++ b/examples/injective.ctt @@ -0,0 +1,104 @@ +module injective where + +import prelude +import prop + + +-- First definition of injectivity, informally: if two elements f a0, f a1 are +-- equal in B, then a0, a1 must be equal in A. +inj0 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : U + = (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1 + +-- Second definition of injectivity, informally: for any b in B, there are +-- only one elment a in A such that f a is equal to b. +inj1 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : U + = (b : B) -> prop ((a : A) * Id B (f a) b) + +-- A map from the first to the second definition. +inj01 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : inj0 A B f sA sB -> + inj1 A B f sA sB + = \ (i0 : inj0 A B f sA sB) (b : B) (c d : (a : A) * Id B (f a) b) -> let + F (a : A) : U + = Id B (f a) b + pF (a : A) : prop (F a) + = sB (f a) b + p : Id B (f c.1) (f d.1) + = comp ( B) (c.2 @ i) [ (i = 0) -> f c.1 + , (i = 1) -> d.2 @ -j ] + q : Id A c.1 d.1 + = i0 c.1 d.1 p + in + lemSig A F pF c d q + +-- A map from the second to the first definition. +inj10 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : inj1 A B f sA sB -> + inj0 A B f sA sB + = \ (i1 : inj1 A B f sA sB) (a0 a1 : A) (p : Id B (f a0) (f a1)) -> let + c : (a : A) * Id B (f a) (f a1) + = (a0, p) + d : (a : A) * Id B (f a) (f a1) + = (a1, f a1) + q : Id ((a : A) * Id B (f a) (f a1)) c d + = i1 (f a1) c d + fst : ((a : A) * Id B (f a) (f a1)) -> A + = \ (x : (a : A) * Id B (f a) (f a1)) -> x.1 + in + fst (q @ i) + +-- A proof that the first definition of injectivity is a proposition. +prop_inj0 (A B : U) (f : A -> B) (sA : set A) (sB : set B) + : prop (inj0 A B f sA sB) + = let + c (a0 a1 : A) : prop (Id B (f a0) (f a1) -> Id A a0 a1) + = let + P : Id B (f a0) (f a1) -> U + = \ (_ : Id B (f a0) (f a1)) -> Id A a0 a1 + h : (x : Id B (f a0) (f a1)) -> prop (P x) + = \ (_ : Id B (f a0) (f a1)) -> sA a0 a1 + in + propPi (Id B (f a0) (f a1)) P h + d (a0 : A) : prop ((a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1) + = let + P : A -> U + = \ (a1 : A) -> ( Id B (f a0) (f a1) -> Id A a0 a1 ) + h : (a1 : A) -> prop (P a1) + = \ (a1 : A) -> c a0 a1 + in + propPi A P h + e : prop (inj0 A B f sA sB) + = let + P : A -> U + = \ (a0 : A) -> ( (a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1 ) + h : (a0 : A) -> prop ( (a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1 ) + = \ (a0 : A) -> d a0 + in + propPi A P h + in + e + +-- A proof that the second definition of injectivity is a proposition. +prop_inj1 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : + prop (inj1 A B f sA sB) + = let + P : B -> U + = \ (b : B) -> (a : A) * Id B (f a) b + Q : B -> U + = \ (b : B) -> prop (P b) + h : (b : B) -> prop (Q b) + = \ (b : B) -> propIsProp (P b) + in + propPi B Q h + +-- A proof that two propositions with maps between them can be identified with +-- each other +propId (A B : U) (f : A -> B) (g : B -> A) (pA : prop A) (pB : prop B) : + Id U A B + = isoId A B f g (\ (b : B) -> pB (f (g b)) b) (\ (a : A) -> pA (g (f a)) a) + +-- A proof that the two definitions of injectivity can be identified with each +-- other +injId (A B : U) (f : A -> B) (sA : set A) (sB : set B) : + Id U (inj0 A B f sA sB) (inj1 A B f sA sB) + = propId (inj0 A B f sA sB) (inj1 A B f sA sB) + (inj01 A B f sA sB) (inj10 A B f sA sB) + (prop_inj0 A B f sA sB) (prop_inj1 A B f sA sB) \ No newline at end of file diff --git a/examples/subset.ctt b/examples/subset.ctt new file mode 100644 index 0000000..8845828 --- /dev/null +++ b/examples/subset.ctt @@ -0,0 +1,189 @@ +module subset where + +import prelude +import injective +import sigma +import univalence + + +-- The first definition of a subset. Informally, there exists a second set B +-- and an injective function from B to A. +subset0 (A : U) (sA : set A) : U + = (B : U) * (sB : set B) * (f : B -> A) * (inj1 B A f sB sA) + +-- The second definition of a subset. Informally, each element of A is tagged +-- with a proposition indicating whether its included in the subset or not. +subset1 (A : U) (sA : set A) : U + = (a : A) -> (X : U) * (prop X) + +-- A map from the first to the second definition of subsets. +subset01 (A : U) (sA : set A) : subset0 A sA -> subset1 A sA + = \ (s : subset0 A sA) (a : A) -> let + -- Take apart s + B : U + = s.1 + sB : set B + = s.2.1 + f : B -> A + = s.2.2.1 + i : inj1 B A f sB sA + = s.2.2.2 + -- Construct a proposition to tag the element a with + X : U + = (b : B) * (Id A (f b) a) + pX : prop X + = i a + in + (X, pX) + +-- A map from the second to the first definition of subsets. +subset10 (A : U) (sA : set A) + : subset1 A sA -> subset0 A sA + = \ (P : subset1 A sA) -> let + -- Construct a predicate on A + Q : (a : A) -> U + = \ (a : A) -> (P a).1 + -- Tag each element of A with the predicate Q to construct B + B : U + = (a : A) * Q a + -- Show that the predicate Q is a set (this follows from it being a + -- proposition) + sQ (a : A) : set (Q a) + = propSet (Q a) (P a).2 + -- Using that A and Q are sets we show that B is a set as well. + sB : set B + = setSig A Q sA sQ + -- Construct a map from B to A by taking the first projection of B. + f : B -> A + = \ (b : B) -> b.1 + -- Show that f is injective. + inj : inj1 B A f sB sA + = \ (a : A) (c d : (b : B) * Id A (f b) a) -> let + p : Id A c.1.1 d.1.1 + = comp ( A) (c.2 @ i) [ (i = 0) -> c.1.1 + , (i = 1) -> d.2 @ -j ] + q : Id B c.1 d.1 + = lem A Q (\ (x : A) -> (P x).2) c.1 d.1 p + r : Id ((b : B) * Id A (f b) a) c d + = lem B (\(b : B) -> Id A (f b) a) (\ (b : B) -> sA (f b) a) c d q + in + r + in + (B, sB, f, inj) + +-- Show that subset10 ∘ subset01 can be identified with the identity function +subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) -> + Id (subset0 A sA) (subset10 A sA (subset01 A sA s0)) s0 + = \ (s0 : subset0 A sA) -> let +-- TEMP : Id (subset0 A sA) (subset10 A sA (subset01 A sA s0)) s0 = undefined + s0' + : subset0 A sA + = subset10 A sA (subset01 A sA s0) + -- Take apart s0 and s0' + B : U + = s0.1 + B' : U + = s0'.1 + sB : set B + = s0.2.1 + sB' : set B' + = s0'.2.1 + f : B -> A + = s0.2.2.1 + f' : B' -> A + = s0'.2.2.1 + inj : inj1 B A f sB sA + = s0.2.2.2 + inj' : inj1 B' A f' sB' sA + = s0'.2.2.2 + -- Show that B' and B are equivalent + g (b : B) : B' + = (f b, b, f b) + g' (b' : B') : B + = b'.2.1 + s (x : B) : Id B (g' (g x)) x + = x + t (x : B') : Id B' (g (g' x)) x + = (x.2.2 @ i, x.2.1, x.2.2 @ i /\ j) + -- Compute a path between B' and B, as well as a path between f'∘g∘g' and f + P (X : U) (h: X -> B) : U + = (p : Id U X B) * (IdP ( p @ i -> A) (\ (x : X) -> f' (g (h x))) f) + q : P B' g' + = elimEquiv B P ( B, f) B' (g', gradLemma B' B g' g s t) + idB : Id U B' B + = q.1 + -- Show that sB can be identified with sB' + idsB : IdP ( set (idB @ i)) sB' sB + -- = lemPropF U set setIsProp B' B idB sB' sB + = undefined + -- Show that f' can be identified with f. This follows from g∘g' ⇔ \x -> x + -- and that there is a path q.2 between f'∘g∘g' and f + idf : IdP ( idB @ i -> A) f' f + = let + TEMP : IdP ( idB @ i -> A) f' f = undefined + Q (h : B' -> B') : U + = IdP ( q.1 @ i -> A) (\ (x : B') -> f' (h x)) f + a : B' -> B' = \ (x : B') -> g (g' x) + b : B' -> B' = \ (x : B') -> x + p : Id (B' -> B') a b = \ (x : B') -> (t x) @ i + in + -- subst (B' -> B') Q a b p q.2 + TEMP + -- Show that inj can be identified with inj' + idinj : IdP ( inj1 (idB @ i) A (idf @ i) (idsB @ i) sA) inj' inj + = let + TEMP : IdP ( inj1 (idB @ i) A (idf @ i) (idsB @ i) sA) inj' inj = undefined + T : U + = (X : U) * (_ : X -> A) * (set X) + P : T -> U + = \ (t : T) -> inj1 t.1 A t.2.1 t.2.2 sA + pP : (t : T) -> prop (P t) + = \ (t : T) -> prop_inj1 t.1 A t.2.1 t.2.2 sA + t0 : T + = (B', f', sB') + t1 : T + = (B, f, sB) + idT : Id T t0 t1 + = (idB @ i, idf @ i, idsB @ i) + in + -- lemPropF T P pP t0 t1 idT inj' inj + TEMP + in + (idB @ i, idsB @ i, idf @ i, idinj @ i) + -- TEMP + +-- Show that subset10 ∘ subset01 can be identified with the identity function +subsetIso1 (A : U) (sA : set A) : (s1 : subset1 A sA) -> + Id (subset1 A sA) (subset01 A sA (subset10 A sA s1)) s1 + = \ (s1 : subset1 A sA) -> let + -- Construct the second subset s1' from s1. + s1' : subset1 A sA + = subset01 A sA (subset10 A sA s1) + -- Show that s1' and s1 produces the same result for all a : A + ids1 : (a : A) -> Id ((X : U) * (prop X)) (s1' a) (s1 a) + = \ (a : A) -> let + -- Construct isomorphism between (s1' a).1 and (s1 a).1 to show that + -- (s1' a).1 can be identified with (s1 a).1 + f : (s1' a).1 -> (s1 a).1 + = \ (x : (s1' a).1) -> subst A (\(a : A) -> (s1 a).1) x.1.1 a x.2 x.1.2 + g : (s1 a).1 -> (s1' a).1 + = \ (x : (s1 a).1) -> ((a, x), a) + s : (x : (s1 a).1) -> Id (s1 a).1 (f (g x)) x + = \ (x : (s1 a).1) -> (s1 a).2 (f (g x)) x + t : (x : (s1' a).1) -> Id (s1' a).1 (g (f x)) x + = \ (x : (s1' a).1) -> (s1' a).2 (g (f x)) x + p : Id U (s1' a).1 (s1 a).1 + = isoId (s1' a).1 (s1 a).1 f g s t + -- Show that for x : prop (s1' a).1, y : prop (s1 a).1, + -- x can be identified with y. + q : IdP ( prop (p @ i)) (s1' a).2 (s1 a).2 + = lemPropF U prop propIsProp (s1' a).1 (s1 a).1 p (s1' a).2 (s1 a).2 + in + (p @ i, q @ i) + in + funExt A (\ (_ : A) -> (X : U) * (prop X)) s1' s1 ids1 + +-- Show that we can identify the two definitions of subsets with each other +subsetId (A : U) (sA : set A) : Id U (subset0 A sA) (subset1 A sA) + = isoId (subset0 A sA) (subset1 A sA) (subset01 A sA) (subset10 A sA) + (subsetIso1 A sA) (subsetIso0 A sA) \ No newline at end of file -- 2.34.1