less prototype, less bad code implementation of CCHM type theory
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

1054 lines
34 KiB

  1. -- We begin by adding some primitive bindings using the PRIMITIVE pragma.
  2. --
  3. -- It goes like this: PRIMITIVE primName varName.
  4. --
  5. -- If the varName is dropped, then it's taken to be the same as primName.
  6. --
  7. -- If there is a previous declaration for the varName, then the type
  8. -- is checked against the internally-known "proper" type for the primitive.
  9. -- Universe of fibrant types
  10. {-# PRIMITIVE Type #-}
  11. -- Universe of non-fibrant types
  12. {-# PRIMITIVE Pretype #-}
  13. -- Fibrant is a fancy word for "has a composition structure". Most types
  14. -- we inherit from MLTT are fibrant:
  15. --
  16. -- Stuff like products Π, sums Σ, naturals, booleans, lists, etc., all
  17. -- have composition structures.
  18. --
  19. -- The non-fibrant types are part of the structure of cubical
  20. -- categories: The interval, partial elements, cubical subtypes, ...
  21. -- The interval
  22. ---------------
  23. -- The interval has two endpoints i0 and i1.
  24. -- These form a de Morgan algebra.
  25. I : Pretype
  26. {-# PRIMITIVE Interval I #-}
  27. i0, i1 : I
  28. {-# PRIMITIVE i0 #-}
  29. {-# PRIMITIVE i1 #-}
  30. -- "minimum" on the interval
  31. iand : I -> I -> I
  32. {-# PRIMITIVE iand #-}
  33. -- "maximum" on the interval.
  34. ior : I -> I -> I
  35. {-# PRIMITIVE ior #-}
  36. -- The interpretation of iand as min and ior as max justifies the fact that
  37. -- ior i (inot i) != i1, since that equality only holds for the endpoints.
  38. -- inot i = 1 - i is a de Morgan involution.
  39. inot : I -> I
  40. {-# PRIMITIVE inot #-}
  41. -- Paths
  42. --------
  43. -- Since every function in type theory is internally continuous,
  44. -- and the two endpoints i0 and i1 are equal, we can take the type of
  45. -- equalities to be continuous functions out of the interval.
  46. -- That is, x ≡ y iff. ∃ f : I -> A, f i0 = x, f i1 = y.
  47. -- The type PathP generalises this to dependent products (i : I) -> A i.
  48. PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
  49. {-# PRIMITIVE PathP #-}
  50. -- By taking the first argument to be constant we get the equality type
  51. -- Path.
  52. Path : {A : Type} -> A -> A -> Type
  53. Path {A} = PathP (\i -> A)
  54. -- reflexivity is given by constant paths
  55. refl : {A : Type} {x : A} -> Path x x
  56. refl {A} {x} i = x
  57. -- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that
  58. -- sym p i0 = p (inot i0) = p i1
  59. -- sym p i1 = p (inot i1) = p i0
  60. -- This has the correct endpoints.
  61. sym : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
  62. sym p i = p (inot i)
  63. id : {A : Type} -> A -> A
  64. id x = x
  65. the : (A : Type) -> A -> A
  66. the A x = x
  67. -- The eliminator for the interval says that if you have x : A i0 and y : A i1,
  68. -- and x ≡ y, then you can get a proof A i for every element of the interval.
  69. iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
  70. iElim p i = p i
  71. -- This corresponds to the elimination principle for the HIT
  72. -- data I : Pretype where
  73. -- i0 i1 : I
  74. -- seg : i0 ≡ i1
  75. -- The singleton subtype of A at x is the type of elements of y which
  76. -- are equal to x.
  77. Singl : (A : Type) -> A -> Type
  78. Singl A x = (y : A) * Path x y
  79. -- Contractible types are those for which there exists an element to which
  80. -- all others are equal.
  81. isContr : Type -> Type
  82. isContr A = (x : A) * ((y : A) -> Path x y)
  83. -- Using the connection \i j -> y.2 (iand i j), we can prove that
  84. -- singletons are contracible. Together with transport later on,
  85. -- we get the J elimination principle of paths.
  86. singContr : {A : Type} {a : A} -> isContr (Singl A a)
  87. singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
  88. -- Some more operations on paths. By rearranging parentheses we get a
  89. -- proof that the images of equal elements are themselves equal.
  90. cong : {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)
  91. cong f p i = f (p i)
  92. -- These satisfy definitional equalities, like congComp and congId, which are
  93. -- propositional in vanilla MLTT.
  94. congComp : {A : Type} {B : Type} {C : Type}
  95. {f : A -> B} {g : B -> C} {x : A} {y : A}
  96. (p : Path x y)
  97. -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)
  98. congComp p = refl
  99. congId : {A : Type} {x : A} {y : A}
  100. (p : Path x y)
  101. -> Path (cong (id {A}) p) p
  102. congId p = refl
  103. -- Just like rearranging parentheses gives us cong, swapping the value
  104. -- and interval binders gives us function extensionality.
  105. funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
  106. (h : (x : A) -> Path (f x) (g x))
  107. -> Path f g
  108. funext h i x = h x i
  109. -- The proposition associated with an element of the interval
  110. -------------------------------------------------------------
  111. -- Associated with every element i : I of the interval, we have the type
  112. -- IsOne i which is inhabited only when i = i1. In the model, this
  113. -- corresponds to the map [φ] from the interval cubical set to the
  114. -- subobject classifier.
  115. IsOne : I -> Pretype
  116. {-# PRIMITIVE IsOne #-}
  117. -- The value itIs1 witnesses the fact that i1 = i1.
  118. itIs1 : IsOne i1
  119. {-# PRIMITIVE itIs1 #-}
  120. -- Partial elements
  121. -------------------
  122. --
  123. -- Since a function I -> A has two endpoints, and a function I -> I -> A
  124. -- has four endpoints + four functions I -> A as "sides" (obtained by
  125. -- varying argument while holding the other as a bound variable), we
  126. -- refer to elements of I^n -> A as "cubes".
  127. -- This justifies the existence of partial elements, which are, as the
  128. -- name implies, partial cubes. Namely, a Partial φ A is an element of A
  129. -- which depends on a proof that IsOne φ.
  130. Partial : I -> Type -> Pretype
  131. {-# PRIMITIVE Partial #-}
  132. -- There is also a dependent version where the type A is itself a
  133. -- partial element.
  134. PartialP : (phi : I) -> Partial phi Type -> Pretype
  135. {-# PRIMITIVE PartialP #-}
  136. -- Why is Partial φ A not just defined as φ -> A? The difference is that
  137. -- Partial φ A has an internal representation which definitionally relates
  138. -- any two partial elements which "agree everywhere", that is, have
  139. -- equivalent values for every possible assignment of variables which
  140. -- makes IsOne φ hold.
  141. -- Cubical Subtypes
  142. --------------------
  143. -- Given A : Type, phi : I, and a partial element u : A defined on φ,
  144. -- we have the type Sub A phi u, notated A[phi -> u] in the output of
  145. -- the type checker, whose elements are "extensions" of u.
  146. -- That is, element of A[phi -> u] is an element of A defined everywhere
  147. -- (a total element), which, when IsOne φ, agrees with u.
  148. Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype
  149. {-# PRIMITIVE Sub #-}
  150. -- Every total element u : A can be made partial on φ by ignoring the
  151. -- constraint. Furthermore, this "totally partial" element agrees with
  152. -- the original total element on φ.
  153. inS : {A : Type} {phi : I} (u : A) -> Sub A phi (\x -> u)
  154. {-# PRIMITIVE inS #-}
  155. -- When IsOne φ, outS {A} {φ} {u} x reduces to u itIs1.
  156. -- This implements the fact that x agrees with u on φ.
  157. outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A
  158. {-# PRIMITIVE outS #-}
  159. -- The composition operation
  160. ----------------------------
  161. -- Now that we have syntax for specifying partial cubes,
  162. -- and specifying that an element agrees with a partial cube,
  163. -- we can describe the composition operation.
  164. comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1
  165. {-# PRIMITIVE comp #-}
  166. -- In particular, when φ is a disjunction of the form
  167. -- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a
  168. -- "tube", an open square with no floor or roof:
  169. --
  170. -- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,
  171. -- we draw:
  172. --
  173. -- x q i1
  174. -- | |
  175. -- \j -> x | | \j -> q j
  176. -- | |
  177. -- x q i0
  178. --
  179. -- The composition operation says that, as long as we can provide a
  180. -- "floor" connecting x -- q i0, as a total element of A which, on
  181. -- phi, extends u i0, then we get the "roof" connecting x and q i1
  182. -- for free.
  183. --
  184. -- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the
  185. -- "floor", and composition gets us the dotted line:
  186. --
  187. -- x..........z
  188. -- | |
  189. -- x | | q j
  190. -- | |
  191. -- x----------y
  192. -- p i
  193. trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z
  194. trans {A} {x} p q i =
  195. comp (\i -> A)
  196. {ior i (inot i)}
  197. (\j [ (i = i0) -> x, (i = i1) -> q j ])
  198. (inS (p i))
  199. -- In particular when the formula φ = i0 we get the "opposite face" to a
  200. -- single point, which corresponds to transport.
  201. transp : (A : I -> Type) (x : A i0) -> A i1
  202. transp A x = comp A {i0} (\i [ ]) (inS x)
  203. -- Since we have the iand operator, we can also derive the *filler* of a cube,
  204. -- which connects the given face and the output of composition.
  205. fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i
  206. fill A {phi} u a0 i =
  207. comp (\j -> A (iand i j))
  208. {ior phi (inot i)}
  209. (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
  210. (inS (outS a0))
  211. hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> I -> A
  212. hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
  213. hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A
  214. hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0
  215. -- For instance, the filler of the previous composition square
  216. -- tells us that trans p refl = p:
  217. transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
  218. transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
  219. transpFill : {A : Type} (x : A) -> Path x (transp (\i -> A) x)
  220. transpFill {A} x i = fill (\i -> A) (\k []) (inS x) i
  221. -- Reduction of composition
  222. ---------------------------
  223. --
  224. -- Composition reduces on the structure of the family A : I -> Type to create
  225. -- the element a1 : (A i1)[phi -> u i1].
  226. --
  227. -- For instance, when filling a cube of functions, the behaviour is to
  228. -- first transport backwards along the domain, apply the function, then
  229. -- forwards along the codomain.
  230. transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path C D)
  231. -> (f : A -> C) -> Path (transp (\i -> p i -> q i) f)
  232. (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))
  233. transpFun p q f = refl
  234. -- transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}
  235. -- -> (f : (x : A i0) -> B i0 x)
  236. -- -> Path (transp (\i -> (x : A i) -> B i x) f)
  237. -- (\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)))
  238. -- transpDFun f = refl
  239. -- When considering the more general case of a composition respecing sides,
  240. -- the outer transport becomes a composition.
  241. -- Glueing and Univalence
  242. -------------------------
  243. -- First, let's get some definitions out of the way.
  244. --
  245. -- The *fiber* of a function f : A -> B at a point y : B is the type of
  246. -- inputs x : A which f takes to y, that is, for which there exists a
  247. -- path f(x) = y.
  248. fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type
  249. fiber f y = (x : A) * Path (f x) y
  250. -- An *equivalence* is a function where every fiber is contractible.
  251. -- That is, for every point in the codomain y : B, there is exactly one
  252. -- point in the input which f maps to y.
  253. isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type
  254. isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)
  255. -- By extracting this point, which must exist because the fiber is contractible,
  256. -- we can get an inverse of f:
  257. inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
  258. inverse eqv y = (eqv y) .1 .1
  259. -- We can prove that «inverse eqv» is a section of f:
  260. section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
  261. section f eqv i y = (eqv y) .1 .2 i
  262. contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A
  263. contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))
  264. -- Proving that it's also a retraction is left as an exercise to the
  265. -- reader. We can package together a function and a proof that it's an
  266. -- equivalence to get a capital-E Equivalence.
  267. Equiv : (A : Type) (B : Type) -> Type
  268. Equiv A B = (f : A -> B) * isEquiv {A} {B} f
  269. -- The identity function is an equivalence between any type A and
  270. -- itself.
  271. idEquiv : {A : Type} -> isEquiv (id {A})
  272. idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))
  273. -- The glue operation expresses that "extensibility is invariant under
  274. -- equivalence". Less concisely, the Glue type and its constructor,
  275. -- glue, let us extend a partial element of a partial type to a total
  276. -- element of a total type, by "gluing" the partial type T using a
  277. -- partial equivalence e onto a total type A.
  278. -- In particular, we have that when φ = i1, Glue A [i1 -> (T, f)] = T.
  279. primGlue : (A : Type) {phi : I}
  280. (T : Partial phi Type)
  281. (e : PartialP phi (\o -> Equiv (T o) A))
  282. -> Type
  283. {-# PRIMITIVE Glue primGlue #-}
  284. -- The glue constructor extends the partial element t : T to a total
  285. -- element of Glue A [φ -> (T, e)] as long as we have a total im : A
  286. -- which is the image of f(t).
  287. --
  288. -- Agreeing with the condition that Glue A [i1 -> (T, e)] = T,
  289. -- we have that glue {A} {i1} t im => t.
  290. prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}
  291. -> (t : PartialP phi T)
  292. -> (im : Sub A phi (\o -> (e o).1 (t o)))
  293. -> primGlue A T e
  294. {-# PRIMITIVE glue prim'glue #-}
  295. -- The unglue operation undoes a glueing. Since when φ = i1,
  296. -- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ...
  297. -- will have type T, and so to get back an A we need to apply the
  298. -- partial equivalence f (defined everywhere).
  299. primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}
  300. -> primGlue A {phi} T e -> A
  301. {-# PRIMITIVE unglue primUnglue #-}
  302. -- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn
  303. -- as giving us the dotted line in:
  304. --
  305. -- T i0 ......... T i1
  306. -- | |
  307. -- | |
  308. -- e i0 |~ ~| e i1
  309. -- | |
  310. -- | |
  311. -- A i0 --------- A i1
  312. -- A
  313. --
  314. -- Where the the two "e" sides are equivalences, and the bottom side is
  315. -- the line i : I |- A.
  316. --
  317. -- Thus, by choosing a base type, a set of partial types and partial
  318. -- equivalences, we can make a line between two types (T i0) and (T i1).
  319. Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type
  320. Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
  321. -- For example, we can glue together the type A and the type B as long
  322. -- as there exists an Equiv A B.
  323. --
  324. -- A ............ B
  325. -- | |
  326. -- | |
  327. -- equiv |~ ua equiv ~| idEquiv {B}
  328. -- | |
  329. -- | |
  330. -- B ------------ B
  331. -- \i → B
  332. --
  333. univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B
  334. univalence {A} {B} equiv i =
  335. Glue B (\[ (i = i0) -> (A, equiv),
  336. (i = i1) -> (B, the B, idEquiv {B}) ])
  337. -- The fact that this diagram has 2 filled-in B sides explains the
  338. -- complication in the proof below.
  339. --
  340. -- In particular, the actual behaviour of transp (\i -> univalence f i)
  341. -- (x : A) is not just to apply f x to get a B (the left side), it also
  342. -- needs to:
  343. --
  344. -- * For the bottom side, compose along (\i -> B) (the bottom side)
  345. -- * For the right side, apply the inverse of the identity, which
  346. -- is just identity, to get *some* b : B
  347. --
  348. -- But that b : B might not agree with the sides of the composition
  349. -- operation in a more general case, so it composes along (\i -> B)
  350. -- *again*!
  351. --
  352. -- Thus the proof: a simple cubical argument suffices, since
  353. -- for any composition, its filler connects either endpoints. So
  354. -- we need to come up with a filler for the bottom and right faces.
  355. univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1
  356. univalenceBeta {A} {B} f i a =
  357. let
  358. -- The bottom left corner
  359. botLeft : B
  360. botLeft = transp (\i -> B) (f.1 a)
  361. -- The "bottom face" filler connects the bottom-left corner, f.1 a,
  362. -- and the bottom-right corner, which is the transport of f.1 a
  363. -- along \i -> B.
  364. botFace : Path (f.1 a) botLeft
  365. botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i
  366. -- The "right face" filler connects the bottom-right corner and the
  367. -- upper-right corner, which is again a simple transport along
  368. -- \i -> B.
  369. rightFace : Path (transp (\i -> B) botLeft) botLeft
  370. rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)
  371. -- The goal is a path between the bottom-left and top-right corners,
  372. -- which we can get by composing (in the path sense) the bottom and
  373. -- right faces.
  374. goal : Path (transp (\i -> B) botLeft) (f.1 a)
  375. goal = trans rightFace (\i -> botFace (inot i))
  376. in goal i
  377. -- The terms univalence + univalenceBeta suffice to prove the "full"
  378. -- univalence axiom of Voevodsky, as can be seen in the paper
  379. --
  380. -- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.
  381. --
  382. -- Available freely here: https://arxiv.org/abs/1712.04890v3
  383. J : {A : Type} {x : A}
  384. (P : (y : A) -> Path x y -> Type)
  385. (d : P x (\i -> x))
  386. {y : A} (p : Path x y)
  387. -> P y p
  388. J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d
  389. -- Isomorphisms
  390. ---------------
  391. --
  392. -- Since isomorphisms are a much more convenient notion of equivalence
  393. -- than contractible fibers, it's natural to ask why the CCHM paper, and
  394. -- this implementation following that, decided on the latter for our
  395. -- definition of equivalence.
  396. isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type
  397. isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x)
  398. -- The reason is that the family of types IsIso is not a proposition!
  399. -- This means that there can be more than one way for a function to be
  400. -- an equivalence. This is Lemma 4.1.1 of the HoTT book.
  401. Iso : Type -> Type -> Type
  402. Iso A B = (f : A -> B) * isIso f
  403. -- Nevertheless, we can prove that any function with an isomorphism
  404. -- structure has contractible fibers, using a cubical argument adapted
  405. -- from CCHM's implementation of cubical type theory:
  406. --
  407. -- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55
  408. IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B
  409. IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
  410. f = iso.1
  411. g = iso.2.1
  412. s = iso.2.2.1
  413. t = iso.2.2.2
  414. lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path (f x0) y) (p1 : Path (f x1) y)
  415. -> PathP (\i -> fiber f y) (x0, p0) (x1, p1)
  416. lemIso y x0 x1 p0 p1 =
  417. let
  418. rem0 : Path x0 (g y)
  419. rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))
  420. rem1 : Path x1 (g y)
  421. rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))
  422. p : Path x0 x1
  423. p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
  424. fill0 : I -> I -> A
  425. fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k)
  426. , (i = i1) -> g y
  427. , (j = i0) -> g (p0 i)
  428. ])
  429. (inS (g (p0 i)))
  430. fill1 : I -> I -> A
  431. fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k)
  432. , (i = i1) -> g y
  433. , (j = i0) -> g (p1 i) ])
  434. (inS (g (p1 i)))
  435. fill2 : I -> I -> A
  436. fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k))
  437. , (i = i1) -> rem1 (ior j (inot k))
  438. , (j = i1) -> g y ])
  439. (inS (g y))
  440. sq : I -> I -> A
  441. sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k)
  442. , (i = i1) -> fill1 j (inot k)
  443. , (j = i1) -> g y
  444. , (j = i0) -> t (p i) (inot k) ])
  445. (inS (fill2 i j))
  446. sq1 : I -> I -> B
  447. sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k
  448. , (i = i1) -> s (p1 j) k
  449. , (j = i0) -> s (f (p i)) k
  450. , (j = i1) -> s y k
  451. ])
  452. (inS (f (sq i j)))
  453. in \i -> (p i, \j -> sq1 i j)
  454. fCenter : (y : B) -> fiber f y
  455. fCenter y = (g y, s y)
  456. fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w
  457. fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
  458. -- We can prove that any involutive function is an isomorphism, since
  459. -- such a function is its own inverse.
  460. involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f
  461. involToIso {A} f inv = (f, inv, inv)
  462. -- An example of univalence
  463. ---------------------------
  464. --
  465. -- The classic example of univalence is the equivalence
  466. -- not : Bool \simeq Bool.
  467. --
  468. -- We define it here.
  469. data Bool : Type where
  470. true : Bool
  471. false : Bool
  472. not : Bool -> Bool
  473. not = \case
  474. true -> false
  475. false -> true
  476. elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b
  477. elimBool P x y = \case
  478. true -> x
  479. false -> y
  480. if : {A : Type} -> A -> A -> Bool -> A
  481. if x y = \case
  482. true -> x
  483. false -> y
  484. -- By pattern matching it suffices to prove (not (not true)) ≡ true and
  485. -- not (not false) ≡ false. Since not (not true) computes to true (resp.
  486. -- false), both proofs go through by refl.
  487. notInvol : (x : Bool) -> Path (not (not x)) x
  488. notInvol = elimBool (\b -> Path (not (not b)) b) refl refl
  489. notp : Path Bool Bool
  490. notp = univalence (IsoToEquiv (not, involToIso not notInvol))
  491. -- This path actually serves to prove a simple lemma about the universes
  492. -- of HoTT, namely, that any univalent universe is not a 0-type. If we
  493. -- had HITs, we could prove that this fact holds for any n, but for now,
  494. -- proving it's not an h-set is the furthest we can go.
  495. -- First we define what it means for something to be false. In type theory,
  496. -- we take ¬P = P → ⊥, where the bottom type is the only type satisfying
  497. -- the elimination principle
  498. --
  499. -- elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b
  500. --
  501. -- This follows from setting bottom := ∀ A, A.
  502. data bottom : Type where {}
  503. elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b
  504. elimBottom P = \case {}
  505. absurd : {P : Type} -> bottom -> P
  506. absurd = \case {}
  507. -- We prove that true != false by transporting along the path
  508. --
  509. -- \i -> if (Bool -> Bool) A (p i)
  510. -- (Bool -> Bool) ------------------------------------ A
  511. --
  512. -- To verify that this has the correct endpoints, check out the endpoints
  513. -- for p:
  514. --
  515. -- true ------------------------------------ false
  516. --
  517. -- and evaluate the if at either end.
  518. trueNotFalse : Path true false -> bottom
  519. trueNotFalse p = transp (\i -> if (Bool -> Bool) bottom (p i)) id
  520. -- To be an h-Set is to have no "higher path information". Alternatively,
  521. --
  522. -- isHSet A = (x : A) (y : A) -> isHProp (Path x y)
  523. --
  524. isHSet : Type -> Type
  525. isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
  526. -- We can prove *a* contradiction (note: this is a direct proof!) by adversarially
  527. -- choosing two paths p, q that we know are not equal. Since "equal" paths have
  528. -- equal behaviour when transporting, we can choose two paths p, q and a point x
  529. -- such that transporting x along p gives a different result from x along q.
  530. --
  531. -- Since transp notp = not but transp refl = id, that's what we go with. The choice
  532. -- of false as the point x is just from the endpoints of trueNotFalse.
  533. universeNotSet : isHSet Type -> bottom
  534. universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)
  535. -- Funext is an inverse of happly
  536. ---------------------------------
  537. --
  538. -- Above we proved function extensionality, namely, that functions
  539. -- pointwise equal everywhere are themselves equal.
  540. -- However, this formulation of the axiom is known as "weak" function
  541. -- extensionality. The strong version is as follows:
  542. Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type
  543. Hom {A} f g = (x : A) -> Path (f x) (g x)
  544. happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
  545. -> (p : Path f g) -> Hom f g
  546. happly p x i = p i x
  547. -- Strong function extensionality: happly is an equivalence.
  548. happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
  549. -> isIso {Path f g} {Hom f g} happly
  550. happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl)
  551. pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
  552. -> Path (Path f g) (Hom f g)
  553. pathIsHom {A} {B} {f} {g} =
  554. let
  555. theIso : Iso (Path f g) (Hom f g)
  556. theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
  557. in univalence (IsoToEquiv theIso)
  558. -- Inductive types
  559. -------------------
  560. --
  561. -- An inductive type is a type freely generated by a finite set of
  562. -- constructors. For instance, the type of natural numbers is generated
  563. -- by the constructors for "zero" and "successor".
  564. data Nat : Type where
  565. zero : Nat
  566. succ : Nat -> Nat
  567. -- Pattern matching allows us to prove that these initial types are
  568. -- initial algebras for their corresponding functors.
  569. Nat_elim : (P : Nat -> Type) -> P zero -> ((x : Nat) -> P x -> P (succ x)) -> (x : Nat) -> P x
  570. Nat_elim P pz ps = \case
  571. zero -> pz
  572. succ x -> ps x (Nat_elim P pz ps x)
  573. -- The type of integers can be defined as A + B, where "pos n" means +n
  574. -- and "neg n" means -(n + 1).
  575. data Int : Type where
  576. pos : Nat -> Int
  577. neg : Nat -> Int
  578. -- On this representation we can define the successor and predecessor
  579. -- functions by (nested) induction.
  580. sucZ : Int -> Int
  581. sucZ = \case
  582. pos n -> pos (succ n)
  583. neg n ->
  584. let suc_neg : Nat -> Int
  585. suc_neg = \case
  586. zero -> pos zero
  587. succ n -> neg n
  588. in suc_neg n
  589. predZ : Int -> Int
  590. predZ = \case
  591. pos n ->
  592. let pred_pos : Nat -> Int
  593. pred_pos = \case
  594. zero -> neg zero
  595. succ n -> pos n
  596. in pred_pos n
  597. neg n -> neg (succ n)
  598. -- And prove that the successor function is an isomorphism, and thus, an
  599. -- equivalence.
  600. sucEquiv : isIso sucZ
  601. sucEquiv =
  602. let
  603. sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
  604. sucPredZ = \case
  605. pos n ->
  606. let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
  607. k = \case
  608. zero -> refl
  609. succ n -> refl
  610. in k n
  611. neg n -> refl
  612. predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
  613. predSucZ = \case
  614. pos n -> refl
  615. neg n ->
  616. let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
  617. k = \case
  618. zero -> refl
  619. succ n -> refl
  620. in k n
  621. in (predZ, sucPredZ, predSucZ)
  622. -- Univalence gives us a path between integers such that transp intPath
  623. -- x = suc x, transp (sym intPath) x = pred x
  624. intPath : Path Int Int
  625. intPath = univalence (IsoToEquiv (sucZ, sucEquiv))
  626. -- Higher inductive types
  627. -------------------------
  628. --
  629. -- While inductive types let us generate discrete spaces like the
  630. -- naturals or integers, they do not support defining higher-dimensional
  631. -- structures given by spaces with points and paths.
  632. -- A very simple higher inductive type is the interval, given by
  633. data Interval : Type where
  634. ii0 : Interval
  635. ii1 : Interval
  636. seg i : Interval [ (i = i0) -> ii0, (i = i1) -> ii1 ]
  637. -- This expresses that we have two points ii0 and ii1 and a path (\i ->
  638. -- seg i) with endpoints ii0 and ii1.
  639. -- With this type we can reproduce the proof of Lemma 6.3.2 from the
  640. -- HoTT book:
  641. iFunext : {A : Type} {B : A -> Type} (f : (x : A) -> B x) (g : (x : A) -> B x)
  642. -> ((x : A) -> Path (f x) (g x)) -> Path f g
  643. iFunext f g p i = h' (seg i) where
  644. h : (x : A) -> Interval -> B x
  645. h x = \case
  646. ii0 -> f x
  647. ii1 -> g x
  648. seg i -> p x i
  649. h' : Interval -> (x : A) -> B x
  650. h' i x = h x i
  651. -- Of course, Cubical Type Theory also has an interval (pre)type, but
  652. -- that, unlike the Interval here, is not Kan: it has no composition
  653. -- structure.
  654. -- Another simple higher-inductive type is the circle, with a point and
  655. -- a non-trivial loop, (\i -> loop i).
  656. data S1 : Type where
  657. base : S1
  658. loop i : S1 [ (i = i1) -> base, (i = i0) -> base ]
  659. -- By writing a function from the circle to the universe of types Type,
  660. -- we can calculate winding numbers along the circle.
  661. helix : S1 -> Type
  662. helix = \case
  663. base -> Int
  664. loop i -> intPath i
  665. loopP : Path base base
  666. loopP i = loop i
  667. winding : Path base base -> Int
  668. winding p = transp (\i -> helix (p i)) (pos zero)
  669. -- For instance, going around the loop once has a winding number of +1,
  670. windingLoop : Path (winding (\i -> loop i)) (pos (succ zero))
  671. windingLoop = refl
  672. -- Going backwards has a winding number of -1 (remember the
  673. -- representation of integers),
  674. windingSymLoop : Path (winding (\i -> loop (inot i))) (neg zero)
  675. windingSymLoop = refl
  676. -- And going around the trivial loop (\i -> base) goes around the the
  677. -- non-trivial loop (\i -> loop) zero times.
  678. windingBase : Path (winding (\i -> base)) (pos zero)
  679. windingBase = refl
  680. goAround : Int -> Path base base
  681. goAround =
  682. \case
  683. pos n -> goAround_nat n
  684. neg n -> sym (goAround_nat (succ n))
  685. where
  686. goAround_nat : Nat -> Path base base
  687. goAround_nat = \case
  688. zero -> refl
  689. succ n -> trans (\i -> loop i) (goAround_nat n)
  690. -- One particularly general higher inductive type is the homotopy pushout,
  691. -- which can be seen as a kind of sum B + C with the extra condition that
  692. -- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.
  693. data Pushout {A : Type} {B : Type} {C : Type} (f : A -> B) (g : A -> C) : Type where
  694. inl : (x : B) -> Pushout f g
  695. inr : (y : C) -> Pushout f g
  696. push i : (a : A) -> Pushout f g [ (i = i0) -> inl (f a), (i = i1) -> inr (g a) ]
  697. -- The name is due to the category-theoretical notion of pushout.
  698. -- TODO: finish writing this tomorrow lol
  699. data Susp (A : Type) : Type where
  700. north : Susp A
  701. south : Susp A
  702. merid i : A -> Susp A [ (i = i0) -> north, (i = i1) -> south ]
  703. data Unit : Type where
  704. tt : Unit
  705. poSusp : Type -> Type
  706. poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)
  707. poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A
  708. poSusp_to_Susp = \case
  709. inl x -> north
  710. inr x -> south
  711. push x i -> merid x i
  712. Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A
  713. Susp_to_poSusp = \case
  714. north -> inl tt
  715. south -> inr tt
  716. merid x i -> push x i
  717. Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x
  718. Susp_to_poSusp_to_Susp = \case
  719. north -> refl
  720. south -> refl
  721. merid x i -> refl
  722. unitEta : (x : Unit) -> Path x tt
  723. unitEta = \case tt -> refl
  724. unitContr : isContr Unit
  725. unitContr = (tt, \x -> sym (unitEta x))
  726. poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
  727. poSusp_to_Susp_to_poSusp {A} = \case
  728. inl x -> cong inl (sym (unitEta x))
  729. inr x -> cong inr (sym (unitEta x))
  730. push x i -> refl
  731. Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)
  732. Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
  733. data T2 : Type where
  734. baseT : T2
  735. pathOne i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
  736. pathTwo i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
  737. square i j : T2 [
  738. (j = i0) -> pathTwo i,
  739. (j = i1) -> pathTwo i,
  740. (i = i0) -> pathOne j,
  741. (i = i1) -> pathOne j
  742. ]
  743. torusToCircs : T2 -> S1 * S1
  744. torusToCircs = \case
  745. baseT -> (base, base)
  746. pathOne i -> (loop i, base)
  747. pathTwo i -> (base, loop i)
  748. square i j -> (loop i, loop j)
  749. circsToTorus : (S1 * S1) -> T2
  750. circsToTorus pair = go pair.1 pair.2
  751. where
  752. baseCase : S1 -> T2
  753. baseCase = \case
  754. base -> baseT
  755. loop j -> pathTwo j
  756. loopCase : Path baseCase baseCase
  757. loopCase i = \case
  758. base -> pathOne i
  759. loop j -> square i j
  760. go : S1 -> S1 -> T2
  761. go = \case
  762. base -> baseCase
  763. loop i -> loopCase i
  764. torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
  765. torusToCircsToTorus = \case
  766. baseT -> refl
  767. pathOne i -> refl
  768. pathTwo i -> refl
  769. square i j -> refl
  770. circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
  771. circsToTorusToCircs pair = go pair.1 pair.2
  772. where
  773. baseCase : (y : S1) -> Path (torusToCircs (circsToTorus (base, y))) (base, y)
  774. baseCase = \case
  775. base -> refl
  776. loop j -> refl
  777. loopCase : (i : I) (y : S1) -> Path (torusToCircs (circsToTorus (loop i, y))) (loop i, y )
  778. loopCase i = \case
  779. base -> refl
  780. loop j -> refl
  781. go : (x : S1) (y : S1) -> Path (torusToCircs (circsToTorus (x, y))) (x, y)
  782. go = \case
  783. base -> baseCase
  784. loop i -> loopCase i
  785. TorusIsTwoCircles : Path T2 (S1 * S1)
  786. TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
  787. theIso : Iso T2 (S1 * S1)
  788. theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)
  789. abs : Int -> Nat
  790. abs = \case
  791. pos n -> n
  792. neg n -> succ n
  793. sign : Int -> Bool
  794. sign = \case
  795. pos n -> true
  796. neg n -> false
  797. boolAnd : Bool -> Bool -> Bool
  798. boolAnd = \case
  799. true -> \case
  800. true -> true
  801. false -> false
  802. false -> \case
  803. true -> false
  804. false -> false
  805. plusNat : Nat -> Nat -> Nat
  806. plusNat = \case
  807. zero -> \x -> x
  808. succ n -> \x -> succ (plusNat n x)
  809. plusZero : (x : Nat) -> Path (plusNat zero x) x
  810. plusZero = \case
  811. zero -> refl
  812. succ n -> \i -> succ (plusZero n i)
  813. multNat : Nat -> Nat -> Nat
  814. multNat = \case
  815. zero -> \x -> zero
  816. succ n -> \x -> plusNat x (multNat n x)
  817. multInt : Int -> Int -> Int
  818. multInt x y = signify (multNat (abs x) (abs y)) (boolAnd (sign x) (sign y)) where
  819. signify : Nat -> Bool -> Int
  820. signify = \case
  821. zero -> \x -> pos zero
  822. succ n -> \case
  823. true -> pos (succ n)
  824. false -> neg n
  825. two : Int
  826. two = pos (succ (succ zero))
  827. four : Int
  828. four = multInt two two
  829. sixteen : Int
  830. sixteen = multInt four four
  831. isProp : Type -> Type
  832. isProp A = (x : A) (y : A) -> Path x y
  833. data Sq (A : Type) : Type where
  834. inc : A -> Sq A
  835. sq i : (x : A) (y : A) -> Sq A [ (i = i0) -> inc x, (i = i1) -> inc y ]
  836. Sq_rec : {A : Type} {B : Type}
  837. -> isProp B
  838. -> (f : A -> B)
  839. -> Sq A -> B
  840. Sq_rec prop f = \case
  841. inc x -> f x
  842. sq x y i -> prop (f x) (f y) i
  843. hitTranspExample : Path (inc false) (inc true)
  844. hitTranspExample i = transp (\i -> Sq (notp i)) (sq true false i)