|
|
- -- 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.
- singContr : {A : Type} {a : A} -> isContr (Singl A a)
- 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.
- 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
-
- -- 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,
- --
- -- isHSet A = (x : A) (y : A) -> isHProp (Path x y)
- --
-
- isProp : Type -> Type
- isProp A = (x : A) (y : A) -> Path x y
-
- isHSet : Type -> Type
- isHSet 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 : isHSet 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
-
- succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y
- succInj p i = pred (p i) where
- pred : Nat -> Nat
- pred = \case
- zero -> zero
- succ x -> x
-
- -- 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
-
- winding : Path base base -> Int
- winding p = transp (\i -> helix (p i)) (pos zero)
-
- -- 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 -> forwards n
- neg n -> backwards n
- where
- forwards : Nat -> Path base base
- forwards = \case
- zero -> refl
- succ n -> trans (goAround (pos n)) (\i -> loop i)
- backwards : Nat -> Path base base
- backwards = \case
- zero -> \i -> loop (inot i)
- succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
-
- 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)
-
- 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
-
- -- 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) ]
-
- -- The name is due to the category-theoretical notion of pushout.
- -- TODO: finish writing this tomorrow lol
-
- 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))
-
- 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
-
- 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)) (boolAnd (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 -> isHSet 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)
-
- 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
-
- 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)
-
- 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))
-
- pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isHSet A
- 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
- uipRefl x p = K {x} (\q -> Path refl q) refl p
-
- Nat_isSet : isHSet Nat
- Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
-
- Bool_isSet : isHSet 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, 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 : {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
- 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 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 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 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 = 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_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
-
- 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))
-
- 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
|