|
-- We begin by adding some primitive bindings using the PRIMITIVE pragma.
|
|
--
|
|
-- It goes like this: PRIMITIVE primName varName.
|
|
--
|
|
-- If the varName is dropped, then it's taken to be the same as primName.
|
|
--
|
|
-- If there is a previous declaration for the varName, then the type
|
|
-- is checked against the internally-known "proper" type for the primitive.
|
|
|
|
-- Universe of fibrant types
|
|
{-# PRIMITIVE Type #-}
|
|
|
|
-- Universe of non-fibrant types
|
|
{-# PRIMITIVE Pretype #-}
|
|
|
|
-- Fibrant is a fancy word for "has a composition structure". Most types
|
|
-- we inherit from MLTT are fibrant:
|
|
--
|
|
-- Stuff like products Π, sums Σ, naturals, booleans, lists, etc., all
|
|
-- have composition structures.
|
|
--
|
|
-- The non-fibrant types are part of the structure of cubical
|
|
-- categories: The interval, partial elements, cubical subtypes, ...
|
|
|
|
-- The interval
|
|
---------------
|
|
|
|
-- The interval has two endpoints i0 and i1.
|
|
-- These form a de Morgan algebra.
|
|
I : Pretype
|
|
{-# PRIMITIVE Interval I #-}
|
|
|
|
i0, i1 : I
|
|
{-# PRIMITIVE i0 #-}
|
|
{-# PRIMITIVE i1 #-}
|
|
|
|
-- "minimum" on the interval
|
|
iand : I -> I -> I
|
|
{-# PRIMITIVE iand #-}
|
|
|
|
-- "maximum" on the interval.
|
|
ior : I -> I -> I
|
|
{-# PRIMITIVE ior #-}
|
|
|
|
-- The interpretation of iand as min and ior as max justifies the fact that
|
|
-- ior i (inot i) != i1, since that equality only holds for the endpoints.
|
|
|
|
-- inot i = 1 - i is a de Morgan involution.
|
|
inot : I -> I
|
|
{-# PRIMITIVE inot #-}
|
|
|
|
-- Paths
|
|
--------
|
|
|
|
-- Since every function in type theory is internally continuous,
|
|
-- and the two endpoints i0 and i1 are equal, we can take the type of
|
|
-- equalities to be continuous functions out of the interval.
|
|
-- That is, x ≡ y iff. ∃ f : I -> A, f i0 = x, f i1 = y.
|
|
|
|
-- The type PathP generalises this to dependent products (i : I) -> A i.
|
|
|
|
PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
|
|
{-# PRIMITIVE PathP #-}
|
|
|
|
-- By taking the first argument to be constant we get the equality type
|
|
-- Path.
|
|
|
|
Path : {A : Type} -> A -> A -> Type
|
|
Path = PathP (\i -> A)
|
|
|
|
-- reflexivity is given by constant paths
|
|
|
|
refl : {A : Type} {x : A} -> Path x 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
|
|
-- sym p i1 = p (inot i1) = p i0
|
|
-- This has the correct endpoints.
|
|
|
|
sym : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
|
|
sym p i = p (inot i)
|
|
|
|
id : {A : Type} -> A -> A
|
|
id x = x
|
|
|
|
the : (A : Pretype) -> A -> A
|
|
the A x = x
|
|
|
|
-- The eliminator for the interval says that if you have x : A i0 and y : A i1,
|
|
-- and x ≡ y, then you can get a proof A i for every element of the interval.
|
|
iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
|
|
iElim p i = p i
|
|
|
|
-- This corresponds to the elimination principle for the HIT
|
|
-- data I : Pretype where
|
|
-- i0 i1 : I
|
|
-- seg : i0 ≡ i1
|
|
|
|
-- The singleton subtype of A at x is the type of elements of y which
|
|
-- are equal to x.
|
|
Singl : (A : Type) -> A -> Type
|
|
Singl A x = (y : A) * Path x y
|
|
|
|
-- Contractible types are those for which there exists an element to which
|
|
-- all others are equal.
|
|
isContr : Type -> Type
|
|
isContr A = (x : A) * ((y : A) -> Path x y)
|
|
|
|
-- Using the connection \i j -> y.2 (iand i j), we can prove that
|
|
-- singletons are contracible. Together with transport later on,
|
|
-- we get the J elimination principle of paths.
|
|
|
|
dropJ : {A : Type} {x : A} {y : A} (p : Path x y)
|
|
-> PathP (\i -> Path (p i) (p i)) refl refl
|
|
dropJ p i j = p i
|
|
|
|
dropI : {A : Type} {x : A} {y : A} (p : Path x y)
|
|
-> PathP (\i -> Path x y) p p
|
|
dropI p i j = p j
|
|
|
|
and : {A : Type} {x : A} {y : A} (p : Path x y)
|
|
-> PathP (\i -> Path x (p i)) refl p
|
|
and p i j = p (iand i j)
|
|
|
|
or : {A : Type} {x : A} {y : A} (p : Path x y)
|
|
-> PathP (\i -> Path (p i) y) p refl
|
|
or p i j = p (ior i j)
|
|
|
|
|
|
singContr : {A : Type} {a : A} -> isContr (Singl A a)
|
|
singContr = ((a, \i -> a), contr) where
|
|
contr : (y : Singl A a) -> PathP (\i -> Singl A a) (a, \i -> a) y
|
|
contr y i = (y.2 i, and y.2 i)
|
|
|
|
-- Some more operations on paths. By rearranging parentheses we get a
|
|
-- proof that the images of equal elements are themselves equal.
|
|
ap : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
|
|
ap f p i = f (p i)
|
|
|
|
-- These satisfy definitional equalities, like apComp and apId, which are
|
|
-- propositional in vanilla MLTT.
|
|
apComp : {A : Type} {B : Type} {C : Type}
|
|
{f : A -> B} {g : B -> C} {x : A} {y : A}
|
|
(p : Path x y)
|
|
-> Path (ap g (ap f p)) (ap (\x -> g (f x)) p)
|
|
apComp p = refl
|
|
|
|
apId : {A : Type} {x : A} {y : A}
|
|
(p : Path x y)
|
|
-> Path (ap (id {A}) p) p
|
|
apId p = refl
|
|
|
|
-- Just like rearranging parentheses gives us ap, swapping the value
|
|
-- and interval binders gives us function extensionality.
|
|
funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
|
|
(h : (x : A) -> Path (f x) (g x))
|
|
-> Path f g
|
|
funext h i x = h x i
|
|
|
|
-- The proposition associated with an element of the interval
|
|
-------------------------------------------------------------
|
|
|
|
Eq_s : {A : Pretype} -> A -> A -> Pretype
|
|
{-# PRIMITIVE Eq_s #-}
|
|
|
|
refl_s : {A : Pretype} {x : A} -> Eq_s x x
|
|
{-# PRIMITIVE refl_s #-}
|
|
|
|
J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p
|
|
{-# PRIMITIVE J_s #-}
|
|
|
|
K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p
|
|
{-# PRIMITIVE K_s #-}
|
|
|
|
-- Associated with every element i : I of the interval, we have the type
|
|
-- IsOne i which is inhabited only when i = i1. In the model, this
|
|
-- corresponds to the map [φ] from the interval cubical set to the
|
|
-- subobject classifier.
|
|
|
|
IsOne : I -> Pretype
|
|
IsOne i = Eq_s i i1
|
|
|
|
-- The value itIs1 witnesses the fact that i1 = i1.
|
|
itIs1 : IsOne i1
|
|
itIs1 = refl_s
|
|
|
|
-- Partial elements
|
|
-------------------
|
|
--
|
|
-- Since a function I -> A has two endpoints, and a function I -> I -> A
|
|
-- has four endpoints + four functions I -> A as "sides" (obtained by
|
|
-- varying argument while holding the other as a bound variable), we
|
|
-- refer to elements of I^n -> A as "cubes".
|
|
|
|
-- This justifies the existence of partial elements, which are, as the
|
|
-- name implies, partial cubes. Namely, a Partial φ A is an element of A
|
|
-- which depends on a proof that IsOne φ.
|
|
|
|
Partial : I -> Type -> Pretype
|
|
{-# PRIMITIVE Partial #-}
|
|
|
|
-- There is also a dependent version where the type A is itself a
|
|
-- partial element.
|
|
|
|
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
|
|
-- equivalent values for every possible assignment of variables which
|
|
-- makes IsOne φ hold.
|
|
|
|
-- Cubical Subtypes
|
|
--------------------
|
|
|
|
-- Given A : Type, phi : I, and a partial element u : A defined on φ,
|
|
-- we have the type Sub A phi u, notated A[phi -> u] in the output of
|
|
-- the type checker, whose elements are "extensions" of u.
|
|
|
|
-- 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
|
|
{-# PRIMITIVE Sub #-}
|
|
|
|
-- Every total element u : A can be made partial on φ by ignoring the
|
|
-- constraint. Furthermore, this "totally partial" element agrees with
|
|
-- the original total element on φ.
|
|
inS : {A : Type} {phi : I} (u : A) -> Sub A phi (\x -> u)
|
|
{-# PRIMITIVE inS #-}
|
|
|
|
-- When IsOne φ, outS {A} {φ} {u} x reduces to u itIs1.
|
|
-- This implements the fact that x agrees with u on φ.
|
|
outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A
|
|
{-# PRIMITIVE outS #-}
|
|
|
|
-- The composition operation
|
|
----------------------------
|
|
|
|
-- Now that we have syntax for specifying partial cubes,
|
|
-- and specifying that an element agrees with a partial cube,
|
|
-- we can describe the composition operation.
|
|
|
|
primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> Sub (A i1) phi (u i1)
|
|
{-# 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 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
|
|
-- "tube", an open square with no floor or roof:
|
|
--
|
|
-- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,
|
|
-- we draw:
|
|
--
|
|
-- x q i1
|
|
-- | |
|
|
-- \j -> x | | \j -> q j
|
|
-- | |
|
|
-- x q i0
|
|
--
|
|
-- The composition operation says that, as long as we can provide a
|
|
-- "floor" connecting x -- q i0, as a total element of A which, on
|
|
-- phi, extends u i0, then we get the "roof" connecting x and q i1
|
|
-- for free.
|
|
--
|
|
-- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the
|
|
-- "floor", and composition gets us the dotted line:
|
|
--
|
|
-- x..........z
|
|
-- | |
|
|
-- x | | q j
|
|
-- | |
|
|
-- x----------y
|
|
-- 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 (\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
|
|
|
|
-- Since we have the iand operator, we can also derive the *filler* of a cube,
|
|
-- which connects the given face and the output of composition.
|
|
|
|
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 u a0 i =
|
|
comp (\j -> A (iand i j))
|
|
{ior phi (inot i)}
|
|
(\j [ (phi = i1) -> u (iand i j) itIs1
|
|
, (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 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 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
|
|
|
|
transFiller' : {A : Type} {x : A} {y : A} {z : A}
|
|
-> (p : Path x y) (q : Path y z)
|
|
-> PathP (\i -> Path (p (inot i)) z) q (trans {A} {x} {y} {z} p q)
|
|
transFiller' p q j i = hcomp (\k [ (i = i0) -> p (inot j)
|
|
, (i = i1) -> q k
|
|
, (j = i0) -> q (iand i k) ])
|
|
(inS (p (ior i (inot j))))
|
|
|
|
transAssoc : {A : Type} {w : A} {x : A} {y : A} {z : A} (p : Path w x) (q : Path x y) (r : Path y z)
|
|
-> Path (trans p (trans q r)) (trans (trans p q) r)
|
|
transAssoc p q r k = trans (transFiller p q k) (transFiller' q r (inot k))
|
|
|
|
dubcomp : {A : Type} {a : A} {b : A} {c : A} {d : A}
|
|
-> Path a b -> Path b c -> Path c d -> Path a d
|
|
dubcomp p q r i = hcomp (\j [ (i = i0) -> p (inot j), (i = i1) -> r j ]) (inS (q i))
|
|
|
|
-- For instance, the filler of the previous composition square
|
|
-- tells us that trans p refl = p:
|
|
|
|
transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
|
|
transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
|
|
|
|
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 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
|
|
|
|
-- Reduction of composition
|
|
---------------------------
|
|
--
|
|
-- Composition reduces on the structure of the family A : I -> Type to create
|
|
-- the element a1 : (A i1)[phi -> u i1].
|
|
--
|
|
-- For instance, when filling a cube of functions, the behaviour is to
|
|
-- first transport backwards along the domain, apply the function, then
|
|
-- forwards along the codomain.
|
|
|
|
transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path C D)
|
|
-> (f : A -> C) -> Path (transp (\i -> p i -> q i) f)
|
|
(\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))
|
|
transpFun p q f = refl
|
|
|
|
transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}
|
|
-> (f : (x : A i0) -> B i0 x)
|
|
-> Path (transp (\i -> (x : A i) -> B i x) f)
|
|
(\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i)))
|
|
(f (fill (\j -> A (inot j)) (\k []) (inS x) i1)))
|
|
transpDFun f = refl
|
|
|
|
-- When considering the more general case of a composition respecing sides,
|
|
-- the outer transport becomes a composition.
|
|
|
|
-- Glueing and Univalence
|
|
-------------------------
|
|
|
|
-- First, let's get some definitions out of the way.
|
|
--
|
|
-- The *fiber* of a function f : A -> B at a point y : B is the type of
|
|
-- inputs x : A which f takes to y, that is, for which there exists a
|
|
-- path f(x) = y.
|
|
|
|
fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type
|
|
fiber f y = (x : A) * Path y (f x)
|
|
|
|
-- An *equivalence* is a function where every fiber is contractible.
|
|
-- That is, for every point in the codomain y : B, there is exactly one
|
|
-- point in the input which f maps to y.
|
|
|
|
isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type
|
|
isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)
|
|
|
|
-- By extracting this point, which must exist because the fiber is contractible,
|
|
-- we can get an inverse of f:
|
|
|
|
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 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
|
|
-- equivalence to get a capital-E Equivalence.
|
|
|
|
Equiv : (A : Type) (B : Type) -> Type
|
|
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 = (\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,
|
|
-- glue, let us extend a partial element of a partial type to a total
|
|
-- element of a total type, by "gluing" the partial type T using a
|
|
-- partial equivalence e onto a total type A.
|
|
|
|
-- In particular, we have that when φ = i1, Glue A [i1 -> (T, f)] = T.
|
|
|
|
primGlue : (A : Type) {phi : I}
|
|
(T : Partial phi Type)
|
|
(e : PartialP phi (\o -> Equiv (T o) A))
|
|
-> Type
|
|
{-# PRIMITIVE Glue primGlue #-}
|
|
|
|
-- The glue constructor extends the partial element t : T to a total
|
|
-- element of Glue A [φ -> (T, e)] as long as we have a total im : A
|
|
-- which is the image of f(t).
|
|
--
|
|
-- 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 (\o -> T o))
|
|
-> (im : Sub A phi (\o -> (e o).1 (t o)))
|
|
-> primGlue A T e
|
|
|
|
{-# PRIMITIVE glue prim'glue #-}
|
|
|
|
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 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} ...
|
|
-- will have type T, and so to get back an A we need to apply the
|
|
-- partial equivalence f (defined everywhere).
|
|
|
|
primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}
|
|
-> primGlue A {phi} T e -> A
|
|
|
|
{-# PRIMITIVE unglue primUnglue #-}
|
|
|
|
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 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:
|
|
--
|
|
-- T i0 ......... T i1
|
|
-- | |
|
|
-- | |
|
|
-- e i0 |~ ~| e i1
|
|
-- | |
|
|
-- | |
|
|
-- A i0 --------- A i1
|
|
-- A
|
|
--
|
|
-- Where the the two "e" sides are equivalences, and the Bottom side is
|
|
-- the line i : I |- A.
|
|
--
|
|
-- Thus, by choosing a base type, a set of partial types and partial
|
|
-- 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 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.
|
|
--
|
|
-- A ............ B
|
|
-- | |
|
|
-- | |
|
|
-- equiv |~ ua equiv ~| idEquiv {B}
|
|
-- | |
|
|
-- | |
|
|
-- B ------------ B
|
|
-- \i → B
|
|
--
|
|
ua : {A : Type} {B : Type} -> Equiv A B -> Path A B
|
|
ua equiv i =
|
|
Glue B (\[ (i = i0) -> (A, equiv)
|
|
, (i = i1) -> (B, idEquiv) ])
|
|
|
|
lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
|
|
{-# PRIMITIVE lineToEquiv #-}
|
|
|
|
idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
|
|
idToEquiv p = lineToEquiv (\i -> p i)
|
|
|
|
isEquivTransport : (A : I -> Type) -> isEquiv (transp A)
|
|
isEquivTransport A = (lineToEquiv A).2
|
|
|
|
-- The fact that this diagram has 2 filled-in B sides explains the
|
|
-- complication in the proof below.
|
|
--
|
|
-- In particular, the actual behaviour of transp (\i -> ua f i)
|
|
-- (x : A) is not just to apply f x to get a B (the left side), it also
|
|
-- needs to:
|
|
--
|
|
-- * For the Bottom side, compose along (\i -> B) (the Bottom side)
|
|
-- * For the right side, apply the inverse of the identity, which
|
|
-- is just identity, to get *some* b : B
|
|
--
|
|
-- But that b : B might not agree with the sides of the composition
|
|
-- operation in a more general case, so it composes along (\i -> B)
|
|
-- *again*!
|
|
--
|
|
-- Thus the proof: a simple cubical argument suffices, since
|
|
-- for any composition, its filler connects either endpoints. So
|
|
-- 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 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
|
|
--
|
|
-- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.
|
|
--
|
|
-- Available freely here: https://arxiv.org/abs/1712.04890v3
|
|
|
|
J : {A : Type} {x : A}
|
|
(P : (y : A) -> Path x y -> Type)
|
|
(d : P x (\i -> x))
|
|
{y : A} (p : Path x y)
|
|
-> P y p
|
|
J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d
|
|
|
|
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)
|
|
|
|
Jay : {A : Type} {x : A}
|
|
(P : ((y : A) * Path x y) -> Type)
|
|
(d : P (x, refl))
|
|
(s : (y : A) * Path x y)
|
|
-> P s
|
|
Jay P d s = transp (\i -> P ((singContr {A} {x}).2 s i)) d
|
|
|
|
|
|
-- Isomorphisms
|
|
---------------
|
|
--
|
|
-- Since isomorphisms are a much more convenient notion of equivalence
|
|
-- than contractible fibers, it's natural to ask why the CCHM paper, and
|
|
-- this implementation following that, decided on the latter for our
|
|
-- definition of equivalence.
|
|
|
|
isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type
|
|
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
|
|
-- an equivalence. This is Lemma 4.1.1 of the HoTT book.
|
|
|
|
Iso : Type -> Type -> Type
|
|
Iso A B = (f : A -> B) * isIso f
|
|
|
|
-- Nevertheless, we can prove that any function with an isomorphism
|
|
-- structure has contractible fibers, using a cubical argument adapted
|
|
-- from CCHM's implementation of cubical type theory:
|
|
--
|
|
-- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55
|
|
|
|
IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B
|
|
IsoToEquiv iso = (f, \y -> (fCenter y, fIsCenter y)) where
|
|
f = iso.1
|
|
g = iso.2.1
|
|
s = iso.2.2.1
|
|
t = iso.2.2.2
|
|
|
|
lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path y (f x0)) (p1 : Path y (f x1))
|
|
-> PathP (\i -> fiber f y) (x0, p0) (x1, p1)
|
|
lemIso y x0 x1 p0 p1 =
|
|
let
|
|
rem0 : Path x0 (g y)
|
|
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 = hcomp (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i))))
|
|
|
|
p : Path x0 x1
|
|
p i = hcomp (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
|
|
|
|
fill0 : I -> I -> A
|
|
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 = 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 = 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 = 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 = 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
|
|
fCenter y = (g y, sym (s y))
|
|
|
|
fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w
|
|
fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
|
|
|
|
IsoToId : {A : Type} {B : Type} -> Iso A B -> Path A B
|
|
IsoToId i = ua (IsoToEquiv i)
|
|
|
|
-- We can prove that any involutive function is an isomorphism, since
|
|
-- such a function is its own inverse.
|
|
|
|
involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f
|
|
involToIso f inv = (f, inv, inv)
|
|
|
|
-- An example of ua
|
|
---------------------------
|
|
--
|
|
-- The classic example of ua is the equivalence
|
|
-- not : Bool \simeq Bool.
|
|
--
|
|
-- We define it here.
|
|
|
|
data Bool : Type where
|
|
true : Bool
|
|
false : Bool
|
|
|
|
not : Bool -> Bool
|
|
not = \case
|
|
true -> false
|
|
false -> true
|
|
|
|
elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b
|
|
elimBool P x y = \case
|
|
true -> x
|
|
false -> y
|
|
|
|
if : {A : Type} -> A -> A -> Bool -> A
|
|
if x y = \case
|
|
true -> x
|
|
false -> y
|
|
|
|
-- By pattern matching it suffices to prove (not (not true)) ≡ true and
|
|
-- not (not false) ≡ false. Since not (not true) computes to true (resp.
|
|
-- false), both proofs go through by refl.
|
|
notInvol : (x : Bool) -> Path (not (not x)) x
|
|
notInvol = elimBool (\b -> Path (not (not b)) b) refl refl
|
|
|
|
notp : Path Bool Bool
|
|
notp = ua (IsoToEquiv (not, involToIso not notInvol))
|
|
|
|
-- This path actually serves to prove a simple lemma about the universes
|
|
-- of HoTT, namely, that any univalent universe is not a 0-type. If we
|
|
-- had HITs, we could prove that this fact holds for any n, but for now,
|
|
-- proving it's not an h-set is the furthest we can go.
|
|
|
|
-- First we define what it means for something to be false. In type theory,
|
|
-- we take ¬P = P → ⊥, where the Bottom type is the only type satisfying
|
|
-- the elimination principle
|
|
--
|
|
-- elimBottom : (P : Bottom -> Type) -> (b : Bottom) -> P b
|
|
--
|
|
-- This follows from setting Bottom := ∀ A, A.
|
|
|
|
data Bottom : Type where {}
|
|
|
|
elimBottom : (P : Bottom -> Pretype) -> (b : Bottom) -> P b
|
|
elimBottom P = \case {}
|
|
|
|
absurd : {P : Pretype} -> Bottom -> P
|
|
absurd = \case {}
|
|
|
|
-- We prove that true != false by transporting along the path
|
|
--
|
|
-- \i -> if (Bool -> Bool) A (p i)
|
|
-- (Bool -> Bool) ------------------------------------ A
|
|
--
|
|
-- To verify that this has the correct endpoints, check out the endpoints
|
|
-- for p:
|
|
--
|
|
-- true ------------------------------------ false
|
|
--
|
|
-- and evaluate the if at either end.
|
|
|
|
trueNotFalse : Path true false -> Bottom
|
|
trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id
|
|
|
|
-- To be an h-Set is to have no "higher path information". Alternatively,
|
|
--
|
|
-- isSet A = (x : A) (y : A) -> isHProp (Path x y)
|
|
--
|
|
|
|
isProp : Type -> Type
|
|
isProp A = (x : A) (y : A) -> Path x y
|
|
|
|
isSet : Type -> Type
|
|
isSet A = (x : A) (y : A) -> isProp (Path x y)
|
|
|
|
-- We can prove *a* contradiction (note: this is a direct proof!) by adversarially
|
|
-- choosing two paths p, q that we know are not equal. Since "equal" paths have
|
|
-- equal behaviour when transporting, we can choose two paths p, q and a point x
|
|
-- such that transporting x along p gives a different result from x along q.
|
|
--
|
|
-- Since transp notp = not but transp refl = id, that's what we go with. The choice
|
|
-- of false as the point x is just from the endpoints of trueNotFalse.
|
|
|
|
universeNotSet : isSet Type -> Bottom
|
|
universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl i j) false)
|
|
|
|
-- Funext is an inverse of happly
|
|
---------------------------------
|
|
--
|
|
-- Above we proved function extensionality, namely, that functions
|
|
-- pointwise equal everywhere are themselves equal.
|
|
-- However, this formulation of the axiom is known as "weak" function
|
|
-- 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 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
|
|
happly p x i = p i x
|
|
|
|
-- Strong function extensionality: happly is an equivalence.
|
|
|
|
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 = (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 =
|
|
let
|
|
theIso : Iso (Path f g) (Hom f g)
|
|
theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
|
|
in ua (IsoToEquiv theIso)
|
|
|
|
-- Inductive types
|
|
-------------------
|
|
--
|
|
-- An inductive type is a type freely generated by a finite set of
|
|
-- constructors. For instance, the type of natural numbers is generated
|
|
-- by the constructors for "zero" and "successor".
|
|
|
|
data Nat : Type where
|
|
zero : Nat
|
|
succ : Nat -> Nat
|
|
|
|
-- Pattern matching allows us to prove that these initial types are
|
|
-- initial algebras for their corresponding functors.
|
|
|
|
Nat_elim : (P : Nat -> Type) -> P zero -> ((x : Nat) -> P x -> P (succ x)) -> (x : Nat) -> P x
|
|
Nat_elim P pz ps = \case
|
|
zero -> pz
|
|
succ x -> ps x (Nat_elim P pz ps x)
|
|
|
|
zeroNotSucc : {x : Nat} -> Path zero (succ x) -> Bottom
|
|
zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where
|
|
fun : Nat -> Type
|
|
fun = \case
|
|
zero -> Nat
|
|
succ x -> Bottom
|
|
|
|
pred : Nat -> Nat
|
|
pred = \case
|
|
zero -> zero
|
|
succ x -> x
|
|
|
|
succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y
|
|
succInj p i = pred (p i)
|
|
|
|
-- The type of integers can be defined as A + B, where "pos n" means +n
|
|
-- and "neg n" means -(n + 1).
|
|
|
|
data Int : Type where
|
|
pos : Nat -> Int
|
|
neg : Nat -> Int
|
|
|
|
-- On this representation we can define the successor and predecessor
|
|
-- functions by (nested) induction.
|
|
|
|
sucZ : Int -> Int
|
|
sucZ = \case
|
|
pos n -> pos (succ n)
|
|
neg n ->
|
|
let suc_neg : Nat -> Int
|
|
suc_neg = \case
|
|
zero -> pos zero
|
|
succ n -> neg n
|
|
in suc_neg n
|
|
|
|
predZ : Int -> Int
|
|
predZ = \case
|
|
pos n ->
|
|
let pred_pos : Nat -> Int
|
|
pred_pos = \case
|
|
zero -> neg zero
|
|
succ n -> pos n
|
|
in pred_pos n
|
|
neg n -> neg (succ n)
|
|
|
|
-- And prove that the successor function is an isomorphism, and thus, an
|
|
-- equivalence.
|
|
sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
|
|
sucPredZ = \case
|
|
pos n ->
|
|
let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
|
|
k = \case
|
|
zero -> refl
|
|
succ n -> refl
|
|
in k n
|
|
neg n -> refl
|
|
|
|
predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
|
|
predSucZ = \case
|
|
pos n -> refl
|
|
neg n ->
|
|
let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
|
|
k = \case
|
|
zero -> refl
|
|
succ n -> refl
|
|
in k n
|
|
|
|
sucEquiv : Equiv Int Int
|
|
sucEquiv = IsoToEquiv (sucZ, (predZ, sucPredZ, predSucZ))
|
|
|
|
-- Univalence gives us a path between integers such that transp intPath
|
|
-- x = suc x, transp (sym intPath) x = pred x
|
|
|
|
intPath : Path Int Int
|
|
intPath = ua sucEquiv
|
|
|
|
-- Higher inductive types
|
|
-------------------------
|
|
--
|
|
-- While inductive types let us generate discrete spaces like the
|
|
-- naturals or integers, they do not support defining higher-dimensional
|
|
-- structures given by spaces with points and paths.
|
|
|
|
-- A very simple higher inductive type is the interval, given by
|
|
|
|
data Interval : Type where
|
|
ii0 : Interval
|
|
ii1 : Interval
|
|
seg i : Interval [ (i = i0) -> ii0, (i = i1) -> ii1 ]
|
|
|
|
-- This expresses that we have two points ii0 and ii1 and a path (\i ->
|
|
-- seg i) with endpoints ii0 and ii1.
|
|
|
|
-- With this type we can reproduce the proof of Lemma 6.3.2 from the
|
|
-- HoTT book:
|
|
|
|
iFunext : {A : Type} {B : A -> Type} (f : (x : A) -> B x) (g : (x : A) -> B x)
|
|
-> ((x : A) -> Path (f x) (g x)) -> Path f g
|
|
iFunext f g p i = h' (seg i) where
|
|
h : (x : A) -> Interval -> B x
|
|
h x = \case
|
|
ii0 -> f x
|
|
ii1 -> g x
|
|
seg i -> p x i
|
|
|
|
h' : Interval -> (x : A) -> B x
|
|
h' i x = h x i
|
|
|
|
-- Of course, Cubical Type Theory also has an interval (pre)type, but
|
|
-- that, unlike the Interval here, is not Kan: it has no composition
|
|
-- structure.
|
|
|
|
-- Another simple higher-inductive type is the circle, with a point and
|
|
-- a non-trivial loop, (\i -> loop i).
|
|
|
|
data S1 : Type where
|
|
base : S1
|
|
loop i : S1 [ (i = i1) -> base, (i = i0) -> base ]
|
|
|
|
-- By writing a function from the circle to the universe of types Type,
|
|
-- we can calculate winding numbers along the circle.
|
|
|
|
helix : S1 -> Type
|
|
helix = \case
|
|
base -> Int
|
|
loop i -> intPath i
|
|
|
|
loopP : Path base base
|
|
loopP i = loop i
|
|
|
|
encode : (x : S1) -> Path base x -> helix x
|
|
encode x p = subst helix p (pos zero)
|
|
|
|
winding : Path base base -> Int
|
|
winding = encode base
|
|
|
|
-- For instance, going around the loop once has a winding number of +1,
|
|
|
|
windingLoop : Path (winding (\i -> loop i)) (pos (succ zero))
|
|
windingLoop = refl
|
|
|
|
-- Going backwards has a winding number of -1 (remember the
|
|
-- representation of integers),
|
|
|
|
windingSymLoop : Path (winding (\i -> loop (inot i))) (neg zero)
|
|
windingSymLoop = refl
|
|
|
|
-- And going around the trivial loop (\i -> base) goes around the the
|
|
-- non-trivial loop (\i -> loop) zero times.
|
|
|
|
windingBase : Path (winding (\i -> base)) (pos zero)
|
|
windingBase = refl
|
|
|
|
goAround : Int -> Path base base
|
|
goAround =
|
|
\case
|
|
pos n ->
|
|
let
|
|
forwards : Nat -> Path base base
|
|
forwards = \case
|
|
zero -> refl
|
|
succ n -> trans (goAround (pos n)) (\i -> loop i)
|
|
in forwards n
|
|
neg n ->
|
|
let
|
|
backwards : Nat -> Path base base
|
|
backwards = \case
|
|
zero -> \i -> loop (inot i)
|
|
succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
|
|
in backwards n
|
|
|
|
windingGoAround : (n : Int) -> Path (winding (goAround n)) n
|
|
windingGoAround =
|
|
\case
|
|
pos n -> posCase n
|
|
neg n -> negCase n
|
|
where
|
|
posCase : (n : Nat) -> Path (winding (goAround (pos n))) (pos n)
|
|
posCase = \case
|
|
zero -> refl
|
|
succ n -> ap sucZ (posCase n)
|
|
negCase : (n : Nat) -> Path (winding (goAround (neg n))) (neg n)
|
|
negCase = \case
|
|
zero -> refl
|
|
succ n -> ap predZ (negCase n)
|
|
|
|
decode : (x : S1) -> helix x -> Path base x
|
|
decode = go decodeSquare where
|
|
decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
|
|
decodeSquare =
|
|
\case
|
|
pos n -> posCase n
|
|
neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
|
|
where
|
|
posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
|
|
posCase = \case
|
|
zero -> \i j -> loop (ior i (inot j))
|
|
succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) i
|
|
|
|
go : ((n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n))
|
|
-> (x : S1) -> helix x -> Path base x
|
|
go decodeSquare = \case
|
|
base -> goAround
|
|
loop i -> \y j ->
|
|
let n : Int
|
|
n = primUnglue {Int} {ior i (inot i)} {\o -> Int} {\[ (i = i1) -> idEquiv, (i = i0) -> sucEquiv ]} y
|
|
in hcomp (\k [ (i = i0) -> goAround (predSucZ y k) j
|
|
, (i = i1) -> goAround y j
|
|
, (j = i0) -> base
|
|
, (j = i1) -> loop i ])
|
|
(inS (decodeSquare n i j))
|
|
|
|
decodeWinding : (x : S1) (p : Path base x) -> Path (decode x (encode x p)) p
|
|
decodeWinding x p = J (\y q -> Path (decode y (encode y q)) q) (\ i -> refl) p
|
|
|
|
loopS1IsoInt : Iso (Path base base) Int
|
|
loopS1IsoInt = (winding, goAround, windingGoAround, decodeWinding base)
|
|
|
|
LoopS1IsInt : Path (Path base base) Int
|
|
LoopS1IsInt = IsoToId loopS1IsoInt
|
|
|
|
-- One particularly general higher inductive type is the homotopy pushout,
|
|
-- which can be seen as a kind of sum B + C with the extra condition that
|
|
-- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.
|
|
|
|
data Pushout {A : Type} {B : Type} {C : Type} (f : A -> B) (g : A -> C) : Type where
|
|
inl : (x : B) -> Pushout f g
|
|
inr : (y : C) -> Pushout f g
|
|
push i : (a : A) -> Pushout f g [ (i = i0) -> inl (f a), (i = i1) -> inr (g a) ]
|
|
|
|
Coproduct : Type -> Type -> Type
|
|
Coproduct A B = Pushout {Bottom} {A} {B} absurd absurd
|
|
|
|
Pushout_rec : {A : Type} {B : Type} {C : Type} {f : A -> B} {g : A -> C}
|
|
-> (P : Pushout f g -> Type)
|
|
-> (fc : (x : B) -> P (inl x))
|
|
-> (gc : (x : C) -> P (inr x))
|
|
-> ((a : A) -> PathP (\i -> P (push a i)) (fc (f a)) (gc (g a)))
|
|
-> (c : Pushout f g) -> P c
|
|
Pushout_rec P fc gc pc = \case
|
|
inl x -> fc x
|
|
inr y -> gc y
|
|
push c i -> pc c i
|
|
|
|
data Susp (A : Type) : Type where
|
|
north : Susp A
|
|
south : Susp A
|
|
merid i : A -> Susp A [ (i = i0) -> north, (i = i1) -> south ]
|
|
|
|
data Unit : Type where
|
|
tt : Unit
|
|
|
|
unitEta : (x : Unit) -> Path x tt
|
|
unitEta = \case tt -> refl
|
|
|
|
unitContr : isContr Unit
|
|
unitContr = (tt, \x -> sym (unitEta x))
|
|
|
|
unitProp : isProp Unit
|
|
unitProp = \case
|
|
tt -> \case
|
|
tt -> refl
|
|
|
|
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 = 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
|
|
inr x -> south
|
|
push x i -> merid x i
|
|
|
|
Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A
|
|
Susp_to_poSusp = \case
|
|
north -> inl tt
|
|
south -> inr tt
|
|
merid x i -> push x i
|
|
|
|
Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x
|
|
Susp_to_poSusp_to_Susp = \case
|
|
north -> refl
|
|
south -> refl
|
|
merid x i -> refl
|
|
|
|
poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
|
|
poSusp_to_Susp_to_poSusp {A} = \case
|
|
inl x -> ap inl (sym (unitEta x))
|
|
inr x -> ap inr (sym (unitEta x))
|
|
push x i -> refl
|
|
|
|
data T2 : Type where
|
|
baseT : T2
|
|
pathOne i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
|
|
pathTwo i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
|
|
square i j : T2 [
|
|
(j = i0) -> pathTwo i,
|
|
(j = i1) -> pathTwo i,
|
|
(i = i0) -> pathOne j,
|
|
(i = i1) -> pathOne j
|
|
]
|
|
|
|
TorusIsTwoCircles : Equiv T2 (S1 * S1)
|
|
TorusIsTwoCircles = IsoToEquiv theIso where
|
|
torusToCircs : T2 -> S1 * S1
|
|
torusToCircs = \case
|
|
baseT -> (base, base)
|
|
pathOne i -> (loop i, base)
|
|
pathTwo i -> (base, loop i)
|
|
square i j -> (loop i, loop j)
|
|
|
|
circsToTorus : (S1 * S1) -> T2
|
|
circsToTorus pair = go pair.1 pair.2
|
|
where
|
|
baseCase : S1 -> T2
|
|
baseCase = \case
|
|
base -> baseT
|
|
loop j -> pathTwo j
|
|
|
|
loopCase : Path baseCase baseCase
|
|
loopCase i = \case
|
|
base -> pathOne i
|
|
loop j -> square i j
|
|
|
|
go : S1 -> S1 -> T2
|
|
go = \case
|
|
base -> baseCase
|
|
loop i -> loopCase i
|
|
|
|
torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
|
|
torusToCircsToTorus = \case
|
|
baseT -> refl
|
|
pathOne i -> refl
|
|
pathTwo i -> refl
|
|
square i j -> refl
|
|
|
|
circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
|
|
circsToTorusToCircs pair = go pair.1 pair.2 where
|
|
baseCase : (y : S1) -> Path (torusToCircs (circsToTorus (base, y))) (base, y)
|
|
baseCase = \case
|
|
base -> refl
|
|
loop j -> refl
|
|
|
|
loopCase : (i : I) (y : S1) -> Path (torusToCircs (circsToTorus (loop i, y))) (loop i, y )
|
|
loopCase i = \case
|
|
base -> refl
|
|
loop j -> refl
|
|
|
|
go : (x : S1) (y : S1) -> Path (torusToCircs (circsToTorus (x, y))) (x, y)
|
|
go = \case
|
|
base -> baseCase
|
|
loop i -> loopCase i
|
|
|
|
theIso : Iso T2 (S1 * S1)
|
|
theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)
|
|
|
|
abs : Int -> Nat
|
|
abs = \case
|
|
pos n -> n
|
|
neg n -> succ n
|
|
|
|
sign : Int -> Bool
|
|
sign = \case
|
|
pos n -> true
|
|
neg n -> false
|
|
|
|
boolAnd : Bool -> Bool -> Bool
|
|
boolAnd = \case
|
|
true -> \case
|
|
true -> true
|
|
false -> false
|
|
false -> \case
|
|
true -> false
|
|
false -> false
|
|
|
|
boolXor : Bool -> Bool -> Bool
|
|
boolXor = \case
|
|
true -> \case
|
|
true -> false
|
|
false -> true
|
|
false -> \case
|
|
false -> false
|
|
true -> true
|
|
|
|
plusNat : Nat -> Nat -> Nat
|
|
plusNat = \case
|
|
zero -> \x -> x
|
|
succ n -> \x -> succ (plusNat n x)
|
|
|
|
plusZero : (x : Nat) -> Path (plusNat zero x) x
|
|
plusZero = \case
|
|
zero -> refl
|
|
succ n -> \i -> succ (plusZero n i)
|
|
|
|
multNat : Nat -> Nat -> Nat
|
|
multNat = \case
|
|
zero -> \x -> zero
|
|
succ n -> \x -> plusNat x (multNat n x)
|
|
|
|
multInt : Int -> Int -> Int
|
|
multInt x y = signify (multNat (abs x) (abs y)) (not (boolXor (sign x) (sign y))) where
|
|
signify : Nat -> Bool -> Int
|
|
signify = \case
|
|
zero -> \x -> pos zero
|
|
succ n -> \case
|
|
true -> pos (succ n)
|
|
false -> neg n
|
|
|
|
two : Int
|
|
two = pos (succ (succ zero))
|
|
|
|
four : Int
|
|
four = multInt two two
|
|
|
|
sixteen : Int
|
|
sixteen = multInt four four
|
|
|
|
Prop : Type
|
|
Prop = (A : Type) * isProp A
|
|
|
|
data Sq (A : Type) : Type where
|
|
inc : A -> Sq A
|
|
sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ]
|
|
|
|
isProp_isSet : {A : Type} -> isProp A -> isSet A
|
|
isProp_isSet h a b p q j i =
|
|
hcomp {A}
|
|
(\k [ (i = i0) -> h a a k
|
|
, (i = i1) -> h a b k
|
|
, (j = i0) -> h a (p i) k
|
|
, (j = i1) -> h a (q i) k
|
|
])
|
|
(inS a)
|
|
|
|
unitSet : isSet Unit
|
|
unitSet = isProp_isSet unitProp
|
|
|
|
isProp_isProp : {A : Type} -> isProp (isProp A)
|
|
isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i
|
|
|
|
isSet_isProp : {A : Type} -> isProp (isSet A)
|
|
isSet_isProp f g i x y = isProp_isProp {_} (f x y) (g x y) i
|
|
|
|
isProp_isContr : {A : Type} -> isProp (isContr A)
|
|
isProp_isContr {A} z0 z1 j =
|
|
( z0.2 z1.1 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
|
|
isContr_isProp x a b i = hcomp (\k [ (i = i0) -> x.2 a k, (i = i1) -> x.2 b k ]) (inS x.1)
|
|
|
|
isSet_prod : {A : Type} {B : Type} -> isSet A -> isSet B -> isSet (A * B)
|
|
isSet_prod a b x y p q i j = (a x.1 y.1 (\i -> (p i).1) (\i -> (q i).1) i j, b x.2 y.2 (\i -> (p i).2) (\i -> (q i).2) i j)
|
|
|
|
isSet_pi : {A : Type} {B : A -> Type} -> ((x : A) -> isSet (B x)) -> isSet ((x : A) -> B x)
|
|
isSet_pi rng a b p q i j z = rng z (a z) (b z) (happly p z) (happly q z) i j
|
|
|
|
sigmaPath : {A : Type} {B : A -> Type} {s1 : (x : A) * B x} {s2 : (x : A) * B x}
|
|
-> (p : Path s1.1 s2.1)
|
|
-> PathP (\i -> B (p i)) s1.2 s2.2
|
|
-> Path s1 s2
|
|
sigmaPath p q i = (p i, q i)
|
|
|
|
propExt : {A : Type} {B : Type}
|
|
-> isProp A -> isProp B
|
|
-> (A -> B)
|
|
-> (B -> A)
|
|
-> Equiv A B
|
|
propExt {A} {B} propA propB f g = (f, contract) where
|
|
contract : (y : B) -> isContr (fiber f y)
|
|
contract y =
|
|
let arg : A
|
|
arg = g y
|
|
in ( (arg, propB y (f arg))
|
|
, \fib -> sigmaPath (propA _ _) (isProp_isSet propB y (f fib.1) _ _))
|
|
|
|
Sq_rec : {A : Type} {B : Type}
|
|
-> isProp B
|
|
-> (f : A -> B)
|
|
-> Sq A -> B
|
|
Sq_rec prop f =
|
|
\case
|
|
inc x -> f x
|
|
sq x y i -> prop (work x) (work y) i
|
|
where
|
|
work : Sq A -> B
|
|
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)
|
|
|
|
data S2 : Type where
|
|
base2 : S2
|
|
surf2 i j : S2 [ (i = i0) -> base2, (i = i1) -> base2, (j = i0) -> base2, (j = i1) -> base2]
|
|
|
|
S2IsSuspS1 : Path S2 (Susp S1)
|
|
S2IsSuspS1 = ua (IsoToEquiv iso) where
|
|
toS2 : Susp S1 -> S2
|
|
toS2 = \case { north -> base2; south -> base2; merid x i -> sphMerid x i } where
|
|
sphMerid = \case
|
|
base -> \i -> base2
|
|
loop j -> \i -> surf2 i j
|
|
|
|
suspSurf : I -> I -> I -> Susp S1
|
|
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 }
|
|
|
|
toFromS2 : (x : S2) -> Path (toS2 (fromS2 x)) x
|
|
toFromS2 = \case { base2 -> refl; surf2 i j -> \k -> toS2 (suspSurf i j (inot k)) }
|
|
|
|
fromToS2 : (x : Susp S1) -> Path (fromS2 (toS2 x)) x
|
|
fromToS2 = \case { north -> refl; south -> \i -> merid base i; merid x i -> meridCase i x } where
|
|
meridCase : (i : I) (x : S1) -> Path (fromS2 (toS2 (merid x i))) (merid x i)
|
|
meridCase i = \case
|
|
base -> \k -> merid base (iand i k)
|
|
loop j -> \k -> suspSurf i j (inot k)
|
|
|
|
iso : Iso S2 (Susp S1)
|
|
iso = (fromS2, toS2, fromToS2, toFromS2)
|
|
|
|
data S3 : Type where
|
|
base3 : S3
|
|
surf3 i j k : S3 [ (i = i0) -> base3, (i = i1) -> base3, (j = i0) -> base3, (j = i1) -> base3, (k = i0) -> base3, (k = i1) -> base3 ]
|
|
|
|
S3IsSuspS2 : Path S3 (Susp S2)
|
|
S3IsSuspS2 = ua (IsoToEquiv iso) where
|
|
toS3 : Susp S2 -> S3
|
|
toS3 = \case { north -> base3; south -> base3; merid x i -> sphMerid x i } where
|
|
sphMerid = \case
|
|
base2 -> \i -> base3
|
|
surf2 j k -> \i -> surf3 i j k
|
|
|
|
suspSurf : I -> I -> I -> I -> Susp S2
|
|
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 }
|
|
|
|
toFromS3 : (x : S3) -> Path (toS3 (fromS3 x)) x
|
|
toFromS3 = \case { base3 -> refl; surf3 i j k -> \l -> toS3 (suspSurf i j k (inot l)) }
|
|
|
|
fromToS3 : (x : Susp S2) -> Path (fromS3 (toS3 x)) x
|
|
fromToS3 = \case { north -> refl; south -> \i -> merid base2 i; merid x i -> meridCase i x } where
|
|
meridCase : (i : I) (x : S2) -> Path (fromS3 (toS3 (merid x i))) (merid x i)
|
|
meridCase i = \case
|
|
base2 -> \k -> merid base2 (iand i k)
|
|
surf2 j k -> \l -> suspSurf i j k (inot l)
|
|
|
|
iso : Iso S3 (Susp S2)
|
|
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 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} 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 = 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 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 (\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 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 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
|
|
zeroCase : (y : Nat) -> Path zero y -> Eq_s zero y
|
|
zeroCase = \case
|
|
zero -> \p -> refl_s
|
|
succ x -> \p -> absurd (zeroNotSucc p)
|
|
succCase : (x : Nat) (y : Nat) -> Path (succ x) y -> Eq_s (succ x) y
|
|
succCase x = \case
|
|
zero -> \p -> absurd (zeroNotSucc (sym p))
|
|
succ y -> \p -> ap_s succ (Path_nat_strict_nat x y (succInj p))
|
|
|
|
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 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)
|
|
|
|
inv : (y : A) (l : Path x y) -> Path (strictEq_pathEq (p_to_s l)) l
|
|
inv y l = J {A} {x} (\y l -> Path (strictEq_pathEq (p_to_s l)) l) (strictEq_pathEq aux) {y} l where
|
|
aux : Eq_s (strictEq_pathEq (p_to_s (\i -> x))) (\i -> x)
|
|
aux = seq_pathRefl (p_to_s (\i -> x))
|
|
|
|
axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isSet 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
|
|
uipRefl x p = K {x} (\q -> Path refl q) refl p
|
|
|
|
pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isSet A
|
|
pathToEq_isSet p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s)
|
|
|
|
Nat_isSet : isSet Nat
|
|
Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
|
|
|
|
Bool_isSet : isSet Bool
|
|
Bool_isSet = pathToEq_isSet {Bool} (\{x} {y} -> p x y) where
|
|
p : (x : Bool) (y : Bool) -> Path x y -> Eq_s x y
|
|
p = \case
|
|
true -> \case
|
|
true -> \p -> refl_s
|
|
false -> \p -> absurd (trueNotFalse p)
|
|
false -> \case
|
|
false -> \p -> refl_s
|
|
true -> \p -> absurd (trueNotFalse (sym p))
|
|
|
|
equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y
|
|
equivCtr e y = (e.2 y).1
|
|
|
|
equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)
|
|
-> (v : fiber e.1 y) -> Path (equivCtr e y) v
|
|
equivCtrPath e y = (e.2 y).2
|
|
|
|
contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u
|
|
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' 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 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 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 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 f = (f base, \i -> f (loop 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 {X}, fro, ret, sec) where
|
|
to = S1Map_to_baseLoop
|
|
fro : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
|
|
fro p = \case
|
|
base -> p.1
|
|
loop i -> p.2 i
|
|
|
|
sec : (f : S1 -> X) -> Path (fro (to f)) f
|
|
sec f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where
|
|
h : (x : S1) -> Path (fro (to f) x) (f x)
|
|
h = \case
|
|
base -> refl
|
|
loop i -> refl
|
|
|
|
ret : {X : Type} -> (x : (a : X) * Path a a) -> Path (to (fro x)) x
|
|
ret x = refl
|
|
|
|
-- HoTT book lemma 8.9.1
|
|
encodeDecode : {A : Type} {a0 : A}
|
|
-> (code : A -> Type)
|
|
-> (c0 : code a0)
|
|
-> (decode : (x : A) -> code x -> (Path a0 x))
|
|
-> ((c : code a0) -> Path (transp (\i -> code (decode a0 c i)) c0) c)
|
|
-> Path (decode a0 c0) refl
|
|
-> Path (Path a0 a0) (code a0)
|
|
encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode _, encDec, decEnc) where
|
|
encode : {x : A} -> Path a0 x -> code x
|
|
encode alpha = transp (\i -> code (alpha i)) c0
|
|
|
|
encodeRefl : Path (encode refl) 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
|
|
q : Path (decode _ (encode refl)) refl
|
|
q = transp (\i -> Path (decode _ (encodeRefl (inot i))) refl) based
|
|
|
|
S1_elim : (P : S1 -> Type)
|
|
-> (pb : P base)
|
|
-> PathP (\i -> P (loop i)) pb pb
|
|
-> (x : S1) -> P x
|
|
S1_elim P pb pq = \case
|
|
base -> pb
|
|
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
|
|
|
|
Constant : {A : Type} {B : Type} -> (A -> B) -> Type
|
|
Constant f = (y : B) * (x : A) -> Path y (f x)
|
|
|
|
Weakly : {A : Type} {B : Type} -> (A -> B) -> Type
|
|
Weakly f = (x : A) (y : A) -> Path (f x) (f y)
|
|
|
|
Conditionally : {A : Type} {B : Type} -> (A -> B) -> Type
|
|
Conditionally f = (f' : Sq A -> B) * Path f (\x -> f' (inc x))
|
|
|
|
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 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)
|
|
|
|
const_c : (y : B) -> Conditionally {A} (\x -> y)
|
|
const_c y = (\x -> y, refl)
|
|
|
|
S1_connected : (f : S1 -> Bool) -> Constant f
|
|
S1_connected f = (f'.1, p) where
|
|
f' : (x : Bool) * Path x x
|
|
f' = S1Map_to_baseLoop f
|
|
|
|
p : (y : S1) -> Path f'.1 (f y)
|
|
p = S1_elim P refl loopc where
|
|
P : S1 -> Type
|
|
P = \y -> Path f'.1 (f y)
|
|
|
|
rr = refl {Bool} {f base}
|
|
|
|
loopc : PathP (\i -> P (loop i)) rr rr
|
|
loopc = transp (\i -> PathP_is_Path (\i -> P (loop i)) rr rr (inot i))
|
|
(Bool_isSet _ _ rr (transp (\i -> P (loop i)) rr))
|
|
|
|
isProp_isEquiv : {A : Type} {B : Type} {f : A -> B} -> isProp (isEquiv f)
|
|
isProp_isEquiv p q i y =
|
|
let
|
|
p2 = (p y).2
|
|
q2 = (q y).2
|
|
in
|
|
( p2 (q y).1 i
|
|
, \w j -> hcomp (\k [ (i = i0) -> p2 w j
|
|
, (i = i1) -> q2 w (ior j (inot k))
|
|
, (j = i0) -> p2 (q2 w (inot k)) i
|
|
, (j = i1) -> w ])
|
|
(inS (p2 w (ior i j)))
|
|
)
|
|
|
|
-- isProp_EqvSq : {P : Type} (x : Equiv P (Sq P)) (y : Equiv P (Sq P)) -> Path x y
|
|
-- isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (\i -> isEquiv (x1_is_y1 i)) x.2) y.2) where
|
|
-- x1_is_y1 : Path x.1 y.1
|
|
-- x1_is_y1 i e = sq (x.1 e) (y.1 e) i
|
|
|
|
equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B}
|
|
-> Path e.1 e'.1
|
|
-> Path e e'
|
|
equivLemma p = sigmaPath {A -> B} {\f -> isEquiv f} p (transp (\i -> PathP_is_Path (\i -> isEquiv (p i)) e.2 e'.2 (inot i)) (isProp_isEquiv {A} {B} {e'.1} _ _))
|
|
|
|
isProp_equiv : {P : Type} {Q : Type} -> Equiv P Q -> isProp P -> isProp Q
|
|
isProp_equiv eqv = transp (\i -> isProp (ua eqv i))
|
|
|
|
-- isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)
|
|
-- isProp_to_Sq_equiv prop = propExt prop sqProp inc proj where
|
|
-- proj : Sq P -> P
|
|
-- proj = Sq_rec prop (\x -> x)
|
|
|
|
-- sqProp : isProp (Sq P)
|
|
-- sqProp x y i = sq x y i
|
|
|
|
-- 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 = 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)
|
|
|
|
isContrRetract : {A : Type} {B : Type}
|
|
-> (f : A -> B) -> (g : B -> A)
|
|
-> (h : retract f g)
|
|
-> isContr B -> isContr A
|
|
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 ua idToEquiv) (f2 ua idToEquiv) (uaretSig ua idToEquiv (uaret {A})) singContr where
|
|
f1 : (ua : {B : Type} -> Equiv A B -> Path A B)
|
|
(idToEquiv : {B : Type} -> Path A B -> Equiv A B)
|
|
(p : (B : Type) * Equiv A B)
|
|
-> (B : Type) * Path A B
|
|
f1 ua idtoequiv p = (p.1, ua p.2)
|
|
|
|
f2 : (ua : {B : Type} -> Equiv A B -> Path A B)
|
|
(idToEquiv : {B : Type} -> Path A B -> Equiv A B)
|
|
(p : (B : Type) * Path A B)
|
|
-> (B : Type) * Equiv A B
|
|
f2 ua idtoequiv p = (p.1, idToEquiv p.2)
|
|
|
|
uaretSig : (ua : {B : Type} -> Equiv A B -> Path A B)
|
|
(idtoequiv : {B : Type} -> Path A B -> Equiv A B)
|
|
(uaret : {B : Type} (e : Equiv A B) -> Path (idToEquiv (ua e)) e)
|
|
-> (a : (B : Type) * Equiv A B) -> Path (f2 ua idtoequiv (f1 ua idtoequiv a)) a
|
|
uaretSig ua idtoequiv ret p i = (p.1, ret {p.1} p.2 i)
|
|
|
|
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 = 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)
|
|
|
|
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 (contrToProp (from y)) y
|
|
toFrom y = isProp_isProp {A} (contrToProp (from y)) y
|
|
|
|
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 = (center, contract) where
|
|
center : (A : Type) * Equiv A B
|
|
center = (B, idEquiv)
|
|
|
|
contract : (p : (A : Type) * Equiv A B) -> Path center p
|
|
contract w i =
|
|
let
|
|
sys : Partial (ior (inot i) i) ((A : Type) * Equiv A B)
|
|
sys = \ [ (i = i0) -> center, (i = i1) -> w ]
|
|
|
|
GlueB = Glue B sys
|
|
|
|
unglueB : GlueB -> B
|
|
unglueB x = unglue {B} (ior (inot i) i) {sys} x
|
|
|
|
unglueEquiv : isEquiv {GlueB} {B} unglueB
|
|
unglueEquiv b =
|
|
let
|
|
ctr : fiber unglueB b
|
|
ctr = ( glue {B} {ior (inot i) i} {sys} (\[ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.1 ])
|
|
(primComp (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
|
|
, fill (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
|
|
|
|
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 (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 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 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_fun : {A : Type} {B : Type} (P : (A : Type) -> (A -> B) -> Type)
|
|
-> P B id -> (e : Equiv A B) -> P A e.1
|
|
EquivJ_fun P r e = EquivJ_domain (\A e -> P A e.1) r 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 = 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 = JRefl (\B p -> Equiv A B) idEquiv
|
|
|
|
ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p
|
|
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 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
|
|
|
|
IsoJ : {B : Type} -> (Q : {A : Type} -> (A -> B) -> (B -> A) -> Type)
|
|
-> Q id id
|
|
-> {A : Type} (f : A -> B) (g : B -> A)
|
|
-> Path (\x -> g (f x)) id -> Path (\x -> f (g x)) id
|
|
-> Q f g
|
|
IsoJ Q h f g sfg rfg = rem1 f g sfg rfg where
|
|
P : (A : Type) -> (A -> B) -> Type
|
|
P A f = (g : B -> A) -> Path (\x -> g (f x)) id -> Path (\x -> f (g x)) id -> Q f g
|
|
|
|
rem : P B id
|
|
rem g sfg rfg = subst (Q id) (\i b -> sfg (inot i) b) h
|
|
|
|
rem1 : {A : Type} (f : A -> B) -> P A f
|
|
rem1 f g sfg rfg = EquivJ_fun P rem (IsoToEquiv (f, g, \i x -> rfg x i, \i x -> sfg x i)) g sfg rfg
|
|
|
|
total : {A : Type} {P : A -> Type} {Q : A -> Type}
|
|
-> ((x : A) -> P x -> Q x)
|
|
-> ((x : A) * P x) -> ((x : A) * Q x)
|
|
total f p = (p.1, f p.1 p.2)
|
|
|
|
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 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)
|
|
|
|
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 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} {(_, _)} (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))
|
|
(sym eq)
|
|
where p : P xv.1
|
|
p = peq.1
|
|
|
|
eq : Path {Q xv.1} xv.2 (f xv.1 p)
|
|
eq = peq.2
|
|
|
|
froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y
|
|
froTo apeq =
|
|
J {(a : A) * Q a} {total f (a, p)}
|
|
(\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)
|
|
where a : A
|
|
a = apeq.1.1
|
|
|
|
p : P a
|
|
p = apeq.1.2
|
|
|
|
eq : Path xv (total f (a, p))
|
|
eq = apeq.2
|
|
|
|
fiberEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
|
|
-> (f : (el : A) -> P el -> Q el)
|
|
-> isEquiv (total f)
|
|
-> (x : A) -> isEquiv (f x)
|
|
fiberEquiv f iseqv x y = isContrRetract {fiber (f x) y} {fiber (total f) (x, y)} eqv.2.1 eqv.1 eqv.2.2.1 (iseqv (x, y)) where
|
|
eqv : Iso (fiber (total f) (x, y)) (fiber (f x) y)
|
|
eqv = total_fibers f
|
|
|
|
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 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)
|
|
)
|
|
|
|
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 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 (toId x))
|
|
totalEquiv x = contrIsEquiv (rContr x) singContr (total (toId x))
|
|
|
|
isSet_Coproduct : {A : Type} {B : Type} -> isSet A -> isSet B -> isSet (Coproduct A B)
|
|
isSet_Coproduct setA setB = Req_isProp where
|
|
T = Coproduct A B
|
|
|
|
R : T -> T -> Type
|
|
R = \case
|
|
inl x -> \case
|
|
inl y -> Path x y
|
|
inr x -> Bottom
|
|
push c i -> absurd c
|
|
inr x -> \case
|
|
inl x -> Bottom
|
|
inr y -> Path x y
|
|
push c i -> absurd c c
|
|
|
|
R_prop : (x : T) (y : T) -> isProp (R x y)
|
|
R_prop = \case
|
|
inl x -> \case
|
|
inl y -> setA x y
|
|
inr y -> \p q -> absurd p
|
|
push c i -> absurd c
|
|
inr x -> \case
|
|
inl y -> \p q -> absurd p
|
|
inr y -> setB x y
|
|
push c i -> absurd c
|
|
|
|
R_refl : (x : T) -> R x x
|
|
R_refl = \case
|
|
inl x -> refl
|
|
inr x -> refl
|
|
push c i -> absurd c
|
|
|
|
R_impliesEq : (x : T) (y : T) -> R x y -> Path x y
|
|
R_impliesEq = \case
|
|
inl x -> \case
|
|
inl y -> \p -> ap inl p
|
|
inr y -> \p -> absurd p
|
|
push c i -> absurd c
|
|
inr x -> \case
|
|
inl y -> \p -> absurd p
|
|
inr y -> \p -> ap inr p
|
|
push c i -> absurd c
|
|
|
|
Req_isEquiv : {x : T} {y : T} -> Equiv (R x y) (Path x y)
|
|
Req_isEquiv = (R_impliesEq x y, theorem722 R_prop R_refl R_impliesEq)
|
|
|
|
Req_isProp : (x : T) (y : T) -> isProp (Path x y)
|
|
Req_isProp x y = isProp_equiv {R x y} {Path x y} (Req_isEquiv {x} {y}) (R_prop x y)
|
|
|
|
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 : {n : Nat} {A : Type} -> isOfHLevel (nTrunc A n) n
|
|
nTrunc_isOfHLevel = spheresFull_hLevel {nTrunc A n} n (\f -> (hub f, \x i -> spoke f x i))
|
|
|
|
nTrunc_rec : {n : Nat} {A : Type} {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
|
|
|
|
nTrunc_lift : {A : Type} {B : Type} {n : Nat} -> (A -> B) -> nTrunc A n -> nTrunc B n
|
|
nTrunc_lift f = nTrunc_rec (nTrunc_isOfHLevel {n} {B}) (\x -> incn {B} {n} (f x))
|
|
|
|
-- data W (A : Type) (B : A -> Type) : Type where
|
|
-- sup : (a : A) -> (B a -> W A B) -> W A B
|
|
|
|
-- Welim : {A : Type} {B : A -> Type} (P : W A B -> Type)
|
|
-- -> (sup : (a : A) (f : B a -> W A B) (g : (x : B a) -> P (f x)) -> P (sup a f))
|
|
-- -> (c : W A B) -> P c
|
|
-- Welim P k = \case
|
|
-- sup a f -> k a f (\x -> Welim P k (f x))
|
|
|
|
-- wnat : Type
|
|
-- wnat = W Bool (if Unit Bottom)
|
|
|
|
-- wzero : wnat
|
|
-- wzero = sup false absurd
|
|
|
|
-- wsucc : wnat -> wnat
|
|
-- wsucc n = sup true (\x -> n)
|
|
|
|
-- wnat_elim : (P : wnat -> Type) (pz : P wzero) (ps : (c : wnat) -> P c -> P (wsucc c)) -> (x : wnat) -> P x
|
|
-- wnat_elim P pz ps x = Welim P (\a f g -> helper a f g) x where
|
|
-- A = Bool
|
|
-- B = if Unit Bottom
|
|
|
|
-- helper : (a : A) (f : B a -> W A B) (g : (x : B a) -> P (f x)) -> P (sup a f)
|
|
-- helper = \case
|
|
-- false -> \f g -> pz
|
|
-- true -> \f g ->
|
|
-- let
|
|
-- t : P (sup true (\x -> f tt))
|
|
-- t = ps (f tt) (g tt)
|
|
-- in transp (\i -> P (sup true (\x -> f (unitEta x (inot i))))) t
|
|
|
|
-- nat_is_wnat : Path Nat wnat
|
|
-- nat_is_wnat = IsoToId (to, from, toFrom, fromTo) where
|
|
-- to : Nat -> wnat
|
|
-- to = Nat_elim (\x -> wnat) wzero (\_ x -> wsucc x)
|
|
|
|
-- from : wnat -> Nat
|
|
-- from = wnat_elim (\x -> Nat) zero (\_ x -> succ x)
|
|
|
|
-- toFrom : (y : wnat) -> Path (to (from y)) y
|
|
-- toFrom = wnat_elim (\x -> Path (to (from x)) x) refl (\x y -> ap wsucc y)
|
|
|
|
-- fromTo : (x : Nat) -> Path (from (to x)) x
|
|
-- fromTo = Nat_elim (\x -> Path (from (to x)) x) refl (\x y -> ap succ y)
|
|
|
|
-- plusWnat : wnat -> wnat -> wnat
|
|
-- plusWnat = subst (\x -> x -> x -> x) nat_is_wnat plusNat
|
|
|
|
-- Pointed : Type
|
|
-- Pointed = (X : Type) * X * isSet X
|
|
|
|
-- Set : Type
|
|
-- Set = (X : Type) * isSet X
|
|
|
|
-- map : Set -> Set -> Type
|
|
-- map A B = A.1 -> B.1
|
|
|
|
-- pmap : Pointed -> Pointed -> Type
|
|
-- pmap A B = (f : A.1 -> B.1) * Path (f A.2.1) B.2.1
|
|
|
|
-- Zero : Pointed
|
|
-- Zero = (Unit, tt, isProp_isSet l) where
|
|
-- l : (a : Unit) (b : Unit) -> Path a b
|
|
-- l = \case
|
|
-- tt -> \case
|
|
-- tt -> refl
|
|
|
|
-- compose : {A : Pointed} {B : Pointed} {C : Pointed} -> pmap B C -> pmap A B -> pmap A C
|
|
-- compose g f = (\x -> g.1 (f.1 x), subst (\x -> Path (g.1 x) C.2.1) (sym f.2) g.2)
|
|
|
|
-- id : {A : Pointed} -> pmap A A
|
|
-- id = (\x -> x, refl)
|
|
|
|
-- initial : {A : Pointed} -> pmap Zero A
|
|
-- initial = (\_ -> A.2.1, refl)
|
|
|
|
-- terminal : {A : Pointed} -> pmap A Zero
|
|
-- terminal = (\_ -> tt, refl)
|
|
|
|
-- cast : {A : Pointed} {B : Pointed} -> pmap A B
|
|
-- cast = compose {A} {Zero} {B} (initial {B}) (terminal {A})
|
|
|
|
-- Product : Pointed -> Pointed -> Pointed
|
|
-- Product A B = (A.1 * B.1, (A.2.1, B.2.1), isSet_prod A.2.2 B.2.2)
|
|
|
|
-- proj1 : {A : Pointed} {B : Pointed} -> pmap (Product A B) A
|
|
-- proj1 = (\x -> x.1, refl)
|
|
|
|
-- proj2 : {A : Pointed} {B : Pointed} -> pmap (Product A B) B
|
|
-- proj2 = (\x -> x.2, refl)
|
|
|
|
-- cross : {G : Pointed} {A : Pointed} {B : Pointed} -> pmap G A -> pmap G B -> pmap G (Product A B)
|
|
-- cross f g = (\x -> (f.1 x, g.1 x), \i -> (f.2 i, g.2 i))
|
|
|
|
-- inj1 : {A : Pointed} {B : Pointed} -> pmap A (Product A B)
|
|
-- inj1 = cross {A} {A} {B} (id {A}) (cast {A} {B})
|
|
|
|
-- inj2 : {A : Pointed} {B : Pointed} -> pmap B (Product A B)
|
|
-- inj2 = cross {B} {A} {B} (cast {B} {A}) (id {B})
|
|
|
|
-- pmap_equal : {A : Pointed} {B : Pointed} (f : pmap A B) (g : pmap A B) -> Path f.1 g.1 -> Path f g
|
|
-- pmap_equal f g p = sigmaPath {A.1 -> B.1} {\f -> Path (f A.2.1) B.2.1} p (transp (\i -> PathP_is_Path (\i -> Path (p i A.2.1) B.2.1) f.2 g.2 (inot i)) (B.2.2 _ _ _ _))
|
|
|
|
-- zero_comp : {A : Pointed} {B : Pointed} {C : Pointed} (f : pmap B C)
|
|
-- -> Path (compose {A} {B} {C} f (cast {A} {B})) (cast {A} {C})
|
|
-- zero_comp f = pmap_equal {A} {C} _ _ (\i x -> f.2 i)
|
|
|
|
-- Forget : Pointed -> Set
|
|
-- Forget P = (P.1, P.2.2)
|
|
|
|
-- Free : Set -> Pointed
|
|
-- Free P = (Coproduct P.1 Unit, inr tt, Coproduct_isSet P.2 unitSet)
|
|
|
|
Precategory : Type
|
|
Precategory = (Ob : Type)
|
|
* (Hom : Ob -> Ob -> Type)
|
|
* (hset : (A : Ob) (B : Ob) -> isSet (Hom A B))
|
|
* (id : {A : Ob} -> Hom A A)
|
|
* (compose : {A : Ob} {B : Ob} {C : Ob} -> Hom B C -> Hom A B -> Hom A C)
|
|
* (idl : {A : Ob} {B : Ob} (f : Hom A B) -> Path (compose id f) f)
|
|
* (idr : {A : Ob} {B : Ob} (f : Hom A B) -> Path (compose f id) f)
|
|
* ({A : Ob} {B : Ob} {C : Ob} {D : Ob}
|
|
-> (f : Hom C D) (g : Hom B C) (h : Hom A B)
|
|
-> Path (compose f (compose g h)) (compose (compose f g) h))
|
|
|
|
Ob : (C : Precategory) -> Type
|
|
Ob C = C.1
|
|
|
|
Hom : (C : Precategory) -> Ob C -> Ob C -> Type
|
|
Hom C = C.2.1
|
|
|
|
homSet : {C : Precategory} (A : Ob C) (B : Ob C) -> isSet (Hom C A B)
|
|
homSet = C.2.2.1
|
|
|
|
Cid : (C : Precategory) {A : Ob C} -> Hom C A A
|
|
Cid C = C.2.2.2.1
|
|
|
|
compose : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} {C : Ob Cat}
|
|
-> Hom Cat B C -> Hom Cat A B -> Hom Cat A C
|
|
compose = Cat.2.2.2.2.1
|
|
|
|
leftId : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat}
|
|
-> (f : Hom Cat A B) -> Path (compose {Cat} (Cid Cat) f) f
|
|
leftId = Cat.2.2.2.2.2.1
|
|
|
|
rightId : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat}
|
|
-> (f : Hom Cat A B) -> Path (compose {Cat} f (Cid Cat)) f
|
|
rightId = Cat.2.2.2.2.2.2.1
|
|
|
|
assocCompose : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} {C : Ob Cat} {D : Ob Cat}
|
|
-> (f : Hom Cat C D) (g : Hom Cat B C) (h : Hom Cat A B)
|
|
-> Path (compose {Cat} f (compose {Cat} g h)) (compose {Cat} (compose {Cat} f g) h)
|
|
assocCompose = Cat.2.2.2.2.2.2.2
|
|
|
|
Opposite : Precategory -> Precategory
|
|
Opposite Cat =
|
|
( Cat.1
|
|
, \A B -> Cat.2.1 B A
|
|
, \A B -> Cat.2.2.1 B A
|
|
, Cat.2.2.2.1
|
|
, \f g -> compose {Cat} g f
|
|
, \f -> rightId {Cat} f
|
|
, \f -> leftId {Cat} f
|
|
, \f g h i -> assocCompose {Cat} h g f (inot i)
|
|
)
|
|
|
|
Coprod : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
|
|
Coprod A B = (sum : Ob Cat)
|
|
* (inl : Hom Cat A sum)
|
|
* (inr : Hom Cat B sum)
|
|
* (elim : {S : Ob Cat} -> Hom Cat A S -> Hom Cat B S -> Hom Cat sum S)
|
|
* (eliml : {S : Ob Cat} (f : Hom Cat A S) (g : Hom Cat B S)
|
|
-> Path (compose {Cat} (elim f g) inl) f)
|
|
* ({S : Ob Cat} (f : Hom Cat A S) (g : Hom Cat B S)
|
|
-> Path (compose {Cat} (elim f g) inr) g)
|
|
|
|
Product : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
|
|
Product = Coprod {Opposite Cat}
|
|
|
|
Set : Precategory
|
|
Set = (T, \A B -> A.1 -> B.1, homset, \x -> x, \g f x -> g (f x), \f -> refl, \f -> refl, \f g h -> refl) where
|
|
T = (X : Type) * isSet X
|
|
|
|
homset : (A : T) (B : T) -> isSet (A.1 -> B.1)
|
|
homset A B = isSet_pi (\_ -> B.2)
|
|
|
|
nat : Ob Set
|
|
nat = (Nat, Nat_isSet)
|
|
|
|
setCoprod : (A : Ob Set) (B : Ob Set) -> Coprod {Set} A B
|
|
setCoprod A B = (T, inl, inr, elim, \f g i x -> f x, \f g i x -> g x) where
|
|
T : Ob Set
|
|
T = (Coproduct A.1 B.1, isSet_Coproduct A.2 B.2)
|
|
|
|
elim : {S : Ob Set} -> Hom Set A S -> Hom Set B S -> Hom Set T S
|
|
elim f g = \case
|
|
inl x -> f x
|
|
inr x -> g x
|
|
push c i -> absurd c
|
|
|
|
setProd : (A : Ob Set) (B : Ob Set) -> Product {Set} A B
|
|
setProd A B = (T, \x -> x.1, \x -> x.2, \{S} -> cross {S}, \f g i -> f, \f g i -> g) where
|
|
T : Ob Set
|
|
T = (A.1 * B.1, isSet_prod A.2 B.2)
|
|
|
|
cross : {S : Ob Set} -> Hom Set S A -> Hom Set S B -> Hom Set S T
|
|
cross f g x = (f x, g x)
|
|
|
|
isIsoHom : {Cat : Precategory} {A : Ob Cat} {B : Ob Cat} -> Hom Cat A B -> Type
|
|
isIsoHom f = (inv : Hom Cat B A) * Path (compose {Cat} f inv) (Cid Cat) * Path (compose {Cat} inv f) (Cid Cat)
|
|
|
|
Isomorphism : {Cat : Precategory} -> Ob Cat -> Ob Cat -> Type
|
|
Isomorphism A B = (f : Hom Cat A B) * isIsoHom {Cat} {A} {B} f
|
|
|
|
isCategory : Precategory -> Type
|
|
isCategory Cat = (A : Ob Cat) (B : Ob Cat) -> Equiv (Path A B) (Isomorphism {Cat} A B)
|
|
|
|
-- setIsCategory : isCategory Set
|
|
-- setIsCategory A B = IsoToEquiv (pathTo, fromIso, pathTo_fromIso, _) where
|
|
-- pathTo : Path A B -> Isomorphism {Set} A B
|
|
-- pathTo = J {Ob Set} {A} (\B _ -> Isomorphism {Set} A B) (id, id, refl, refl)
|
|
--
|
|
-- augment : Path A.1 B.1 -> Path A B
|
|
--
|
|
-- fromIso : Isomorphism {Set} A B -> Path A B
|
|
-- fromIso iso = augment (IsoJ (\{A} f g -> Path A B.1) refl iso.1 iso.2.1 iso.2.2.2 iso.2.2.1)
|
|
--
|
|
-- augment p = sigmaPath {Type} {isSet} p (transp (\i -> PathP_is_Path (\j -> isSet (p j)) A.2 B.2 (inot i)) (isSet_isProp {B.1} (transp (\i -> isSet (p i)) A.2) B.2))
|
|
--
|
|
-- pathTo_fromIso : (i : Isomorphism {Set} A B) -> Path (pathTo (fromIso i)) i
|
|
-- pathTo_fromIso iso i = (iso.1, iso.2.1, iso.2.2.1, iso.2.2.2)
|
|
|
|
sym_subst : {A : Type} {x : A} {y : A} -> Path x y -> Path y x
|
|
sym_subst p = subst (\y -> Path y x) p refl
|
|
|
|
trans_subst : {A : Type} {x : A} {y : A} {z : A} -> Path x y -> Path y z -> Path x z
|
|
trans_subst p q = subst (\y -> Path y z -> Path x z) p id q
|
|
|
|
data Unlist (A : Type) : Type where
|
|
uncons : A -> Unlist A -> Unlist A
|
|
|
|
unelim : {A : Type}
|
|
(P : Unlist A -> Type)
|
|
-> ((x : A) (tail : Unlist A) -> P tail -> P (uncons x tail))
|
|
-> (x : Unlist A) -> P x
|
|
unelim P c = \case
|
|
uncons x xs -> c x xs (unelim P c xs)
|
|
|
|
contra : {A : Type} -> Unlist A -> Bottom
|
|
contra = unelim (\x -> Bottom) (\_ _ x -> x)
|
|
|
|
plusInt : Int -> Int -> Int
|
|
plusInt x y = winding (trans (goAround x) (goAround y))
|
|
|
|
add : Nat -> Nat -> Nat
|
|
add = Nat_elim (\ _ -> Nat -> Nat) (\ x -> x) (\n k x -> succ (k x))
|
|
|
|
addAssoc : (i : Nat) (j : Nat) (k : Nat) -> Path (add i (add j k)) (add (add i j) k)
|
|
addAssoc = Nat_elim (\ i -> (j : Nat) (k : Nat) -> Path (add i (add j k)) (add (add i j) k)) (\j k -> refl) (\n assoc j k -> ap succ (assoc j k))
|
|
|
|
Jsym : {A : Type} {x : A} {y : A} -> Path x y -> Path y x
|
|
Jsym = J (\y _ -> Path y x) refl
|
|
|
|
Vect : Type -> Nat -> Type
|
|
Vect A = \case
|
|
zero -> Unit
|
|
succ n -> A * Vect A n
|
|
|
|
Vect_elim : {A : Type} (P : {n : Nat} -> Vect A n -> Type)
|
|
-> P {zero} tt
|
|
-> ({n : Nat} (x : A) (xs : Vect A n) -> P {n} xs -> P {succ n} (x, xs))
|
|
-> {n : Nat} (x : Vect A n) -> P {n} x
|
|
Vect_elim P nil cons {n} x = go n x where
|
|
go : (n : Nat) (x : Vect A n) -> P x
|
|
go = \case
|
|
zero -> \case
|
|
tt -> nil
|
|
succ n -> \xs -> cons {n} xs.1 xs.2 (go n xs.2)
|
|
|
|
head : {A : Type} {n : Nat} -> Vect A (succ n) -> A
|
|
head xs = xs.1
|
|
|
|
tail : {A : Type} {n : Nat} -> Vect A (succ n) -> Vect A n
|
|
tail xs = xs.2
|
|
|
|
equivToIso : {A : Type} {B : Type} (f : A -> B) -> isEquiv f -> isIso f
|
|
equivToIso f e = EquivJ (\X Y f -> isIso f.1) (\x -> (id, \x -> refl, \x -> refl)) (f, e)
|