-
Notifications
You must be signed in to change notification settings - Fork 0
/
bib.bib
101 lines (87 loc) · 4.88 KB
/
bib.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/
https://en.wikipedia.org/wiki/Formal_verification
https://en.wikipedia.org/wiki/Dialectica_interpretation
https://en.wikipedia.org/wiki/G%C3%B6del_numbering
http://gregorulm.com/godels-system-t-in-agda/
https://deniskyashif.com/g%C3%B6dels-system-t-in-typescript/
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
https://www.sciencedirect.com/science/article/pii/S0304397509008081
https://en.wikipedia.org/wiki/Dialectica_interpretation
https://gist.github.com/copumpkin/1286093
https://doisinkidney.com/posts/2018-12-14-primes-in-agda.html
https://www.sciencedirect.com/science/article/pii/S0304397509008081
https://github.com/ryanartecona/agda-pfpl/blob/master/src/SystemT.agda
https://github.com/MrChico/agda-stdlib
https://en.wikipedia.org/wiki/Construction_of_the_real_numbers
https://en.wikipedia.org/wiki/Field_(mathematics)
https://en.wikipedia.org/wiki/Real_number
https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers
http://www.cs.cornell.edu/courses/cs3110/2013fa/lectures/11/lecture11.pdf
https://arxiv.org/pdf/1610.05072.pdf
https://mroman42.github.io/ctlc/ctlc.pdf
https://math.stackexchange.com/questions/2073041/what-is-so-wrong-with-thinking-of-real-numbers-as-infinite-decimals
https://en.wikipedia.org/wiki/Morphism
https://en.wikipedia.org/wiki/Function_(mathematics)
https://en.wikipedia.org/wiki/Group_homomorphism
https://en.wikipedia.org/wiki/Function_(mathematics)
https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection
https://ncatlab.org/nlab/show/geometry+of+physics
https://ncatlab.org/schreiber/show/Modern+Physics+formalized+in+Modal+Homotopy+Type+Theory
https://ncatlab.org/schreiber/files/MPfiMHTT200618.pdf
https://arxiv.org/abs/1310.7930
https://en.wikipedia.org/wiki/Categorical_quantum_mechanics
https://math.berkeley.edu/~erabin/The%20Categorical%20Language%20of%20Physics.pdf
https://www.physicsforums.com/insights/higher-category-theory-physics/
https://ncatlab.org/nlab/show/higher+category+theory+and+physics
https://ncatlab.org/nlab/show/geometry+of+physics
https://golem.ph.utexas.edu/category/2013/10/the_hott_approach_to_physics.html
https://arxiv.org/abs/1011.3401
https://en.wikipedia.org/wiki/Supergeometry
https://mathoverflow.net/questions/172014/why-differential-forms-are-important
https://ncatlab.org/nlab/show/differential+form
https://en.wikipedia.org/wiki/Differential_form
https://en.wikipedia.org/wiki/%C3%89tale_morphism
http://www.cse.chalmers.se/research/group/logic/book/book.pdf
https://en.wikipedia.org/wiki/Agda_(programming_language)#Inductive_types
https://en.wiktionary.org/wiki/mixfix
https://ncatlab.org/nlab/show/finite+set
http://firsov.ee/finset/finset.pdf
https://en.wikipedia.org/wiki/Kan_extension
https://ncatlab.org/nlab/show/Kan+extension
http://www.math.jhu.edu/~eriehl/cathtpy.pdf
https://ncatlab.org/nlab/show/extranatural+transformation
https://golem.ph.utexas.edu/category/2014/01/ends.html
https://bartoszmilewski.com/2017/03/29/ends-and-coends/
https://mathoverflow.net/questions/78471/intuition-for-coends
https://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space
https://en.wikipedia.org/wiki/Eilenberg%E2%80%93MacLane_space
https://mathoverflow.net/questions/5518/dirty-proof-that-eilenberg-maclane-spaces-represent-cohomology
https://ncatlab.org/nlab/show/cohomology
https://stacks.math.columbia.edu/browse
https://stackoverflow.com/questions/33052086/what-is-a-singleton-type-exactly
https://stackoverflow.com/questions/30794282/how-to-compare-two-sets-in-agda
https://en.wikipedia.org/wiki/Polymorphism_(computer_science)
https://agda.readthedocs.io/en/latest/language/universe-levels.html
https://arxiv.org/abs/1107.1901
https://plfa.github.io/Decidable/
https://en.wikipedia.org/wiki/Total_order
https://ncatlab.org/nlab/show/synthetic+topology
https://www.cs.bham.ac.uk/~mhe/agda-new/index.html
https://gist.github.com/osense/06cf3c35dbd700da92ae90773e59af95
https://gist.github.com/copumpkin/5945905
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/
https://golem.ph.utexas.edu/category/2011/03/homotopy_type_theory_i.html
https://ncatlab.org/nlab/show/homotopy+type+theory
https://www.mathematik.uni-kl.de/~gathmann/class/alggeom-2019/alggeom-2019.pdf
http://math.stanford.edu/~vakil/216blog/FOAGnov1817public.pdf
https://www.researchgate.net/publication/2625594_Understanding_And_Using_Brouwer%27s_Continuity_Principle
https://www.cs.bham.ac.uk/~mhe/.talks/tlca2015/tlca2015.pdf
https://www.cs.bham.ac.uk/~mhe/talks/escardo-ihp2014.pdf
http://page.mi.fu-berlin.de/shagnik/notes/continuity.pdf
http://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf
https://www.math3ma.com/blog/what-is-category-theory-anyway
https://ncatlab.org/nlab/show/nerve
https://ncatlab.org/nlab/show/pasting+diagram
https://ncatlab.org/nlab/show/directed+graph#connections_to_category_theory
https://ncatlab.org/nlab/show/representable+functor
https://en.wikipedia.org/wiki/Representable_functor