Commit graph

377 commits

Author SHA1 Message Date
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
Frederik Hanghøj Iversen 2058154c65 Helpers to work with isomorphisms and equivalences 2018-03-19 15:15:03 +01:00
Frederik Hanghøj Iversen f69ab0ee62 [WIP] Univalence for the category of hSets 2018-03-19 14:08:59 +01:00
Andrea Vezzosi f7f8953a42 Voe: Use the isomorphism directly for better computation 2018-03-15 13:39:42 +00:00
Frederik Hanghøj Iversen 438978973d Construct isomorphism from equivalence
Using this somewhat round-about way of constructing an isomorphism from
an equivalence has made typechecking slower in some situations.

E.g. if you're constructing an equivalence from gradLemma and later use
that constructed equivalence to recover the isomorphism, then you
might as well have kept using those functions.
2018-03-15 12:33:00 +01:00
Frederik Hanghøj Iversen 360e2b95dd Make parameter to monad equivalence explicit 2018-03-14 11:20:07 +01:00
Frederik Hanghøj Iversen 7aec22b30a Expose both monad formulations qualified from Cat.Category.Monad 2018-03-14 11:00:52 +01:00
Frederik Hanghøj Iversen 6229decfb2 Merge branch 'master' into dev 2018-03-14 10:50:57 +01:00
Frederik Hanghøj Iversen 41e2d02c8d [WIP] Prove voe §2.3
By Andrea

The reason you cannot use cong in [1] is that §2-fromMonad result type
depends on the input, you need a dependent version of cong:

cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A}
               → (f : (x : A) → B x)
               → (eq : x ≡ y)
               → PathP (\ i → B (eq i)) (f x) (f y)
cong-d f p = λ i → f (p i)

I attach a modified Voevodsky.agda.

Notice that the definition of "t" is still highlighted in yellow,
that's because it being a homogeneous path depends on the exact
definition of lem, see the comment with the two definitional equality
constraints.
2018-03-14 10:30:42 +01:00
Frederik Hanghøj Iversen 091e77b583 Rename IsProduct.isProduct to IsProduct.ump
[WIP]: Also some stuff about propositionality for products.
2018-03-14 10:23:23 +01:00
Frederik Hanghøj Iversen 7065455712 More readable goal for voevodsky's construction 2018-03-13 11:29:13 +01:00
Frederik Hanghøj Iversen 3ab88395dc Merge branch 'dev' 2018-03-13 10:41:54 +01:00
Frederik Hanghøj Iversen 6db2a3e5d4 Update changelog and backlog 2018-03-13 10:41:37 +01:00
Frederik Hanghøj Iversen 896e0d3d37 Stuff about univalence for the category of functors 2018-03-13 10:24:50 +01:00
Frederik Hanghøj Iversen fe453a6d3a Trying to prove cummulativity of homotopy levels 2018-03-12 16:00:27 +01:00
Frederik Hanghøj Iversen c52384b012 Change name of fromMonad 2018-03-12 14:43:43 +01:00
Frederik Hanghøj Iversen 5e092964c8 Change naming and fuse some modules 2018-03-12 14:38:52 +01:00
Frederik Hanghøj Iversen ccf753d438 Move monoidal and kleisli representation to own modules 2018-03-12 14:23:23 +01:00
Frederik Hanghøj Iversen 8dadfa22a0 Add documentation header to monad module 2018-03-12 14:11:31 +01:00
Frederik Hanghøj Iversen aa645fb11e Move voevodsky's construction to own module 2018-03-12 14:04:10 +01:00