8d5f607122c9db68f7d1c63979bbee0b5528d840595b8f9fde1d9ac2e746b1c5  README.md
db2e2813b0cc3156d7d9760e54409124a28a5d420620d3d7f450329482bab7ba  check-hott.sh
f88e63a7c7c2c453a14769f636dd40df945a97ecf7a89866bc81b587fa8c2208  editorial-summary.md
02e7e026b5246b472fbc9d3e79e75f9a221d76be36da6a521689adcec7c5fe95  examples/check_lean.py
a386bdcd8b366fa7cf249ed13a380c4bd41fadc76049ceeb8e04be01f1e3f688  examples/finite_cases.py
9acbc8c85d89247796c4b9fed1ca95f5d5aa5d5c1cbde5c357d1b9dacbd7bd0d  examples/higher_cases.py
df553ff40bd0f7ad4f7981774b31be94f05585ca148c2c3656d0736859ffc4ca  examples/listings.py
5aee872478dde6e64e728c2f6685f8efdd5719292399577061f390486a161bbc  examples/predicate_cases.py
5968496c171988bac3c3faab1c592ab431055e74ee3bf8be449c4e63ae13165f  examples/render.py
f551539efed4f71cd33151ccd2a0f98de2b8764de471cb7cdb3c1fe244baade1  examples/stress_cases.py
6635796cf7370aeb34d5d58b5efe8b994279221f5bd5bb72fa85902cd07dc504  hott/FiniteLift.hlean
47efe1e5ba76e2b243a9e9de7de469074c7ec866ebb082bbbef1d0560ccd2de0  hott/Logic.hlean
76ebca27dc9f5a1e613f7de2f0284b8ce6e038ddf402f9bc6e822056d487f403  hott/Residual.hlean
10700fda1137d1e7634106dcdc9fbe8cd26c7e08a855f385209fb05f00f441b4  lean/Audit.lean
302c1c50ea330f71e8e14d7f435cf68e65acfce0062933dd7033e3c1f03b351f  lean/Cegar/Core.lean
5bcab2b2608942491f485dcf0132725fd4fa84d977787eaca568ae92e509cb7e  lean/Cegar/Layered.lean
f02b2bd741e304f0cacab598d8113026fa0fdd646b78686247fb916fc120901c  lean/Cegar/Logic.lean
8d55641aca9d970fe4e6baadc71dddb535917bf428a1d07adb29750db137ac03  lean/Cegar/Refinement.lean
42a08cef4387b3841e423a633c48966ff6b5c4dc3461813fc91f9e61f0b8355a  lean/Cegar.lean
1ca7fa19d82f2bcbe85ae257ff766c4af81cb40cb6e84404a2e29744fc1272d2  lean/Main.lean
5655ebde2888f2d24b64802a5c9b7aeaee922de599ccbdd993d86aa60e4d67e6  lean/lake-manifest.json
4177a21547d4f7086a8a21e2966371397b07d3321b99ac6e226cfe8df3484cad  lean/lakefile.toml
55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea  lean/lean-toolchain
1843f8c19a07786bc68ab5d07addf5b0ce33d4eaa7f53807c47b6e3cc8e218ff  manuscript/generated/code/01.txt
c77f731e26d7d4b20c8d1696f5ae2e2aa3e359e271be06b281d121e5777a653e  manuscript/generated/code/02.txt
1dabfb65aa929d9b969b7a55a900ce1d2432f38fee660fd869ff07a6d8a29ffb  manuscript/generated/code/03.txt
a237f08dbdb7ae4eef51f469bc634d06dd23de198437fe808724215fa79982ea  manuscript/generated/code/04.txt
d291b2dc73753cbd9389d3b064a7522bcda327c673c197ca49784225fded9867  manuscript/generated/code/05.txt
10700fda1137d1e7634106dcdc9fbe8cd26c7e08a855f385209fb05f00f441b4  manuscript/generated/code/06.txt
f7e332c70d1473317499f38c02c907043c6eec6363cfd4747a136105bbd8efd2  manuscript/generated/code/07.txt
b763904b6531f52b6d0efd9ef7f98b57d8cf172475cf20fcc800264def3ce720  manuscript/generated/code/08.txt
7eff321a07ca7d7185d2f87d994087ce1a5c70375d65167881069646b52fe96a  manuscript/generated/code/09.txt
00df10659f9bdcad32439643ddcc165ec1c60885e3f0cc16e1fd3be5004d33ae  manuscript/generated/finite.json
453fbb30106053e654ff4d1f8a4182bd5e72135bcf97b51e2a8cf9ed9f0212b5  manuscript/generated/finite.tex
ec32847d35ce4484d3be87b84f86d77b44ff7fa74e43850e1bd0b6486a21ec1e  manuscript/generated/higher.json
1ac780822219bbdc0827e6b2d7ac464b270f155c2f24e346531dd714149a690c  manuscript/generated/higher.tex
d45a6d9844ac28b615d0fa95ac540073360e5e574b0f3a560943fcd87ddfeba8  manuscript/generated/listings.tex
2629482a517e551f006ad955226678e66cf50535399b4f24c2f91f86bff29012  manuscript/generated/predicates.json
3212978047824db562453eae2f2de0b4204e12c02980806d357fe001287d2e3d  manuscript/generated/predicates.tex
091ab17f9009e32cd412f81922cdc438ed5767faa8df9b22bf67a09d886cef8e  manuscript/main.tex
648271cff5e26f3a15446cd122932f1e797618a9e3bf0b9ece2c969397e03a89  manuscript/references.tex
24b8b5d45cc5d00eda3ffa85aa9ff203ddd7e957ba1e80598525359f43cbcc64  manuscript/sections/01-introduction.tex
5f7477359aa2ca85ddbe220915e9a5c1858ae4b99571b471207ac126fab51b17  manuscript/sections/02-classical.tex
1c7f3f2c5c669b1f5c65bac7288acce55d7e0a587861114ac5159b9151ef9f74  manuscript/sections/03-topos.tex
5b348eb1bce138c554f367465ad9f6bfcecd079342d00ece0af8c2491d2bfcfe  manuscript/sections/04-towers.tex
d709eda08deb53fa71196fcce625089492cd657d8d8d46890b9a96c01babbf69  manuscript/sections/05-descent.tex
96d0a34ff12018bc78ba7f9cb8d3a7a33ba4e9b3bfef57548867fc21701670a7  manuscript/sections/06-hott.tex
cb268f990ae6f905f916724d395344fc8bd966c02d29f81f5968f49d55f9f869  manuscript/sections/07-segal.tex
17715fcb1c9f0fe435a957abed08b712ce0f558efe1f949ace8503db85e0830f  manuscript/sections/08-refine.tex
017efc66048bd804297304c3ac8fcde98901ddbd31bc1d3382111d6f1ca2cb12  manuscript/sections/09-predicates.tex
5d5aff59573a7a2388875ff3a0888ac73591d0433d58fb16a51979c45aeb1cff  manuscript/sections/10-logic.tex
bd5b6a8efe09e6db4f530e11510e75ac0083ac9e2928cef7fbbf9fb8dbd01507  manuscript/sections/11-lean.tex
bbb0090603f2eaaf8b11c87bf585dd986867c6627e4d9f85c0556acbe20dffc9  manuscript/sections/12-general.tex
e189bb4b8a98fa42cd32016e0269fafc89a102497a69f3ef5fd4584eeb5da05e  manuscript/sections/13-algebra.tex
3eea5b55c823ff14fdbed792129b8cab3ebdc8b84dd313c9ed277efebd1b9aa7  manuscript/sections/13-patterns.tex
922aba567aa01f8358c86cda6b76cbb8df016d20c948fc467bca1ecd2d9935a3  manuscript/sections/13-study.tex
e3efbe12dfb0c983af7231c3d1d728dc381ae0006a7ec3efe2cd00551dae5cbd  manuscript/sections/14-repro.tex
8b28515ffffc5c0fe2807d8ae3735b00b324d9b7ce807dd63ff6ac8922fbce7e  runtime/lean-hott-linux-x86_64/LICENSE
ec094e3ab253cf87d12001315f764088634491c64df8ff29e7633341653a7698  runtime/lean-hott-linux-x86_64/UPSTREAM.txt
d724146144f366703825ee563c246f27b5bbc2b104ae62ec37abb369c77ca240  runtime/lean-hott-linux-x86_64/bin/lean
6fc2cb37ee151c659f882fd4b3a4dc44e87578c0aafc5da03e10cc20946962f2  runtime/lean-hott-linux-x86_64/hott/algebra/binary.olean
783335477cf495d848353eada8427b276860b9e11a74be07751a8d25d518a9a3  runtime/lean-hott-linux-x86_64/hott/algebra/bundled.olean
d292215800bf9dd4523d347d5a078c9b9f45c7bd597a9e06918e093744915367  runtime/lean-hott-linux-x86_64/hott/algebra/category/category.olean
58c99b7bc33d5636ddca4ccb199d691228f0f6fcff526b23c15f4aaa754108c7  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/comma.olean
91766d5bbaa16d5591541d10bf38ab2b5f4c58ec14e48420252770a9c0fadac0  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/cone.olean
ca43986a9176aabd2f7272abd4dce9a40009ad5ec2f6f5ef152c4f549b8a21d7  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/default.olean
bf364883754008e931f90696bbfe0f4dc0892dc64a362779f2b52584c552bbfc  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/discrete.olean
24429dba07abf888e5acf43a285e9dfebadd28aa9483da4c453eef8e5870ef4e  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/finite_cats.olean
61009e9a448f2613842a4c68a714d32dff9b3091c90d3caaa62d3ba3dc24ba31  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/functor.olean
5079feda81d4eb6473664bf0b73aa97919b83c03ae4425a6bdb1a3ae1d44d0cb  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/fundamental_groupoid.olean
869b177ece82d7c126737f4f3ca48aee060f745e5f2beb511038f5255e16b0e4  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/indiscrete.olean
b3ef6095d285aa7229e56210026e479cb07ac837bd162711d3da8c6d43fdbf90  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/initial.olean
12a87640e35d126c7d22e1b7beba490198267b9354676b1e0d768adedd1df566  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/opposite.olean
707f0341cf9d63e70a11e0e2a7c941c4901f3adb79f4f2251121c113b1dd2709  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/order.olean
6a9763a34a8f80112be5691252c8ea6e3e0f1caf812c38594704f9fd1716e5ff  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/product.olean
9d1c80bdbc76287cd706588e06d67be83d4cd6a9c752848cfab2f7d53b2448ea  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/pullback.olean
7db70ed15dc32ca9159a06a29018a38ae6c7875e6345c8b5dca20e21103515d8  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/pushout.olean
0fec7a0c942ca99f11375acbd7c0112bf755bd1e2b2a377871eec9c94575509d  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/rezk.olean
3f3409aaa2da79eaf5ccbb462111665b3576cff3e73c3863db1d09bdddbb8df5  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/set.olean
67a724bb38d769445abb892ceb26081b2ef9db948be5c86178c43c5f675438b3  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/sum.olean
9419ec51a7a3eaf94c73f7c07cb6ff66b0c0bf6a14c5a9f293f51f5050b3841f  runtime/lean-hott-linux-x86_64/hott/algebra/category/constructions/terminal.olean
fa71a748a4e0b5884e299b77bb99113cd6e74c661552de4096db7fde33cd9bb4  runtime/lean-hott-linux-x86_64/hott/algebra/category/default.olean
9e50933f8bb5bdbf3aee4e00aa64527ade96b44beca5f6d7a70a0ac9e32ab0a5  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/adjoint.olean
e738165f4c7d88bf44c0d96cfaa416caece9e252b749f6984c2181899b02c7b4  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/adjoint2.olean
df183e4800c08302f51cb20df1c8f22bc70cf9d5809337136e77e2429a885e89  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/attributes.olean
9dac0461caa77a2363f64e5b62745ef246e6ed1b40ee13558bf40b3709eca1ee  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/basic.olean
30fc32dca3f1851e84d3a2fe57059ab309b53f780a500e9bd08d2c5e1aa3dab1  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/default.olean
938c43f8f0917bf8681084a900800f84991dae84ab964a7d91709476a0ba547a  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/equivalence.olean
d844522c783aaad6c4fa81bfbfb4f842bb2bbff7772c6fe452ec702aff10ec9b  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/examples.olean
01a64e782e28c45da055f4653a21e88c868139d629982ba11430209b6ebbd023  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/exponential_laws.olean
1f52fbb7ccf4e620b7b12a4b9d86c2aab037a575e72a5ec1581db9a65a03c9bb  runtime/lean-hott-linux-x86_64/hott/algebra/category/functor/yoneda.olean
08575f02cabfa5bf53905d1b5c2fe9920b014e7ca80704675d94460b2b3b91f2  runtime/lean-hott-linux-x86_64/hott/algebra/category/groupoid.olean
a063551eb3a32f6f9e3b66785e0c0bf6df4a57ca0616cf73eba905fb03184071  runtime/lean-hott-linux-x86_64/hott/algebra/category/iso.olean
1db93887ad90b908964d5c0e4c583519bd62c5bbbe34c20b99548c1b7dca115f  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/adjoint.olean
5e911e6b4f0124d5ef24e738605ba7de6646537649314982df3d2fc2debad264  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/colimits.olean
09ca74779889e1e929856973ef37b9acfc048d03b60b242516020c7493fc5304  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/default.olean
643f584f355bda1f1264f859b3a93dba3ff83d067cd09b1549d3853e86c930f6  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/functor.olean
aa94e48376bdf23748ceb68e282af111b16956d5e0a8303be09bc5fc3df298cc  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/functor_preserve.olean
8d0fb85de659d917bb25c9630414172fdf671b07074c1e5ef337e930b159a46c  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/limits.olean
eced4420a388fcaaeb4de7aed6e7926e3897239bae6d45ee5f5f8ead23626873  runtime/lean-hott-linux-x86_64/hott/algebra/category/limits/set.olean
7dd294aec11f8eb550ad782a217ddbf766e620b7dd926d0127f82028acd29ff0  runtime/lean-hott-linux-x86_64/hott/algebra/category/nat_trans.olean
b0cc6c4b35898ad39c343d75f9132d2e473f6960b62b89e59c02659a85ada9ee  runtime/lean-hott-linux-x86_64/hott/algebra/category/precategory.olean
98be82f3e2ce44d079e002c8be113291c776118112834514d5fdf55b371f7b49  runtime/lean-hott-linux-x86_64/hott/algebra/category/strict.olean
75c40974958ef09128b6ec9ce478bfca28baa7046a7400be44572f8a002ceefe  runtime/lean-hott-linux-x86_64/hott/algebra/default.olean
80d233da15aa7dd54d04d3a01f6bfca0030187d9763b678223caea6e8442e241  runtime/lean-hott-linux-x86_64/hott/algebra/e_closure.olean
c87821d931a66375623bb7a5fb6ba70e6e46ccf6707e5fcb255024b5aaf67a21  runtime/lean-hott-linux-x86_64/hott/algebra/field.olean
2a4531fc7097cbf8548e67b074ae5bbdb467afe1b3992a14dd59a1b3932348a9  runtime/lean-hott-linux-x86_64/hott/algebra/graph.olean
cb276ad7f8e4fd0d50452a09977b928eb0af0115668edd7b1c64b146ebee084a  runtime/lean-hott-linux-x86_64/hott/algebra/group.olean
b8e5c84080bcc206f0475fe0d2d496b4f4805e53303cf5adfaac314470e3b045  runtime/lean-hott-linux-x86_64/hott/algebra/group_power.olean
e5ab9304ae41d6260641ea9f555039b438f99676448e73589f8436e80c09b8fe  runtime/lean-hott-linux-x86_64/hott/algebra/group_theory.olean
391140b4f06e9143cd318ebf46cd214d54978d90a1e61a4fb2b5bad9151377ec  runtime/lean-hott-linux-x86_64/hott/algebra/homomorphism.olean
a838846115a60e88a8ad6727214d9100873643db28e9c0a600ec2545a8ca20c6  runtime/lean-hott-linux-x86_64/hott/algebra/homotopy_group.olean
1dd4bf62affb201bccc3433c4e889091b217be5bcc7c0e463005a65387cc7800  runtime/lean-hott-linux-x86_64/hott/algebra/inf_group.olean
4e4f4a2e8240164ed48a8ceabdae7c0ed823d0b6d1b712474a3498def9d03261  runtime/lean-hott-linux-x86_64/hott/algebra/inf_group_theory.olean
09bb02bdf5bc1bc69d5b0a2462ad0127da8d6702284f6ea235b90dfa27b81a56  runtime/lean-hott-linux-x86_64/hott/algebra/lattice.olean
91ab3dc209202b32d9a0477e0be8c983d5d59ab97894fd16cff71bdf679d6bd6  runtime/lean-hott-linux-x86_64/hott/algebra/order.olean
28387c61556910b30a355d8d3c8c05c88e7954bc11c5c4adb262d3cad1f85ac4  runtime/lean-hott-linux-x86_64/hott/algebra/ordered_field.olean
635531357819ca26e7fad917937471062eae0b527a2cf00cac499479d34c6927  runtime/lean-hott-linux-x86_64/hott/algebra/ordered_group.olean
6fea0e572ded4a19a86024df69bd4bcca4033866b3f12b080e91aaa6b0c920c1  runtime/lean-hott-linux-x86_64/hott/algebra/ordered_ring.olean
b3a656c8de27cac4dc92357b07d0a4ea862c84e128a9cb27e829e9e9acd59d43  runtime/lean-hott-linux-x86_64/hott/algebra/priority.olean
5e0eac299daaaec480e9426449d78997d729e0f675c905690faea30b6b79847a  runtime/lean-hott-linux-x86_64/hott/algebra/relation.olean
2f44ccf05105343ae7de56c3ac204bdc39925014ce5ac8d0b3f7b7904d22a69b  runtime/lean-hott-linux-x86_64/hott/algebra/ring.olean
824dc65e479aacb8943492167ea53aa94d89877a85f1519dd8e823a6b17ae46a  runtime/lean-hott-linux-x86_64/hott/algebra/trunc_group.olean
d758e1ff0ea679f83e0847e3460940b03a191bcb82fdb17ea43d5afa9a8901a9  runtime/lean-hott-linux-x86_64/hott/arity.olean
68afd8a75d1696fb0442b55c18cda876207f351cf9e2cb6148899356806076ca  runtime/lean-hott-linux-x86_64/hott/choice.olean
64e8871eeeb2ffc05e7a6409895cff5518ad6449d0e53a244cc70d268813e7c6  runtime/lean-hott-linux-x86_64/hott/core.olean
14507c1f77caa0c52759a26f5d13774a525a80769f259431e81adc012a2512d1  runtime/lean-hott-linux-x86_64/hott/cubical/cube.olean
33f5fbce32e555f98a62c26eff6f114375826fc526050ecf1064ce2875ff0b2a  runtime/lean-hott-linux-x86_64/hott/cubical/cubeover.olean
fff389761dee0f9cce37bae92c0e6bcaa72f618a7ef1b7269c9d7fb4958ab78d  runtime/lean-hott-linux-x86_64/hott/cubical/default.olean
0a3d863f91b36cb0d194aefc482e637082bf45ba53113c6eb25b08a1e05fd875  runtime/lean-hott-linux-x86_64/hott/cubical/pathover2.olean
8a87b8fde5bdaa72305016d57f06397a48ebf357c1237b558a9e97b365438a45  runtime/lean-hott-linux-x86_64/hott/cubical/square.olean
db05186467b7196808fcabef4b8ebc18fd4bd46e344a9ef09ab363915a4151a6  runtime/lean-hott-linux-x86_64/hott/cubical/squareover.olean
9fc4c7a8a376b72be2284568b7e1a91253e855cd864a5839966c5842101b66ba  runtime/lean-hott-linux-x86_64/hott/eq2.olean
d293f8480396678f32415a17ccbfaeb8b83ccbfadb52f6536fbb439f18248816  runtime/lean-hott-linux-x86_64/hott/function.olean
0c695b3e443deed1be3563bb5f7361021f6ad4a54d999bdbd3042bea0c96041b  runtime/lean-hott-linux-x86_64/hott/hit/coeq.olean
c4aa04200ef06cc7d88422150bc6389e64f1e67461460335dbd3fa4c8948acfc  runtime/lean-hott-linux-x86_64/hott/hit/colimit.olean
d7eb385ec40a2f31bcd4a5eab8233f7ba9a6a8f44b69a016e94e0c1a84111503  runtime/lean-hott-linux-x86_64/hott/hit/default.olean
b4dec69bc54a755027cc403a95875fae62fef31974b6a76e05aba7e9d8b593cd  runtime/lean-hott-linux-x86_64/hott/hit/groupoid_quotient.olean
04b52614ef9c0dfbca80a1881c6704cb363dcfbd33f00b66ad95a2611f6ce786  runtime/lean-hott-linux-x86_64/hott/hit/prop_trunc.olean
1663357524f72369422f8a90ab9d69afcd4577f6a10e427e626e426e5c4b7b1d  runtime/lean-hott-linux-x86_64/hott/hit/pushout.olean
df07fe94a6ca8c18f66561d98ac99fb1c8bc3dc422fe5eb7d60eb070fcb43482  runtime/lean-hott-linux-x86_64/hott/hit/quotient.olean
4c1c7dec0c92ee812db4906e480917119b81a9c434a55b831a1e281ffe2d9fd6  runtime/lean-hott-linux-x86_64/hott/hit/refl_quotient.olean
7359c0f234637134e5bf52ff82e860efd25543fc5b915f991b1f33299b3a7f0f  runtime/lean-hott-linux-x86_64/hott/hit/set_quotient.olean
fc788add346c9359e2e106c199e9dd4fc7eac7cc47ad58cc3d5fb918e90de37d  runtime/lean-hott-linux-x86_64/hott/hit/trunc.olean
8c202385c0705c53d0ba8e912ded763d53e557a4c38efedafb135bf58aa88bd4  runtime/lean-hott-linux-x86_64/hott/hit/two_quotient.olean
1b8c87e46cfcc48e73098142e5b58c8b26f32ee2fb42fa0d6fcf16aea1fe91ab  runtime/lean-hott-linux-x86_64/hott/homotopy/EM.olean
8e91adfa5a04a65ba96bf34714b06067eac7d4e19817d97e8310380933cbc517  runtime/lean-hott-linux-x86_64/hott/homotopy/LES_of_homotopy_groups.olean
bf8d18fbb80917d7f34afbb81e5993944f02c1462f5acdbd2819b4dc23b42b42  runtime/lean-hott-linux-x86_64/hott/homotopy/cellcomplex.olean
486f3214ad8b95c7a297279034aacbc2654ebf0eff2ac0a6a9827d553d7f463f  runtime/lean-hott-linux-x86_64/hott/homotopy/chain_complex.olean
d85065ba6a6b52763220b3185247a84e8ca514c29c198f4b853a145520ed0823  runtime/lean-hott-linux-x86_64/hott/homotopy/circle.olean
5d01aeae715dd598ef853a8bce8affce0f79340f2962cf92e14be068dea53b63  runtime/lean-hott-linux-x86_64/hott/homotopy/cofiber.olean
51d53890846d2e812fce004e21cb7c48c5b7226e0a23401b43503567f600813f  runtime/lean-hott-linux-x86_64/hott/homotopy/complex_hopf.olean
33f519d2713adf3158c44f83f6858237d7fce945c1ebaae3e054549c5be54677  runtime/lean-hott-linux-x86_64/hott/homotopy/connectedness.olean
4264257211788eef1bac3aea4fcbc12b771980649dc1d76159750c415f701c1f  runtime/lean-hott-linux-x86_64/hott/homotopy/cylinder.olean
74535c7dde00400f39b2b934ef9fb21583a5c18f1f4430aa22ce59fb64d18f82  runtime/lean-hott-linux-x86_64/hott/homotopy/default.olean
1dbfe9ac1ea34cf9e7895c4c7559cdaafaea2a9e2ae03bf00c8cdcde0ed7ab7f  runtime/lean-hott-linux-x86_64/hott/homotopy/freudenthal.olean
964e188eb6eea2d368940c43d7039a026dad0aa318cb0d3153487b74d4840737  runtime/lean-hott-linux-x86_64/hott/homotopy/homotopy_group.olean
86546fdbc978a43111960bc491f3ce61b70dbaa35f12a06eab130740d1a424ea  runtime/lean-hott-linux-x86_64/hott/homotopy/hopf.olean
b1641ec38c8900f020d02d44daae352e62a3e830015e2efd6c359f40f9116e5c  runtime/lean-hott-linux-x86_64/hott/homotopy/imaginaroid.olean
0c55d6b63bf1b1911a5cd649fe5d1f465461790cbefe79a998606e6a11e6251b  runtime/lean-hott-linux-x86_64/hott/homotopy/interval.olean
760bb327d95faa8f7b8197388dfdebe7d7dc613b3fe9c898adfaa9821efd0bd2  runtime/lean-hott-linux-x86_64/hott/homotopy/join.olean
2f646ac29881bfce332b39642cc5ef2eda95eade1480883690212cb028ff530a  runtime/lean-hott-linux-x86_64/hott/homotopy/quaternionic_hopf.olean
e5e1705a0f1881191373e37cdbbc235ace773b87dc6815afaa4dcadc5dde5eba  runtime/lean-hott-linux-x86_64/hott/homotopy/red_susp.olean
80cc1788d7bd02307c2fdf1369339191a2691de6a4d52308e7b9a762ace8456e  runtime/lean-hott-linux-x86_64/hott/homotopy/smash.olean
e174d334f1327fcfb3f55b0f77911ba6eb24eb95be18cba61c48b8623a75c8d2  runtime/lean-hott-linux-x86_64/hott/homotopy/sphere.olean
9b62933851a5b76c8cbb67797b6ce0a32cbd3ee1de2071f730b238e7404eb499  runtime/lean-hott-linux-x86_64/hott/homotopy/sphere2.olean
6b279dccf8d2ec23d1da32f2f6b96146fc37e7e27ec702a0f10af9769d325b29  runtime/lean-hott-linux-x86_64/hott/homotopy/susp.olean
fac6a7646b917717df8541d3acc4bc3550113b8a537300a286020279bd53ce45  runtime/lean-hott-linux-x86_64/hott/homotopy/torus.olean
3b0d27720bad5eab49e5fcd7acc7fd37b7c28a8136ad2978ea9865573d4fb2bc  runtime/lean-hott-linux-x86_64/hott/homotopy/vankampen.olean
018802581e34cb75953f1511d5541e793dceb77b983bf807bbff0dd87f2f1d98  runtime/lean-hott-linux-x86_64/hott/homotopy/wedge.olean
70e3b39a826a4ab5922cc0577b1423eadc7fc486cbc477154a442e15dba75c85  runtime/lean-hott-linux-x86_64/hott/init/bool.olean
f45a865bbb60efb68dc009d3a375f12054bbd660f1ff9266d02d4360244636c6  runtime/lean-hott-linux-x86_64/hott/init/connectives.olean
312218f9f9ceb5dfcfffaaf65ee8c420a5cf86c373003132588886c69f62b768  runtime/lean-hott-linux-x86_64/hott/init/datatypes.olean
26d70483253807d6096a92633f65c7ee8da7f99dcb72a08371e44d53a5ef3744  runtime/lean-hott-linux-x86_64/hott/init/default.olean
84624e5ba4525cad74141656c3f3051c211e646bc2369d55c168a690307654b4  runtime/lean-hott-linux-x86_64/hott/init/equiv.olean
d756ce26eb063e26eaa287ee394617303c333e05a7089bf8b7c62350276f1754  runtime/lean-hott-linux-x86_64/hott/init/function.olean
04189ed7cf4b0acd3b5fa913913f8265324beb550fd84a02af6f28ace4eab436  runtime/lean-hott-linux-x86_64/hott/init/funext.olean
ed93d787b2921a60f0d8bb3caee0457583ada2006c07068471e1fea0d7cea031  runtime/lean-hott-linux-x86_64/hott/init/hedberg.olean
dd0d7abce9b693616669a93ffc11f8217e18832f17db112922e0f7eb9b337d68  runtime/lean-hott-linux-x86_64/hott/init/hit.olean
750dcfe791f5517debd6ca9c67876a16b55e5e7e01afe361d6eacc1c3dc468a3  runtime/lean-hott-linux-x86_64/hott/init/logic.olean
ebb7e899e457acc852e838d18fdd602be39f2b3f492a1d3b28b384a45ae74bdf  runtime/lean-hott-linux-x86_64/hott/init/nat.olean
16b4b2025becd2162effafd5b9b653b783b9990bd5cb80bdff394df8f9a63bf4  runtime/lean-hott-linux-x86_64/hott/init/num.olean
326c35d1636b62c30f20fc23a8d847bde8b30b4e6dac1bfe819bb49ba929cb7c  runtime/lean-hott-linux-x86_64/hott/init/path.olean
2e982825acb76bd00c5b7b31bb3b563298dc923dd827736daecefe004f030081  runtime/lean-hott-linux-x86_64/hott/init/pathover.olean
1fcb194fbe876cd80e69ded1f7f8e82b6c05357368200d9e2f33a4590d176693  runtime/lean-hott-linux-x86_64/hott/init/pointed.olean
9de5821c230d2f09c05570ce297fb711b70b0ff0de1b49367072a7f832f36e23  runtime/lean-hott-linux-x86_64/hott/init/relation.olean
d8c91b595e83c9dcbcb4052267337343f5bd42f4f7916d0ab22ff6c463f32269  runtime/lean-hott-linux-x86_64/hott/init/reserved_notation.olean
4f603f633dfdf20f5f865ea9c964bba076dbb3d1b61083f4fab37ad43d665df7  runtime/lean-hott-linux-x86_64/hott/init/tactic.olean
cf2128eea74ad00e45b0235b20ba97cb424066481c6e0c0c5879cce78e1c4e52  runtime/lean-hott-linux-x86_64/hott/init/trunc.olean
ce2942b9fe7194b56a56cfe48c4c316685cc7a4af3039617d58f60cdb5161e33  runtime/lean-hott-linux-x86_64/hott/init/types.olean
f4d78e426900b2124f0bf4458a88110e95107fe710304e33d67d95a65e48210a  runtime/lean-hott-linux-x86_64/hott/init/ua.olean
74430adebf367cdcc5503dbb10c0b162314e5cfdc31d066a819eae9207ab6524  runtime/lean-hott-linux-x86_64/hott/init/util.olean
d38ea211f6294f92fa995967afc91d5e12e17524a52b7faaab80fdccb6bf0fff  runtime/lean-hott-linux-x86_64/hott/init/wf.olean
99089e00797e8b2fc29663f317340214acc09feeabeab1a7034bb64e4b6e7b44  runtime/lean-hott-linux-x86_64/hott/logic.olean
c906dece40ee278991d2cc2bfe1f535d7d56f2a8a3923ec25833b1796aba2683  runtime/lean-hott-linux-x86_64/hott/prop_trunc.olean
e463e7aa63401ef5d198282a76e35d0dcb62a9006433ccd315d0b960bd0bde45  runtime/lean-hott-linux-x86_64/hott/tools/helper_tactics.olean
3d54aed3ea3b7b4c8dde68ed5226d04c68c0892a8ca13af3834eeb99e6de1965  runtime/lean-hott-linux-x86_64/hott/types/W.olean
09dde44ac8aa396cee49a3012070f6c1daaa90d946072e2b3d68b83d10354c69  runtime/lean-hott-linux-x86_64/hott/types/arrow.olean
decdccaf78809c2ed1395b78cc796ee59008b25d51c15b56c45679cba2fe86db  runtime/lean-hott-linux-x86_64/hott/types/arrow_2.olean
dde6a21f8da680b984ac4866a9d20777672d3a60478a158924fbcdaaa9fa1399  runtime/lean-hott-linux-x86_64/hott/types/bool.olean
49738f8405a49818034dcbe8b5307a656332fc79e1b32b9afd262cc9c8e04612  runtime/lean-hott-linux-x86_64/hott/types/default.olean
7828ce6428580198ece4d4a2302382b13b32094c24ba25eac688644d3f484c75  runtime/lean-hott-linux-x86_64/hott/types/eq.olean
4654cb98843b4c4680181228f3f0ab255b763edee8eb3dcc85b6ee5f481fb66c  runtime/lean-hott-linux-x86_64/hott/types/equiv.olean
15df9b2ca6168a7120d78b0924e0c382856342741a55dfc65645afdf350dac8f  runtime/lean-hott-linux-x86_64/hott/types/fiber.olean
2e1295a37b7c842681d20285d9f039d3c301468b8873127f60a7488a24ed8b95  runtime/lean-hott-linux-x86_64/hott/types/fin.olean
215b7516078d9473fd6353cd4bdc3d236762815637f29b8bc9b5fd25d30eb067  runtime/lean-hott-linux-x86_64/hott/types/int/basic.olean
61bfc8f64138bf34b12a233fe43efd28d34ea41facb145514d7b513202985519  runtime/lean-hott-linux-x86_64/hott/types/int/default.olean
336fcd02287401fc9bf1d28f5228ab9a297f513e7e59d03039b8f0a954cba440  runtime/lean-hott-linux-x86_64/hott/types/int/hott.olean
cdd27342cc46df9dd7f8b1dd6d302357df64854b39b9583a4cc5d547e73ef6c6  runtime/lean-hott-linux-x86_64/hott/types/int/order.olean
b6216e5c45f266db2e63f40ebfc72b0eef4ba9f27e4a2ac28d3ab4297f85179e  runtime/lean-hott-linux-x86_64/hott/types/lift.olean
a64ec19162818034c54586f8d723c6a02720ee147ceb365e5ce52d03898aedca  runtime/lean-hott-linux-x86_64/hott/types/list.olean
32eaac171eb2c7ed556d471bb386c9eba505d7f46ca931c35fdfa87c59080eaf  runtime/lean-hott-linux-x86_64/hott/types/nat/basic.olean
5db434543ee286a1f55e4939bc6e274d7eecc9c0dd73447b379669f548bccf4d  runtime/lean-hott-linux-x86_64/hott/types/nat/default.olean
273158fed3ba067e4f211a94b650137a6e9a0c298525962b977d6e5e9f81eb6e  runtime/lean-hott-linux-x86_64/hott/types/nat/div.olean
8cf2c2e6dede9d6271dbb5bc53fcc423aac5e05a5351678fd91738dc2653c997  runtime/lean-hott-linux-x86_64/hott/types/nat/hott.olean
8ae2aa29db6cb217f65b6b2b8f62d12625addcceab5e1b93a1cdcfcba64c8d2e  runtime/lean-hott-linux-x86_64/hott/types/nat/order.olean
a4243e6b6a4b3044d55ebc488249ddee588204ce67d0c9429de9dd25cdb29339  runtime/lean-hott-linux-x86_64/hott/types/nat/sub.olean
db817532f1c6ce88c97c05e763d7409f4dac2e86cb0fb4a53877389ccb0289e2  runtime/lean-hott-linux-x86_64/hott/types/num.olean
0a2d9fc07f6fc790f2745b22d8c211088b4f66e17cd52b541031e12c93b7a05c  runtime/lean-hott-linux-x86_64/hott/types/pi.olean
b7c7bd01221c28e7bf60c222e74e7e22a47b45a2517c3f17cb9d8180eda8b341  runtime/lean-hott-linux-x86_64/hott/types/pointed.olean
8893aea0c571a6cbb5ebbdadf2d0fa63e58af1ba079abfaf1d185a0e41290327  runtime/lean-hott-linux-x86_64/hott/types/pointed2.olean
c49ab35bbc4aec43d716420f52790bcc8b6c46e5223c9fce2fe4dfdc32807eac  runtime/lean-hott-linux-x86_64/hott/types/prod.olean
d4132eda0d6d7e998644f1bb3b01db980bb967894de7042ea5fac113c629cef0  runtime/lean-hott-linux-x86_64/hott/types/pullback.olean
94d1ffe4a9da7a15bbfe50fe5bf1e107e3559f586d728c33de369a52f9c81792  runtime/lean-hott-linux-x86_64/hott/types/sigma.olean
b82732c7fcc3cb7e2c7040b0a54619861e829aa42ea174fc1c4e920460352e13  runtime/lean-hott-linux-x86_64/hott/types/sum.olean
747e29bb01d948bb551daaab1467ff9857dcd5b5f8f66680964bedf6248e993b  runtime/lean-hott-linux-x86_64/hott/types/trunc.olean
28ad028b0a5189bc2843ed13f0e0a0f052edd88363330d342bbeb326a191ba5b  runtime/lean-hott-linux-x86_64/hott/types/type_functor.olean
5646db6106b5d9b405725d5849d5e7e093f077e99526d832365117d125aab3dc  runtime/lean-hott-linux-x86_64/hott/types/unit.olean
4e600ae1c0f47f4204c488997dfa84e2d44fb1b1ca760a4d55f0b879bfa47ba0  runtime/lean-hott-linux-x86_64/hott/types/univ.olean
10fdfa090b5adf11cbb5784eafcbc8209bef6e117822149785f7147591801575  verification/finite-results.json
f17bda3b30da80e5f5f8ccfbb0b068adbbd9bb75f4f7efc7209a5ed07114b15a  verification/hott-check.txt
e390341b394ca74beb0c08cbfc4b200db7df6dcace9067b6b0f00dc6d4d4fefe  verification/lean4-axioms.txt
5362a246ce2545424db10a77de8fd4694f4cf8b0170dfd43fa727acf7f7f259b  verification/lean4-version.txt
81304abe60db6c992a4961ac615c4cba7eae29468b995cb34ac83bf1edd8174f  verification/pdf-check.txt
