fredefox
/
cat
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
496 Commits 1 Branch 10 Tags 6.6 MiB
Commit Graph

496 Commits

Author SHA1 Message Date
Frederik Hanghøj Iversen 432cc78821 Prove assoc and ident for funky category 2018-03-29 15:47:43 +02:00
Frederik Hanghøj Iversen ffedb83210 Initial objects are also propositional 2018-03-29 14:31:58 +02:00
Frederik Hanghøj Iversen 52ac9b4b78 Terminal objects are propositional 2018-03-29 14:26:47 +02:00
Frederik Hanghøj Iversen af25db7e31 Merge remote-tracking branch 'Saizan/dev' into dev 2018-03-29 13:36:09 +02:00
Frederik Hanghøj Iversen 2f6b129ed6 Move proposal to report, use xelatex 2018-03-29 13:32:48 +02:00
Frederik Hanghøj Iversen 8752b1435d Update report 2018-03-29 13:32:06 +02:00
Andrea Vezzosi 8ac6b97213 isProp (Product C A B) setup 2018-03-29 00:07:49 +02:00
Frederik Hanghøj Iversen facd1167e0 Fix unique existential 2018-03-27 14:18:13 +02:00
Frederik Hanghøj Iversen b7a80d0b86 Proof: Being an initial- terminal- object is a mere proposition 
Also tries to use this to prove that being a product is a mere
proposition
 2018-03-27 12:20:24 +02:00
Frederik Hanghøj Iversen 9898685491 Prove that the opposite category is a category 2018-03-26 14:11:15 +02:00
Frederik Hanghøj Iversen d3864dbae5 Move properties about natural transformations to that module 2018-03-23 15:20:26 +01:00
Frederik Hanghøj Iversen ef688202a2 Move identity functor laws to functor module... 
and make progress on univalence in the functor category
 2018-03-23 13:55:03 +01:00
Frederik Hanghøj Iversen a713d560d5 Preview target 2018-03-23 11:33:55 +01:00
Frederik Hanghøj Iversen 1dde3f8e74 Restructure latex-stuff 2018-03-23 11:22:17 +01:00
Frederik Hanghøj Iversen 8ff93e04ec Move proposal to doc/ 2018-03-23 11:13:52 +01:00
Frederik Hanghøj Iversen c8c61a8d03 Half-time report 2018-03-23 11:11:44 +01:00
Frederik Hanghøj Iversen 96fb1d3a3b Formatting 2018-03-23 10:08:28 +01:00
Frederik Hanghøj Iversen 73c3b35631 Merge branch 'dev' 2018-03-22 14:52:01 +01:00
Frederik Hanghøj Iversen 4ae898dfe0 Update backlog and changelog 2018-03-22 14:51:43 +01:00
Frederik Hanghøj Iversen ac01b786a7 Cleanup 2018-03-22 14:27:16 +01:00
Frederik Hanghøj Iversen ebcab2528e Prove second inverse law for from/to-isomorphism 2018-03-22 13:49:53 +01:00
Frederik Hanghøj Iversen 0246c1b5ab Readability 2018-03-22 12:25:12 +01:00
Frederik Hanghøj Iversen d816ba657b QED! Show that the category of homotopic sets are univalent. 2018-03-22 12:11:27 +01:00
Frederik Hanghøj Iversen 52ca0b6732 Merge remote-tracking branch 'Saizan/dev' into dev 2018-03-22 11:54:22 +01:00
Frederik Hanghøj Iversen d12122ce60 Add another approach for univalence in Set 2018-03-22 11:50:07 +01:00
Andrea Vezzosi 66ab7138a6 generalized lem3 and made progress for Sets univalence 2018-03-22 10:41:38 +00:00
Frederik Hanghøj Iversen 807a0f3dcd Slight readability improvement 2018-03-21 18:05:25 +01:00
Frederik Hanghøj Iversen 181edc0cd5 Prove step 3 in proof of unvivalence for hSet without `ua` 2018-03-21 17:52:32 +01:00
Frederik Hanghøj Iversen 8f67ff9f36 Use explicit parameter for hSet 2018-03-21 15:01:31 +01:00
Frederik Hanghøj Iversen ae0ff092f8 Use prelude everywhere 2018-03-21 14:56:43 +01:00
Frederik Hanghøj Iversen 29f45d1426 Delete equality module 2018-03-21 14:47:01 +01:00
Frederik Hanghøj Iversen 183906dc8c Define and use custom prelude 2018-03-21 14:39:56 +01:00
Frederik Hanghøj Iversen 084befbbc6 Merge remote-tracking branch 'Saizan/dev' into dev 
From Andrea:

The problem with "h" there is that ve-re is building a square, "(qq0 j
, h)" is a fine element of the sigma type, but it does not really
connect "(g ∘ f) e" to "e" across dimension "i", in particular it does
not reduce to "e" when "i" is "i1".
 2018-03-21 13:31:28 +01:00
Frederik Hanghøj Iversen cd3514c8cf Formatting 2018-03-21 13:25:24 +01:00
Andrea Vezzosi ed3b3047e6 Progress on univalence for sets. 2018-03-21 12:00:47 +00:00
Frederik Hanghøj Iversen 890154a81d Simplify qualified imports, change make-target: clean 2018-03-21 12:28:26 +01:00
Frederik Hanghøj Iversen e98ed89db5 Make propositionality a submodule of the actual proposition 2018-03-21 12:21:47 +01:00
Frederik Hanghøj Iversen 4beb48e066 Use correct order for left- and right identity 
Define and use helpers left- and right identity
 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen 71d9acff9a Stuff about half-time report 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen 31257a4d97 Do not export helpers in `Fun` 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen 629115661b Formatting in yoneda 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen b6a9befd9c Naming and formatting 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen 63a51fbfdc Include modules in "everything"-module 2018-03-21 11:58:50 +01:00
Frederik Hanghøj Iversen 811a6bf58e Make univalence a submodule of RawCategory 2018-03-21 11:58:23 +01:00
Frederik Hanghøj Iversen b03bfb0c77 Restructure in free monad 2018-03-20 14:58:27 +01:00
Frederik Hanghøj Iversen 66cb5b363d [WIP] Finnish all intermediate steps for univalence of hSets 2018-03-20 13:26:40 +01:00
Frederik Hanghøj Iversen 2188e690a0 Prove identity law for coercions. 2018-03-20 12:12:09 +01:00
Frederik Hanghøj Iversen 30725d71b6 [WIP] Scary goal 2018-03-20 11:58:54 +01:00
Frederik Hanghøj Iversen 32d1833d51 [WIP] A long way towards proving univalence in the category of hSets 2018-03-20 11:27:04 +01:00
Frederik Hanghøj Iversen 43563d1ad9 [WIP] Univalence for category of homotopy sets 2018-03-19 16:27:03 +01:00