|
|
|
@ -66,12 +66,12 @@ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type |
|
|
|
-- Path. |
|
|
|
|
|
|
|
Path : {A : Type} -> A -> A -> Type |
|
|
|
Path {A} = PathP (\i -> A) |
|
|
|
Path = PathP (\i -> A) |
|
|
|
|
|
|
|
-- reflexivity is given by constant paths |
|
|
|
|
|
|
|
refl : {A : Type} {x : A} -> Path x x |
|
|
|
refl {A} {x} i = x |
|
|
|
refl i = x |
|
|
|
|
|
|
|
-- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that |
|
|
|
-- sym p i0 = p (inot i0) = p i1 |
|
|
|
@ -111,7 +111,7 @@ isContr A = (x : A) * ((y : A) -> Path x y) |
|
|
|
-- singletons are contracible. Together with transport later on, |
|
|
|
-- we get the J elimination principle of paths. |
|
|
|
singContr : {A : Type} {a : A} -> isContr (Singl A a) |
|
|
|
singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j))) |
|
|
|
singContr = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j))) |
|
|
|
|
|
|
|
-- Some more operations on paths. By rearranging parentheses we get a |
|
|
|
-- proof that the images of equal elements are themselves equal. |
|
|
|
@ -186,6 +186,9 @@ Partial : I -> Type -> Pretype |
|
|
|
PartialP : (phi : I) -> Partial phi Type -> Pretype |
|
|
|
{-# PRIMITIVE PartialP #-} |
|
|
|
|
|
|
|
partialExt : {A : Type} (phi : I) (psi : I) -> Partial phi A -> Partial psi A -> Partial (ior phi psi) A |
|
|
|
{-# PRIMITIVE partialExt #-} |
|
|
|
|
|
|
|
-- Why is Partial φ A not just defined as φ -> A? The difference is that |
|
|
|
-- Partial φ A has an internal representation which definitionally relates |
|
|
|
-- any two partial elements which "agree everywhere", that is, have |
|
|
|
@ -202,7 +205,7 @@ PartialP : (phi : I) -> Partial phi Type -> Pretype |
|
|
|
-- That is, element of A[phi -> u] is an element of A defined everywhere |
|
|
|
-- (a total element), which, when IsOne φ, agrees with u. |
|
|
|
|
|
|
|
Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype |
|
|
|
Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype |
|
|
|
{-# PRIMITIVE Sub #-} |
|
|
|
|
|
|
|
-- Every total element u : A can be made partial on φ by ignoring the |
|
|
|
@ -227,7 +230,7 @@ primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub ( |
|
|
|
{-# PRIMITIVE comp primComp #-} |
|
|
|
|
|
|
|
comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1 |
|
|
|
comp A {phi} u a0 = outS (primComp A {phi} u a0) |
|
|
|
comp A u a0 = outS (primComp A {phi} u a0) |
|
|
|
|
|
|
|
-- In particular, when φ is a disjunction of the form |
|
|
|
-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a |
|
|
|
@ -257,18 +260,12 @@ comp A {phi} u a0 = outS (primComp A {phi} u a0) |
|
|
|
-- x----------y |
|
|
|
-- p i |
|
|
|
|
|
|
|
trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z |
|
|
|
trans {A} {x} p q i = |
|
|
|
comp (\i -> A) |
|
|
|
{ior i (inot i)} |
|
|
|
(\j [ (i = i0) -> x, (i = i1) -> q j ]) |
|
|
|
(inS (p i)) |
|
|
|
|
|
|
|
-- In particular when the formula φ = i0 we get the "opposite face" to a |
|
|
|
-- single point, which corresponds to transport. |
|
|
|
|
|
|
|
transp : (A : I -> Type) (x : A i0) -> A i1 |
|
|
|
transp A x = comp A {i0} (\i [ ]) (inS x) |
|
|
|
transp A x = comp A (\i [ ]) (inS x) |
|
|
|
|
|
|
|
subst : {A : Type} (P : A -> Type) {x : A} {y : A} -> Path x y -> P x -> P y |
|
|
|
subst P p x = transp (\i -> P (p i)) x |
|
|
|
@ -278,19 +275,28 @@ subst P p x = transp (\i -> P (p i)) x |
|
|
|
|
|
|
|
fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) (a0 : Sub (A i0) phi (u i0)) |
|
|
|
-> PathP A (outS a0) (comp A {phi} u a0) |
|
|
|
fill A {phi} u a0 i = |
|
|
|
fill A u a0 i = |
|
|
|
comp (\j -> A (iand i j)) |
|
|
|
{ior phi (inot i)} |
|
|
|
(\j [ (phi = i1) -> u (iand i j) itIs1 |
|
|
|
, (i = i0) -> outS a0 |
|
|
|
, (i = i0) -> outS {A i0} {phi} {u i0} a0 |
|
|
|
]) |
|
|
|
(inS (outS a0)) |
|
|
|
|
|
|
|
hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A |
|
|
|
hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0 |
|
|
|
hcomp u a0 = comp (\i -> A) {phi} u a0 |
|
|
|
|
|
|
|
hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> Path (outS a0) (hcomp u a0) |
|
|
|
hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i |
|
|
|
hfill u a0 i = fill (\i -> A) {phi} u a0 i |
|
|
|
|
|
|
|
|
|
|
|
trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z |
|
|
|
trans p q i = comp (\j -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> q k ]) (inS {A} {ior i (inot i)} (p i)) |
|
|
|
|
|
|
|
transFiller : {A : Type} {x : A} {y : A} {z : A} |
|
|
|
-> (p : Path x y) (q : Path y z) |
|
|
|
-> PathP (\i -> Path x (q i)) p (trans {A} {x} {y} {z} p q) |
|
|
|
transFiller p q j i = hfill (\k [ (i = i0) -> x, (i = i1) -> q k ]) (inS (p i)) j |
|
|
|
|
|
|
|
-- For instance, the filler of the previous composition square |
|
|
|
-- tells us that trans p refl = p: |
|
|
|
@ -301,18 +307,18 @@ transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) |
|
|
|
rightCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p (sym p)) refl |
|
|
|
rightCancel p j i = cube p i1 j i where |
|
|
|
cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A |
|
|
|
cube {A} {x} p k j i = |
|
|
|
hfill {A} (\ k [ (i = i0) -> x |
|
|
|
, (i = i1) -> p (iand (inot k) (inot j)) |
|
|
|
, (j = i1) -> x |
|
|
|
]) |
|
|
|
(inS (p (iand i (inot j)))) k |
|
|
|
cube p k j i = |
|
|
|
hfill (\ k [ (i = i0) -> x |
|
|
|
, (i = i1) -> p (iand (inot k) (inot j)) |
|
|
|
, (j = i1) -> x |
|
|
|
]) |
|
|
|
(inS (p (iand i (inot j)))) k |
|
|
|
|
|
|
|
leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl |
|
|
|
leftCancel p = rightCancel (sym p) |
|
|
|
|
|
|
|
transpFill : {A : I -> Type} (x : A i0) -> PathP A x (transp (\i -> A i) x) |
|
|
|
transpFill {A} x i = fill (\i -> A i) (\k []) (inS x) i |
|
|
|
transpFill : (A : I -> Type) (x : A i0) -> PathP A x (transp (\i -> A i) x) |
|
|
|
transpFill A x i = fill (\i -> A i) (\k []) (inS x) i |
|
|
|
|
|
|
|
-- Reduction of composition |
|
|
|
--------------------------- |
|
|
|
@ -365,7 +371,7 @@ invert : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A |
|
|
|
invert eqv y = (eqv y) .1 .1 |
|
|
|
|
|
|
|
retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type |
|
|
|
retract {A} {B} f g = (a : A) -> Path (g (f a)) a |
|
|
|
retract f g = (a : A) -> Path (g (f a)) a |
|
|
|
|
|
|
|
-- Proving that it's also a retraction is left as an exercise to the |
|
|
|
-- reader. We can package together a function and a proof that it's an |
|
|
|
@ -377,7 +383,7 @@ Equiv A B = (f : A -> B) * isEquiv {A} {B} f |
|
|
|
-- The identity function is an equivalence between any type A and |
|
|
|
-- itself. |
|
|
|
idEquiv : {A : Type} -> Equiv A A |
|
|
|
idEquiv {A} = (\x -> x, \y -> ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))) |
|
|
|
idEquiv = (\x -> x, \y -> ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))) |
|
|
|
|
|
|
|
-- The glue operation expresses that "extensibility is invariant under |
|
|
|
-- equivalence". Less concisely, the Glue type and its constructor, |
|
|
|
@ -400,7 +406,7 @@ primGlue : (A : Type) {phi : I} |
|
|
|
-- Agreeing with the condition that Glue A [i1 -> (T, e)] = T, |
|
|
|
-- we have that glue {A} {i1} t im => t. |
|
|
|
prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} |
|
|
|
-> (t : PartialP phi T) |
|
|
|
-> (t : PartialP phi (\o -> T o)) |
|
|
|
-> (im : Sub A phi (\o -> (e o).1 (t o))) |
|
|
|
-> primGlue A T e |
|
|
|
|
|
|
|
@ -410,7 +416,7 @@ glue : {A : Type} {phi : I} {Te : Partial phi ((T : Type) * Equiv T A)} |
|
|
|
-> (t : PartialP phi (\o -> (Te o).1)) |
|
|
|
-> (im : Sub A phi (\o -> (Te o).2.1 (t o))) |
|
|
|
-> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2) |
|
|
|
glue {A} {phi} {Te} t im = prim'glue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} t im |
|
|
|
glue t im = prim'glue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} t im |
|
|
|
|
|
|
|
-- The unglue operation undoes a glueing. Since when φ = i1, |
|
|
|
-- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ... |
|
|
|
@ -424,7 +430,7 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o - |
|
|
|
|
|
|
|
unglue : {A : Type} (phi : I) {Te : Partial phi ((T : Type) * Equiv T A)} |
|
|
|
-> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2) -> A |
|
|
|
unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} |
|
|
|
unglue phi = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} |
|
|
|
|
|
|
|
-- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn |
|
|
|
-- as giving us the dotted line in: |
|
|
|
@ -445,7 +451,7 @@ unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} |
|
|
|
-- equivalences, we can make a line between two types (T i0) and (T i1). |
|
|
|
|
|
|
|
Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type |
|
|
|
Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2) |
|
|
|
Glue A u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2) |
|
|
|
|
|
|
|
-- For example, we can glue together the type A and the type B as long |
|
|
|
-- as there exists an Equiv A B. |
|
|
|
@ -460,9 +466,9 @@ Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2) |
|
|
|
-- \i → B |
|
|
|
-- |
|
|
|
ua : {A : Type} {B : Type} -> Equiv A B -> Path A B |
|
|
|
ua {A} {B} equiv i = |
|
|
|
Glue B (\[ (i = i0) -> (A, equiv), |
|
|
|
(i = i1) -> (B, idEquiv) ]) |
|
|
|
ua equiv i = |
|
|
|
Glue B (\[ (i = i0) -> (A, equiv) |
|
|
|
, (i = i1) -> (B, idEquiv) ]) |
|
|
|
|
|
|
|
lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1) |
|
|
|
{-# PRIMITIVE lineToEquiv #-} |
|
|
|
@ -493,7 +499,7 @@ isEquivTransport A = (lineToEquiv A).2 |
|
|
|
-- we need to come up with a filler for the Bottom and right faces. |
|
|
|
|
|
|
|
uaBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> ua f i)) f.1 |
|
|
|
uaBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i) |
|
|
|
uaBeta f i a = transpFill (\i -> B) (f.1 a) (inot i) |
|
|
|
|
|
|
|
-- The terms ua + uaBeta suffice to prove the "full" |
|
|
|
-- ua axiom of Voevodsky, as can be seen in the paper |
|
|
|
@ -513,7 +519,7 @@ JRefl : {A : Type} {x : A} |
|
|
|
(P : (y : A) -> Path x y -> Type) |
|
|
|
(d : P x (\i -> x)) |
|
|
|
-> Path (J {A} {x} P d {x} (\i -> x)) d |
|
|
|
JRefl P d i = transpFill {\i -> P x (\j -> x)} d (inot i) |
|
|
|
JRefl P d i = transpFill (\i -> P x (\j -> x)) d (inot i) |
|
|
|
|
|
|
|
Jay : {A : Type} {x : A} |
|
|
|
(P : ((y : A) * Path x y) -> Type) |
|
|
|
@ -532,7 +538,7 @@ Jay P d s = transp (\i -> P ((singContr {A} {x}).2 s i)) d |
|
|
|
-- definition of equivalence. |
|
|
|
|
|
|
|
isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type |
|
|
|
isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x) |
|
|
|
isIso f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x) |
|
|
|
|
|
|
|
-- The reason is that the family of types IsIso is not a proposition! |
|
|
|
-- This means that there can be more than one way for a function to be |
|
|
|
@ -548,7 +554,7 @@ Iso A B = (f : A -> B) * isIso f |
|
|
|
-- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55 |
|
|
|
|
|
|
|
IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B |
|
|
|
IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where |
|
|
|
IsoToEquiv iso = (f, \y -> (fCenter y, fIsCenter y)) where |
|
|
|
f = iso.1 |
|
|
|
g = iso.2.1 |
|
|
|
s = iso.2.2.1 |
|
|
|
@ -559,47 +565,47 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where |
|
|
|
lemIso y x0 x1 p0 p1 = |
|
|
|
let |
|
|
|
rem0 : Path x0 (g y) |
|
|
|
rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 (inot i)))) |
|
|
|
rem0 i = hcomp (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 (inot i)))) |
|
|
|
|
|
|
|
rem1 : Path x1 (g y) |
|
|
|
rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i)))) |
|
|
|
rem1 i = hcomp (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i)))) |
|
|
|
|
|
|
|
p : Path x0 x1 |
|
|
|
p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) |
|
|
|
p i = hcomp (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) |
|
|
|
|
|
|
|
fill0 : I -> I -> A |
|
|
|
fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k) |
|
|
|
, (i = i1) -> g y |
|
|
|
, (j = i0) -> g (p0 (inot i)) |
|
|
|
]) |
|
|
|
(inS (g (p0 (inot i)))) |
|
|
|
fill0 i j = hcomp (\k [ (i = i0) -> t x0 (iand j k) |
|
|
|
, (i = i1) -> g y |
|
|
|
, (j = i0) -> g (p0 (inot i)) |
|
|
|
]) |
|
|
|
(inS (g (p0 (inot i)))) |
|
|
|
|
|
|
|
fill1 : I -> I -> A |
|
|
|
fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k) |
|
|
|
, (i = i1) -> g y |
|
|
|
, (j = i0) -> g (p1 (inot i)) ]) |
|
|
|
(inS (g (p1 (inot i)))) |
|
|
|
fill1 i j = hcomp (\k [ (i = i0) -> t x1 (iand j k) |
|
|
|
, (i = i1) -> g y |
|
|
|
, (j = i0) -> g (p1 (inot i)) ]) |
|
|
|
(inS (g (p1 (inot i)))) |
|
|
|
|
|
|
|
fill2 : I -> I -> A |
|
|
|
fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k)) |
|
|
|
, (i = i1) -> rem1 (ior j (inot k)) |
|
|
|
, (j = i1) -> g y ]) |
|
|
|
(inS (g y)) |
|
|
|
fill2 i j = hcomp (\k [ (i = i0) -> rem0 (ior j (inot k)) |
|
|
|
, (i = i1) -> rem1 (ior j (inot k)) |
|
|
|
, (j = i1) -> g y ]) |
|
|
|
(inS (g y)) |
|
|
|
|
|
|
|
sq : I -> I -> A |
|
|
|
sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k) |
|
|
|
, (i = i1) -> fill1 j (inot k) |
|
|
|
, (j = i1) -> g y |
|
|
|
, (j = i0) -> t (p i) (inot k) ]) |
|
|
|
(inS (fill2 i j)) |
|
|
|
sq i j = hcomp (\k [ (i = i0) -> fill0 j (inot k) |
|
|
|
, (i = i1) -> fill1 j (inot k) |
|
|
|
, (j = i1) -> g y |
|
|
|
, (j = i0) -> t (p i) (inot k) ]) |
|
|
|
(inS (fill2 i j)) |
|
|
|
|
|
|
|
sq1 : I -> I -> B |
|
|
|
sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 (inot j)) k |
|
|
|
, (i = i1) -> s (p1 (inot j)) k |
|
|
|
, (j = i0) -> s (f (p i)) k |
|
|
|
, (j = i1) -> s y k |
|
|
|
]) |
|
|
|
(inS (f (sq i j))) |
|
|
|
sq1 i j = hcomp (\k [ (i = i0) -> s (p0 (inot j)) k |
|
|
|
, (i = i1) -> s (p1 (inot j)) k |
|
|
|
, (j = i0) -> s (f (p i)) k |
|
|
|
, (j = i1) -> s y k |
|
|
|
]) |
|
|
|
(inS (f (sq i j))) |
|
|
|
in \i -> (p i, \j -> sq1 i (inot j)) |
|
|
|
|
|
|
|
fCenter : (y : B) -> fiber f y |
|
|
|
@ -615,7 +621,7 @@ IsoToId i = ua (IsoToEquiv i) |
|
|
|
-- such a function is its own inverse. |
|
|
|
|
|
|
|
involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f |
|
|
|
involToIso {A} f inv = (f, inv, inv) |
|
|
|
involToIso f inv = (f, inv, inv) |
|
|
|
|
|
|
|
-- An example of ua |
|
|
|
--------------------------- |
|
|
|
@ -720,7 +726,7 @@ universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl |
|
|
|
-- extensionality. The strong version is as follows: |
|
|
|
|
|
|
|
Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type |
|
|
|
Hom {A} f g = (x : A) -> Path (f x) (g x) |
|
|
|
Hom f g = (x : A) -> Path (f x) (g x) |
|
|
|
|
|
|
|
happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} |
|
|
|
-> (p : Path f g) -> Hom f g |
|
|
|
@ -730,11 +736,11 @@ happly p x i = p i x |
|
|
|
|
|
|
|
happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} |
|
|
|
-> isIso {Path f g} {Hom f g} happly |
|
|
|
happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl) |
|
|
|
happlyIsIso = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl) |
|
|
|
|
|
|
|
pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} |
|
|
|
-> Path (Path f g) (Hom f g) |
|
|
|
pathIsHom {A} {B} {f} {g} = |
|
|
|
pathIsHom = |
|
|
|
let |
|
|
|
theIso : Iso (Path f g) (Hom f g) |
|
|
|
theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g}) |
|
|
|
@ -978,7 +984,7 @@ poSusp : Type -> Type |
|
|
|
poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt) |
|
|
|
|
|
|
|
Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A) |
|
|
|
Susp_is_poSusp {A} = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where |
|
|
|
Susp_is_poSusp = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where |
|
|
|
poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A |
|
|
|
poSusp_to_Susp = \case |
|
|
|
inl x -> north |
|
|
|
@ -1014,8 +1020,8 @@ data T2 : Type where |
|
|
|
(i = i1) -> pathOne j |
|
|
|
] |
|
|
|
|
|
|
|
TorusIsTwoCircles : Path T2 (S1 * S1) |
|
|
|
TorusIsTwoCircles = ua (IsoToEquiv theIso) where |
|
|
|
TorusIsTwoCircles : Equiv T2 (S1 * S1) |
|
|
|
TorusIsTwoCircles = IsoToEquiv theIso where |
|
|
|
torusToCircs : T2 -> S1 * S1 |
|
|
|
torusToCircs = \case |
|
|
|
baseT -> (base, base) |
|
|
|
@ -1143,11 +1149,11 @@ isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i |
|
|
|
isProp_isContr : {A : Type} -> isProp (isContr A) |
|
|
|
isProp_isContr {A} z0 z1 j = |
|
|
|
( z0.2 z1.1 j |
|
|
|
, \x i -> hcomp {A} (\k [ (i = i0) -> z0.2 z1.1 j |
|
|
|
, (i = i1) -> z0.2 x (ior j k) |
|
|
|
, (j = i0) -> z0.2 x (iand i k) |
|
|
|
, (j = i1) -> z1.2 x i ]) |
|
|
|
(inS (z0.2 (z1.2 x i) j)) |
|
|
|
, \x i -> hcomp (\k [ (i = i0) -> z0.2 z1.1 j |
|
|
|
, (i = i1) -> z0.2 x (ior j k) |
|
|
|
, (j = i0) -> z0.2 x (iand i k) |
|
|
|
, (j = i1) -> z1.2 x i ]) |
|
|
|
(inS (z0.2 (z1.2 x i) j)) |
|
|
|
) |
|
|
|
|
|
|
|
isContr_isProp : {A : Type} -> isContr A -> isProp A |
|
|
|
@ -1170,7 +1176,7 @@ propExt {A} {B} propA propB f g = (f, contract) where |
|
|
|
let arg : A |
|
|
|
arg = g y |
|
|
|
in ( (arg, propB y (f arg)) |
|
|
|
, \fib -> sigmaPath (propA _ _) (isProp_isSet {B} propB y (f fib.1) _ _)) |
|
|
|
, \fib -> sigmaPath (propA _ _) (isProp_isSet propB y (f fib.1) _ _)) |
|
|
|
|
|
|
|
Sq_rec : {A : Type} {B : Type} |
|
|
|
-> isProp B |
|
|
|
@ -1185,6 +1191,9 @@ Sq_rec prop f = |
|
|
|
work = \case |
|
|
|
inc x -> f x |
|
|
|
|
|
|
|
Sq_prop : {A : Type} -> isProp (Sq A) |
|
|
|
Sq_prop x y i = sq x y i |
|
|
|
|
|
|
|
hitTranspExample : Path (inc false) (inc true) |
|
|
|
hitTranspExample i = transp (\i -> Sq (notp i)) (sq (inc true) (inc false) i) |
|
|
|
|
|
|
|
@ -1201,12 +1210,12 @@ S2IsSuspS1 = ua (IsoToEquiv iso) where |
|
|
|
loop j -> \i -> surf2 i j |
|
|
|
|
|
|
|
suspSurf : I -> I -> I -> Susp S1 |
|
|
|
suspSurf i j = hfill {Susp S1} (\k [ (i = i0) -> north |
|
|
|
, (i = i1) -> merid base (inot k) |
|
|
|
, (j = i0) -> merid base (iand (inot k) i) |
|
|
|
, (j = i1) -> merid {S1} base (iand (inot k) i) |
|
|
|
]) |
|
|
|
(inS (merid (loop j) i)) |
|
|
|
suspSurf i j = hfill (\k [ (i = i0) -> north {S1} |
|
|
|
, (i = i1) -> merid {S1} base (inot k) |
|
|
|
, (j = i0) -> merid {S1} base (iand (inot k) i) |
|
|
|
, (j = i1) -> merid {S1} base (iand (inot k) i) |
|
|
|
]) |
|
|
|
(inS (merid (loop j) i)) |
|
|
|
|
|
|
|
fromS2 : S2 -> Susp S1 |
|
|
|
fromS2 = \case { base2 -> north; surf2 i j -> suspSurf i j i1 } |
|
|
|
@ -1237,14 +1246,14 @@ S3IsSuspS2 = ua (IsoToEquiv iso) where |
|
|
|
surf2 j k -> \i -> surf3 i j k |
|
|
|
|
|
|
|
suspSurf : I -> I -> I -> I -> Susp S2 |
|
|
|
suspSurf i j k = hfill {Susp S2} (\l [ (i = i0) -> north |
|
|
|
, (i = i1) -> merid base2 (inot l) |
|
|
|
, (j = i0) -> merid base2 (iand (inot l) i) |
|
|
|
, (j = i1) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
, (k = i0) -> merid base2 (iand (inot l) i) |
|
|
|
, (k = i1) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
]) |
|
|
|
(inS (merid (surf2 j k) i)) |
|
|
|
suspSurf i j k = hfill (\l [ (i = i0) -> north {S2} |
|
|
|
, (i = i1) -> merid {S2} base2 (inot l) |
|
|
|
, (j = i0) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
, (j = i1) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
, (k = i0) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
, (k = i1) -> merid {S2} base2 (iand (inot l) i) |
|
|
|
]) |
|
|
|
(inS (merid (surf2 j k) i)) |
|
|
|
|
|
|
|
fromS3 : S3 -> Susp S2 |
|
|
|
fromS3 = \case { base3 -> north; surf3 i j k -> suspSurf i j k i1 } |
|
|
|
@ -1263,24 +1272,24 @@ S3IsSuspS2 = ua (IsoToEquiv iso) where |
|
|
|
iso = (fromS3, toS3, fromToS3, toFromS3) |
|
|
|
|
|
|
|
ap_s : {A : Pretype} {B : Pretype} (f : A -> B) {x : A} {y : A} -> Eq_s x y -> Eq_s (f x) (f y) |
|
|
|
ap_s {A} {B} f {x} {y} = J_s (\y p -> Eq_s (f x) (f y)) refl_s |
|
|
|
ap_s f {x} = J_s (\y p -> Eq_s (f x) (f y)) refl_s |
|
|
|
|
|
|
|
subst_s : {A : Pretype} (P : A -> Pretype) {x : A} {y : A} -> Eq_s x y -> P x -> P y |
|
|
|
subst_s {A} P {x} {z} p px = J_s {A} {x} (\y p -> P x -> P y) id p px |
|
|
|
subst_s {A} P {x} p px = J_s (\y p -> P x -> P y) id p px |
|
|
|
|
|
|
|
sym_s : {A : Pretype} {x : A} {y : A} -> Eq_s x y -> Eq_s y x |
|
|
|
sym_s {A} {x} {y} = J_s {A} {x} (\y p -> Eq_s y x) refl_s |
|
|
|
sym_s = J_s (\y p -> Eq_s y x) refl_s |
|
|
|
|
|
|
|
UIP : {A : Pretype} {x : A} {y : A} (p : Eq_s x y) (q : Eq_s x y) -> Eq_s p q |
|
|
|
UIP {A} {x} {y} p q = J_s (\y p -> (q : Eq_s x y) -> Eq_s p q) (uipRefl A x) p q where |
|
|
|
UIP p q = J_s (\y p -> (q : Eq_s x y) -> Eq_s p q) (uipRefl A x) p q where |
|
|
|
uipRefl : (A : Pretype) (x : A) (p : Eq_s x x) -> Eq_s refl_s p |
|
|
|
uipRefl A x p = K_s {A} {x} (\q -> Eq_s refl_s q) refl_s p |
|
|
|
uipRefl A x p = K_s (\q -> Eq_s refl_s q) refl_s p |
|
|
|
|
|
|
|
strictEq_pathEq : {A : Type} {x : A} {y : A} -> Eq_s x y -> Path x y |
|
|
|
strictEq_pathEq {A} {x} {y} eq = J_s {A} {x} (\y p -> Path x y) (\i -> x) {y} eq |
|
|
|
strictEq_pathEq eq = J_s {A} {x} (\y p -> Path x y) (\i -> x) {y} eq |
|
|
|
|
|
|
|
seq_pathRefl : {A : Type} {x : A} (p : Eq_s x x) -> Eq_s (strictEq_pathEq p) (refl {A} {x}) |
|
|
|
seq_pathRefl {A} {x} p = K_s (\p -> Eq_s (strictEq_pathEq {A} {x} {x} p) (refl {A} {x})) refl_s p |
|
|
|
seq_pathRefl p = K_s (\p -> Eq_s (strictEq_pathEq {A} {x} {x} p) (refl {A} {x})) refl_s p |
|
|
|
|
|
|
|
Path_nat_strict_nat : (x : Nat) (y : Nat) -> Path x y -> Eq_s x y |
|
|
|
Path_nat_strict_nat = \case { zero -> zeroCase; succ x -> succCase x } where |
|
|
|
@ -1296,7 +1305,7 @@ Path_nat_strict_nat = \case { zero -> zeroCase; succ x -> succCase x } where |
|
|
|
pathToEqS_K : {A : Type} {x : A} |
|
|
|
-> (s : {x : A} {y : A} -> Path x y -> Eq_s x y) |
|
|
|
-> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p |
|
|
|
pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop where |
|
|
|
pathToEqS_K p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop where |
|
|
|
psloop : P (strictEq_pathEq (p_to_s loop)) |
|
|
|
psloop = K_s (\l -> P (strictEq_pathEq {A} {x} {x} l)) pr (p_to_s {x} {x} loop) |
|
|
|
|
|
|
|
@ -1306,7 +1315,7 @@ pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop wh |
|
|
|
aux = seq_pathRefl (p_to_s (\i -> x)) |
|
|
|
|
|
|
|
pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isHSet A |
|
|
|
pathToEq_isSet {A} p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where |
|
|
|
pathToEq_isSet p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where |
|
|
|
axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isHSet A |
|
|
|
axK_to_isSet K x y p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where |
|
|
|
uipRefl : (x : A) (p : Path x x) -> Path refl p |
|
|
|
@ -1334,34 +1343,33 @@ equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B) |
|
|
|
equivCtrPath e y = (e.2 y).2 |
|
|
|
|
|
|
|
contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u |
|
|
|
contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) -> p.2 (u itIs1) i ]) (inS p.1) |
|
|
|
contr p u = primComp (\i -> A) (\i [ (phi = i1) -> p.2 (u itIs1) i ]) (inS p.1) |
|
|
|
|
|
|
|
contr' : {A : Type} -> ({phi : I} -> (u : Partial phi A) -> Sub A phi u) -> isContr A |
|
|
|
contr' {A} contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where |
|
|
|
contr' contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where |
|
|
|
x : A |
|
|
|
x = outS (contr (\ [])) |
|
|
|
|
|
|
|
leftIsOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s (ior a b) i1 |
|
|
|
leftIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior i b)) refl_s (sym_s p) |
|
|
|
leftIsOne p = J_s {I} {i1} (\i p -> IsOne (ior i b)) refl_s (sym_s p) |
|
|
|
|
|
|
|
rightIsOne : {a : I} {b : I} -> Eq_s b i1 -> Eq_s (ior a b) i1 |
|
|
|
rightIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p) |
|
|
|
rightIsOne p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p) |
|
|
|
|
|
|
|
bothAreOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s b i1 -> Eq_s (iand a b) i1 |
|
|
|
bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p) |
|
|
|
bothAreOne p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p) |
|
|
|
|
|
|
|
S1Map_to_baseLoop : {X : Type} -> (S1 -> X) -> (a : X) * Path a a |
|
|
|
S1Map_to_baseLoop {X} f = (f base, \i -> f (loop i)) |
|
|
|
S1Map_to_baseLoop f = (f base, \i -> f (loop i)) |
|
|
|
|
|
|
|
baseLoop_to_S1Map : {X : Type} -> ((a : X) * Path a a) -> S1 -> X |
|
|
|
baseLoop_to_S1Map {X} p = \case |
|
|
|
base -> p.1 |
|
|
|
loop i -> p.2 i |
|
|
|
|
|
|
|
S1_univ : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a) |
|
|
|
S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, baseLoop_to_S1Map, ret, sec) where |
|
|
|
S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, fro, ret, sec) where |
|
|
|
to = S1Map_to_baseLoop |
|
|
|
fro = baseLoop_to_S1Map |
|
|
|
fro : {X : Type} -> ((a : X) * Path a a) -> S1 -> X |
|
|
|
fro p = \case |
|
|
|
base -> p.1 |
|
|
|
loop i -> p.2 i |
|
|
|
|
|
|
|
sec : {X : Type} -> (f : S1 -> X) -> Path (fro (to f)) f |
|
|
|
sec {X} f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where |
|
|
|
@ -1386,7 +1394,7 @@ encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode _, encDe |
|
|
|
encode alpha = transp (\i -> code (alpha i)) c0 |
|
|
|
|
|
|
|
encodeRefl : Path (encode refl) c0 |
|
|
|
encodeRefl = sym (transpFill {\i -> code a0} c0) |
|
|
|
encodeRefl = sym (transpFill (\i -> code a0) c0) |
|
|
|
|
|
|
|
decEnc : {x : A} (p : Path a0 x) -> Path (decode _ (encode p)) p |
|
|
|
decEnc p = J (\x p -> Path (decode _ (encode p)) p) q p where |
|
|
|
@ -1402,7 +1410,7 @@ S1_elim P pb pq = \case |
|
|
|
loop i -> pq i |
|
|
|
|
|
|
|
PathP_is_Path : (P : I -> Type) (p : P i0) (q : P i1) -> Path (PathP P p q) (Path {P i1} (transp (\i -> P i) p) q) |
|
|
|
PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill {\j -> P j} p i) q |
|
|
|
PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill (\j -> P j) p i) q |
|
|
|
|
|
|
|
Constant : {A : Type} {B : Type} -> (A -> B) -> Type |
|
|
|
Constant f = (y : B) * (x : A) -> Path y (f x) |
|
|
|
@ -1417,7 +1425,7 @@ Constant_weakly : {A : Type} {B : Type} (f : A -> B) -> Constant f -> Weakly f |
|
|
|
Constant_weakly f p x y = trans (sym (p.2 x)) (p.2 y) |
|
|
|
|
|
|
|
Constant_conditionally : {A : Type} {B : Type} -> (f : A -> B) -> Constant f -> Conditionally f |
|
|
|
Constant_conditionally {A} {B} f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where |
|
|
|
Constant_conditionally f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where |
|
|
|
c_const : Path f (\y -> p.1) |
|
|
|
c_const i x = p.2 x (inot i) |
|
|
|
|
|
|
|
@ -1441,7 +1449,7 @@ S1_connected f = (f'.1, p) where |
|
|
|
(Bool_isSet _ _ rr (transp (\i -> P (loop i)) rr)) |
|
|
|
|
|
|
|
isProp_isEquiv : {A : Type} {B : Type} {f : A -> B} -> isProp (isEquiv f) |
|
|
|
isProp_isEquiv {f} p q i y = |
|
|
|
isProp_isEquiv p q i y = |
|
|
|
let |
|
|
|
p2 = (p y).2 |
|
|
|
q2 = (q y).2 |
|
|
|
@ -1462,10 +1470,10 @@ isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp ( |
|
|
|
equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B} |
|
|
|
-> Path e.1 e'.1 |
|
|
|
-> Path e e' |
|
|
|
equivLemma {A} {B} {e} {e'} p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2) |
|
|
|
equivLemma p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2) |
|
|
|
|
|
|
|
isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P) |
|
|
|
isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where |
|
|
|
isProp_to_Sq_equiv prop = propExt prop sqProp inc proj where |
|
|
|
proj : Sq P -> P |
|
|
|
proj = Sq_rec prop (\x -> x) |
|
|
|
|
|
|
|
@ -1476,69 +1484,58 @@ Sq_equiv_to_isProp : {P : Type} -> Equiv P (Sq P) -> isProp P |
|
|
|
Sq_equiv_to_isProp eqv = transp (\i -> isProp (ua eqv (inot i))) (\x y i -> sq x y i) |
|
|
|
|
|
|
|
exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P)) |
|
|
|
exercise_3_21 {P} = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp |
|
|
|
exercise_3_21 = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp |
|
|
|
|
|
|
|
uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (ua {A} {B}) (idToEquiv {A} {B}) |
|
|
|
uaret eqv = equivLemma (uaBeta eqv) |
|
|
|
|
|
|
|
f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B |
|
|
|
f1 {A} p = (p.1, ua p.2) |
|
|
|
|
|
|
|
f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B |
|
|
|
f2 {A} p = (p.1, idToEquiv p.2) |
|
|
|
|
|
|
|
uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a |
|
|
|
uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2) |
|
|
|
|
|
|
|
isContrRetract : {A : Type} {B : Type} |
|
|
|
-> (f : A -> B) -> (g : B -> A) |
|
|
|
-> (h : retract f g) |
|
|
|
-> isContr B -> isContr A |
|
|
|
isContrRetract {A} {B} f g h v = (g b, p) where |
|
|
|
isContrRetract f g h v = (g b, p) where |
|
|
|
b = v.1 |
|
|
|
|
|
|
|
p : (x : A) -> Path (g b) x |
|
|
|
p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i))) |
|
|
|
|
|
|
|
contrEquivSingl : {A : Type} -> isContr ((B : Type) * Equiv A B) |
|
|
|
contrEquivSingl = isContrRetract f1 f2 uaretSig singContr where |
|
|
|
f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B |
|
|
|
f1 p = (p.1, ua p.2) |
|
|
|
|
|
|
|
f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B |
|
|
|
f2 p = (p.1, idToEquiv p.2) |
|
|
|
|
|
|
|
uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a |
|
|
|
uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2) |
|
|
|
|
|
|
|
curry : {A : Type} {B : A -> Type} {C : (x : A) -> B x -> Type} |
|
|
|
-> Path ((x : A) (y : B x) -> C x y) ((p : (x : A) * B x) -> C p.1 p.2) |
|
|
|
curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where |
|
|
|
curry = IsoToId (to, from, \f -> refl, \g -> refl) where |
|
|
|
to : ((x : A) (y : B x) -> C x y) -> (p : (x : A) * B x) -> C p.1 p.2 |
|
|
|
to f p = f p.1 p.2 |
|
|
|
|
|
|
|
from : ((p : (x : A) * B x) -> C p.1 p.2) -> (x : A) (y : B x) -> C x y |
|
|
|
from f x y = f (x, y) |
|
|
|
|
|
|
|
ContractibleIfInhabited : {A : Type} -> Path (A -> isContr A) (isProp A) |
|
|
|
ContractibleIfInhabited {A} = IsoToId (to, from, toFrom, fromTo) where |
|
|
|
to : (A -> isContr A) -> isProp A |
|
|
|
to cont x y = trans (sym (p.2 x)) (p.2 y) where |
|
|
|
p = cont x |
|
|
|
contrToProp : {A : Type} -> (A -> isContr A) -> isProp A |
|
|
|
contrToProp cont x y = trans (sym (p.2 x)) (p.2 y) where |
|
|
|
p = cont x |
|
|
|
|
|
|
|
ContractibleIfInhabited : {A : Type} -> isEquiv contrToProp |
|
|
|
ContractibleIfInhabited = (IsoToEquiv (contrToProp, from, toFrom, fromTo)).2 where |
|
|
|
from : isProp A -> A -> isContr A |
|
|
|
from prop x = (x, prop x) |
|
|
|
|
|
|
|
toFrom : (y : isProp A) -> Path (to (from y)) y |
|
|
|
toFrom y = isProp_isProp {A} (to (from y)) y |
|
|
|
|
|
|
|
fromTo : (y : A -> isContr A) -> Path (from (to y)) y |
|
|
|
fromTo y i a = isProp_isContr {A} (from (to y) a) (y a) i |
|
|
|
toFrom : (y : isProp A) -> Path (contrToProp (from y)) y |
|
|
|
toFrom y = isProp_isProp {A} (contrToProp (from y)) y |
|
|
|
|
|
|
|
data cone (A : Type) : Type where |
|
|
|
point : cone A |
|
|
|
base : A -> cone A |
|
|
|
side i : (x : A) -> cone A [ (i = i0) -> point, (i = i1) -> base x ] |
|
|
|
|
|
|
|
ConeA_contr : {A : Type} -> isContr (cone A) |
|
|
|
ConeA_contr {A} = (point, contr) where |
|
|
|
contr : (y : cone A) -> Path point y |
|
|
|
contr = \case |
|
|
|
point -> refl |
|
|
|
base x -> \i -> side x i |
|
|
|
side x i -> \j -> side x (iand i j) |
|
|
|
fromTo : (y : A -> isContr A) -> Path (from (contrToProp y)) y |
|
|
|
fromTo y i a = isProp_isContr {A} (from (contrToProp y) a) (y a) i |
|
|
|
|
|
|
|
contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B) |
|
|
|
contrSinglEquiv {B} = (center, contract) where |
|
|
|
contrSinglEquiv = (center, contract) where |
|
|
|
center : (A : Type) * Equiv A B |
|
|
|
center = (B, idEquiv) |
|
|
|
|
|
|
|
@ -1564,51 +1561,75 @@ contrSinglEquiv {B} = (center, contract) where |
|
|
|
contr : (v : fiber unglueB b) -> Path ctr v |
|
|
|
contr v j = ( glue {B} {ior (inot i) i} {sys} |
|
|
|
(\[ (i = i0) -> v.2 j, (i = i1) -> ((w.2.2 b).2 v j).1 ]) |
|
|
|
(inS (comp (\i -> B) |
|
|
|
(\k [ (i = i0) -> v.2 (iand j k) |
|
|
|
, (i = i1) -> ((w.2.2 b).2 v j).2 k |
|
|
|
, (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k |
|
|
|
, (j = i1) -> v.2 k |
|
|
|
]) |
|
|
|
(inS b))) |
|
|
|
, fill (\j -> B) (\k [ (i = i0) -> v.2 (iand j k) |
|
|
|
, (i = i1) -> ((w.2.2 b).2 v j).2 k |
|
|
|
, (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k |
|
|
|
, (j = i1) -> v.2 k |
|
|
|
]) |
|
|
|
(inS b) |
|
|
|
(inS (hcomp (\k [ (i = i0) -> v.2 (iand j k) |
|
|
|
, (i = i1) -> ((w.2.2 b).2 v j).2 k |
|
|
|
, (j = i0) -> fill (\j -> B) |
|
|
|
{ior i (inot i)} |
|
|
|
(\k [ (i = i0) -> b |
|
|
|
, (i = i1) -> (w.2.2 b).1.2 k ]) |
|
|
|
(inS {B} {ior i (inot i)} b) k |
|
|
|
, (j = i1) -> v.2 k |
|
|
|
]) |
|
|
|
(inS b))) |
|
|
|
, hfill (\k [ (i = i0) -> v.2 (iand j k) |
|
|
|
, (i = i1) -> ((w.2.2 b).2 v j).2 k |
|
|
|
, (j = i0) -> fill (\j -> B) |
|
|
|
{ior i (inot i)} |
|
|
|
(\k [ (i = i0) -> b |
|
|
|
, (i = i1) -> (w.2.2 b).1.2 k ]) |
|
|
|
(inS {B} {ior i (inot i)} b) k |
|
|
|
, (j = i1) -> v.2 k |
|
|
|
]) |
|
|
|
(inS b) |
|
|
|
) |
|
|
|
in (ctr, contr) |
|
|
|
in (GlueB, unglueB, unglueEquiv) |
|
|
|
|
|
|
|
uaIdEquiv : {A : Type} -> Path (ua idEquiv) (\i -> A) |
|
|
|
uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv)) |
|
|
|
uaIdEquiv i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv)) |
|
|
|
|
|
|
|
EquivJ : (P : (X : Type) (Y : Type) -> Equiv X Y -> Type) |
|
|
|
-> ((X : Type) -> P X X idEquiv) |
|
|
|
-> {X : Type} {Y : Type} (E : Equiv X Y) |
|
|
|
-> P X Y E |
|
|
|
EquivJ P p {X} {Y} E = |
|
|
|
EquivJ P p E = |
|
|
|
subst {(X : Type) * Equiv X Y} |
|
|
|
(\x -> P x.1 Y x.2) |
|
|
|
(\i -> isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) i) |
|
|
|
(p Y) |
|
|
|
|
|
|
|
EquivJ_domain : {Y : Type} (P : (X : Type) -> Equiv X Y -> Type) |
|
|
|
-> P Y idEquiv |
|
|
|
-> {X : Type} (E : Equiv X Y) |
|
|
|
-> P X E |
|
|
|
EquivJ_domain P p E = subst {(X : Type) * Equiv X Y} (\x -> P x.1 x.2) q p where |
|
|
|
q : Path {(X : Type) * Equiv X Y} (Y, idEquiv) (X, E) |
|
|
|
q = isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) |
|
|
|
|
|
|
|
EquivJ_range : {X : Type} (P : (Y : Type) -> Equiv X Y -> Type) |
|
|
|
-> P X idEquiv |
|
|
|
-> {Y : Type} (E : Equiv X Y) |
|
|
|
-> P Y E |
|
|
|
EquivJ_range P p E = subst {(Y : Type) * Equiv X Y} (\x -> P x.1 x.2) q p |
|
|
|
where |
|
|
|
q : Path {(Y : Type) * Equiv X Y} (X, idEquiv) (Y, E) |
|
|
|
q = isContr_isProp {(Y : Type) * Equiv X Y} (contrEquivSingl {X}) (X, idEquiv) (Y, E) |
|
|
|
|
|
|
|
pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B |
|
|
|
pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) idEquiv |
|
|
|
pathToEquiv = J {Type} {A} (\B p -> Equiv A B) idEquiv |
|
|
|
|
|
|
|
univalence : {A : Type} {B : Type} -> Equiv (Path A B) (Equiv A B) |
|
|
|
univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where |
|
|
|
pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) idEquiv |
|
|
|
pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) idEquiv |
|
|
|
pathToEquiv_refl = JRefl (\B p -> Equiv A B) idEquiv |
|
|
|
|
|
|
|
ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p |
|
|
|
ua_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where |
|
|
|
ua_pathToEquiv p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where |
|
|
|
lemma : Path (ua (pathToEquiv (\i -> A))) (\i -> A) |
|
|
|
lemma = transp (\i -> Path (ua (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv |
|
|
|
|
|
|
|
pathToEquiv_ua : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (ua p)) p |
|
|
|
pathToEquiv_ua {A} {B} p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where |
|
|
|
pathToEquiv_ua p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where |
|
|
|
lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv |
|
|
|
lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl |
|
|
|
|
|
|
|
@ -1621,19 +1642,18 @@ total_fibers : {A : Type} {P : A -> Type} {Q : A -> Type} |
|
|
|
-> {xv : (a : A) * Q a} |
|
|
|
-> (f : (el : A) -> P el -> Q el) |
|
|
|
-> Iso (fiber (total f) xv) (fiber (f xv.1) xv.2) |
|
|
|
total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where |
|
|
|
total_fibers f = (to, fro, toFro {xv}, froTo) where |
|
|
|
to : {xv : (a : A) * Q a} -> fiber (total f) xv -> fiber (f xv.1) xv.2 |
|
|
|
to peq = J {(a : A) * Q a} {_} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2) |
|
|
|
to peq = J {(a : A) * Q a} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2) |
|
|
|
|
|
|
|
fro : {xv : (a : A) * Q a} -> fiber (f xv.1) xv.2 -> fiber (total f) xv |
|
|
|
fro peq = ((xv.1, peq.1), \i -> (_, peq.2 i)) |
|
|
|
|
|
|
|
toFro : {xv : (a : A) * Q a} -> (y : fiber (f xv.1) xv.2) -> Path (to (fro y)) y |
|
|
|
toFro {xv} peq = |
|
|
|
J {Q xv.1} {f xv.1 p} |
|
|
|
toFro peq = |
|
|
|
J {_} {f xv.1 p} |
|
|
|
(\xv1 eq1 -> Path (to {(xv.1, xv1)} (fro (p, sym eq1))) (p, sym eq1)) |
|
|
|
(JRefl {(a : A) * Q a} {(xv.1, f xv.1 peq.1)} |
|
|
|
(\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)) |
|
|
|
(JRefl {(a : A) * Q a} {(_, _)} (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)) |
|
|
|
(sym eq) |
|
|
|
where p : P xv.1 |
|
|
|
p = peq.1 |
|
|
|
@ -1642,9 +1662,9 @@ total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where |
|
|
|
eq = peq.2 |
|
|
|
|
|
|
|
froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y |
|
|
|
froTo {xv} apeq = |
|
|
|
froTo apeq = |
|
|
|
J {(a : A) * Q a} {total f (a, p)} |
|
|
|
(\xv1 eq1 -> Path (fro {_} (to {_} ((a, p), sym eq1))) ((a, p), sym eq1)) |
|
|
|
(\xv1 eq1 -> Path (fro (to ((a, p), sym eq1))) ((a, p), sym eq1)) |
|
|
|
(ap fro (JRefl {(a : A) * Q a} {(a, _)} |
|
|
|
(\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))) |
|
|
|
(sym eq) |
|
|
|
@ -1669,22 +1689,162 @@ totalEquiv : {A : Type} {P : A -> Type} {Q : A -> Type} |
|
|
|
-> (f : (el : A) -> P el -> Q el) |
|
|
|
-> ((x : A) -> isEquiv (f x)) |
|
|
|
-> isEquiv (total f) |
|
|
|
totalEquiv f iseqv xv = isContrRetract {fiber (total f) xv} {fiber (f xv.1) xv.2} eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where |
|
|
|
totalEquiv f iseqv xv = isContrRetract eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where |
|
|
|
eqv : Iso (fiber (total f) xv) (fiber (f xv.1) xv.2) |
|
|
|
eqv = total_fibers f |
|
|
|
|
|
|
|
contrIsEquiv : {A : Type} {B : Type} -> isContr A -> isContr B |
|
|
|
-> (f : A -> B) -> isEquiv f |
|
|
|
contrIsEquiv cA cB f y = ((cA.1, isContr_isProp cB _ _), \v -> sigmaPath (isContr_isProp cA _ _) (isProp_isSet (isContr_isProp cB) _ _ _ v.2)) |
|
|
|
contrIsEquiv cA cB f y = |
|
|
|
( (cA.1, isContr_isProp cB _ _) |
|
|
|
, \v -> sigmaPath (isContr_isProp cA _ _) |
|
|
|
(isProp_isSet (isContr_isProp cB) _ _ _ v.2) |
|
|
|
) |
|
|
|
|
|
|
|
theorem722 : {A : Type} {R : A -> A -> Type} |
|
|
|
-> ((x : A) (y : A) -> isProp (R x y)) |
|
|
|
-> ({x : A} -> R x x) |
|
|
|
-> (f : (x : A) (y : A) -> R x y -> Path x y) |
|
|
|
-> {x : A} {y : A} -> isEquiv {R x y} {Path x y} (f x y) |
|
|
|
theorem722 {A} {R} prop rho toId {x} {y} = fiberEquiv {A} {R x} {Path x} (toId x) (totalEquiv x) y where |
|
|
|
theorem722 prop rho toId {x} {y} = fiberEquiv (toId x) (totalEquiv x) y where |
|
|
|
rContr : (x : A) -> isContr ((y : A) * R x y) |
|
|
|
rContr x = ((x, rho {x}), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2)) |
|
|
|
|
|
|
|
totalEquiv : (x : A) -> isEquiv (total {A} {R x} {Path x} (toId x)) |
|
|
|
totalEquiv x = contrIsEquiv (rContr x) singContr (total {A} {R x} {Path x} (toId x)) |
|
|
|
totalEquiv : (x : A) -> isEquiv (total (toId x)) |
|
|
|
totalEquiv x = contrIsEquiv (rContr x) singContr (total (toId x)) |
|
|
|
|
|
|
|
lemma492 : {A : Type} {B : Type} {X : Type} |
|
|
|
-> (e : Equiv A B) |
|
|
|
-> isEquiv {X -> A} {X -> B} (\f x -> e.1 (f x)) |
|
|
|
lemma492 = |
|
|
|
EquivJ (\A B e -> isEquiv {X -> _} {X -> B} (\f x -> e.1 (f x))) |
|
|
|
(\R -> (idEquiv {X -> R}).2) |
|
|
|
|
|
|
|
twoOutOfThree_1 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C} |
|
|
|
-> isEquiv f |
|
|
|
-> isEquiv g |
|
|
|
-> isEquiv (\x -> g (f x)) |
|
|
|
twoOutOfThree_1 feq geq = |
|
|
|
EquivJ_range (\_ g -> isEquiv (\x -> g.1 (f x))) feq (g, geq) |
|
|
|
|
|
|
|
twoOutOfThree_2 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C} |
|
|
|
-> isEquiv f |
|
|
|
-> isEquiv (\x -> g (f x)) |
|
|
|
-> isEquiv g |
|
|
|
twoOutOfThree_2 feq gofeq = |
|
|
|
EquivJ_domain (\_ f -> isEquiv (\x -> g (f.1 x)) -> isEquiv g) id (f, feq) gofeq |
|
|
|
|
|
|
|
twoOutOfThree_3 : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : B -> C} |
|
|
|
-> isEquiv g |
|
|
|
-> isEquiv (\x -> g (f x)) |
|
|
|
-> isEquiv f |
|
|
|
twoOutOfThree_3 geq gofeq = |
|
|
|
EquivJ_range (\_ g -> isEquiv (\x -> g.1 (f x)) -> isEquiv f) id (g, geq) gofeq |
|
|
|
|
|
|
|
equivalence_isEmbedding : {A : Type} {B : Type} |
|
|
|
-> {f : A -> B} |
|
|
|
-> isEquiv f |
|
|
|
-> {x : A} {y : A} |
|
|
|
-> isEquiv (ap f {x} {y}) |
|
|
|
equivalence_isEmbedding feqv {x} {y} = |
|
|
|
EquivJ (\A B eq -> (x : A) (y : A) -> isEquiv {_} {Path (eq.1 x) (eq.1 y)} (ap eq.1)) (\X x y -> (idEquiv {Path _ _}).2) (f, feqv) x y |
|
|
|
|
|
|
|
isOfHLevel : Type -> Nat -> Type |
|
|
|
isOfHLevel A = \case |
|
|
|
zero -> (a : A) (b : A) -> Path a b |
|
|
|
succ n -> (a : A) (b : A) -> isOfHLevel (Path a b) n |
|
|
|
|
|
|
|
Sphere : Nat -> Type |
|
|
|
Sphere = \case |
|
|
|
zero -> Bottom |
|
|
|
succ n -> Susp (Sphere n) |
|
|
|
|
|
|
|
sphereFull : {A : Type} {n : Nat} (f : Sphere n -> A) -> Type |
|
|
|
sphereFull f = (top : A) * (x : Sphere n) -> Path top (f x) |
|
|
|
|
|
|
|
spheresFull : {n : Nat} -> Type -> Type |
|
|
|
spheresFull A = (f : Sphere n -> A) -> sphereFull f |
|
|
|
|
|
|
|
spheresFull_hLevel : {A : Type} (n : Nat) -> spheresFull {succ n} A -> isOfHLevel A n |
|
|
|
spheresFull_hLevel = |
|
|
|
\case |
|
|
|
zero -> \full a b -> |
|
|
|
let f : Sphere (succ zero) -> A |
|
|
|
f = \case |
|
|
|
north -> a |
|
|
|
south -> b |
|
|
|
merid u i -> absurd u |
|
|
|
p = (full f).2 |
|
|
|
in trans (sym (p north)) (p south) |
|
|
|
succ n -> \h x y -> spheresFull_hLevel n (helper h x y) |
|
|
|
where |
|
|
|
helper : {n : Nat} -> spheresFull {succ (succ n)} A -> (x : A) (y : A) -> spheresFull {succ n} (Path x y) |
|
|
|
helper h x y f = (trans p q, r (transFiller p q)) where |
|
|
|
f' : Susp (Sphere (succ n)) -> A |
|
|
|
f' = \case |
|
|
|
north -> x |
|
|
|
south -> y |
|
|
|
merid u i -> f u i |
|
|
|
|
|
|
|
p : Path x (h f').1 |
|
|
|
p i = (h f').2 north (inot i) |
|
|
|
|
|
|
|
q : Path (h f').1 y |
|
|
|
q = (h f').2 south |
|
|
|
|
|
|
|
r : (fillpq : PathP (\i -> Path x (q i)) p (trans p q)) |
|
|
|
(s : Sphere (succ n)) |
|
|
|
-> Path (fillpq i1) (f s) |
|
|
|
r fillpq s i j = hcomp (\k [ (i = i0) -> fillpq k j |
|
|
|
, (i = i1) -> (h f').2 (merid s j) k |
|
|
|
, (j = i0) -> p (iand (inot k) i) |
|
|
|
, (j = i1) -> q k ]) |
|
|
|
(inS (p (ior i j))) |
|
|
|
|
|
|
|
isOfHLevel_hasSpheres : {A : Type} (n : Nat) -> isOfHLevel A n -> spheresFull {succ n} A |
|
|
|
isOfHLevel_hasSpheres = |
|
|
|
\case |
|
|
|
zero -> \prop f -> (f north, \x -> prop (f north) (f x)) |
|
|
|
succ n -> \h -> helper {n} (\x y -> isOfHLevel_hasSpheres n (h x y)) |
|
|
|
where |
|
|
|
helper : {n : Nat} -> ((a : A) (b : A) -> spheresFull {succ n} (Path a b)) |
|
|
|
-> spheresFull {succ (succ n)} A |
|
|
|
helper {n} h f = (f north, r) where |
|
|
|
north' = north {Sphere (succ n)} |
|
|
|
south' = south {Sphere (succ n)} |
|
|
|
merid' = merid {Sphere (succ n)} |
|
|
|
|
|
|
|
r : (x : Sphere (succ (succ n))) -> Path (f north) (f x) |
|
|
|
r = \case |
|
|
|
north -> refl |
|
|
|
south -> (h (f north') (f south') (\x i -> f (merid x i))).1 |
|
|
|
merid x i -> \j -> |
|
|
|
hcomp (\k [ (i = i0) -> f north' |
|
|
|
, (i = i1) -> (h (f north') (f south') (\x i -> f (merid' x i))).2 x (inot k) j |
|
|
|
, (j = i0) -> f north' |
|
|
|
, (j = i1) -> f (merid' x i) ]) |
|
|
|
(inS (f (merid' x (iand i j)))) |
|
|
|
|
|
|
|
data nTrunc (A : Type) (n : Nat) : Type where |
|
|
|
incn : A -> nTrunc A n |
|
|
|
hub : (f : Sphere (succ n) -> nTrunc A n) -> nTrunc A n |
|
|
|
spoke i : (f : Sphere (succ n) -> nTrunc A n) (x : Sphere (succ n)) -> nTrunc A n [ (i = i0) -> hub f, (i = i1) -> f x ] |
|
|
|
|
|
|
|
nTrunc_isOfHLevel : {A : Type} {n : Nat} -> isOfHLevel (nTrunc A n) n |
|
|
|
nTrunc_isOfHLevel = spheresFull_hLevel {nTrunc A n} n (\f -> (hub f, \x i -> spoke f x i)) |
|
|
|
|
|
|
|
nTrunc_rec : {A : Type} {n : Nat} {B : Type} |
|
|
|
-> isOfHLevel B n |
|
|
|
-> (A -> B) |
|
|
|
-> nTrunc A n -> B |
|
|
|
nTrunc_rec bofhl f = go (isOfHLevel_hasSpheres n bofhl) where |
|
|
|
work : (p : spheresFull {succ n} B) -> nTrunc A n -> B |
|
|
|
work p = \case |
|
|
|
hub sph -> (p (\x -> work p (sph x))).1 |
|
|
|
incn x -> f x |
|
|
|
|
|
|
|
go : (p : spheresFull {succ n} B) -> nTrunc A n -> B |
|
|
|
go p = \case |
|
|
|
incn x -> f x |
|
|
|
hub sph -> (p (\x -> work p (sph x))).1 |
|
|
|
spoke sph cell i -> (p (\x -> work p (sph x))).2 cell i |
