Frederik Hanghøj Iversen
5c4b4db692
Simplifications
2018-04-11 14:10:01 +02:00
Frederik Hanghøj Iversen
1c963db7e6
Make AreInveres an alias for \Sigma
2018-04-11 13:53:33 +02:00
Frederik Hanghøj Iversen
e6a2e3a0f0
Reduce applications of symmetry
2018-04-11 13:18:34 +02:00
Frederik Hanghøj Iversen
770bce52a2
Use 3rd formulation of univalence
2018-04-11 12:54:22 +02:00
Frederik Hanghøj Iversen
4ff8f155ab
[QED] Get equivalence from 3rd formulation
2018-04-11 12:46:22 +02:00
Frederik Hanghøj Iversen
c23c2716a5
Move lemma to equivalence-module
2018-04-11 12:27:33 +02:00
Frederik Hanghøj Iversen
db5fb3603a
Banish qualified import of Function - use \o for fun-comp!
2018-04-11 11:12:09 +02:00
Frederik Hanghøj Iversen
c90b064bb0
Rename \o to <<<
2018-04-11 10:58:50 +02:00
Frederik Hanghøj Iversen
6d59a8f79e
Add note about proving 9.1.9
2018-04-10 17:33:22 +02:00
Frederik Hanghøj Iversen
772e6778f3
[WIP] Univalence in ad-hoc category in product
2018-04-10 17:17:04 +02:00
Frederik Hanghøj Iversen
fd18985e53
Export TypeIsomorphism as an alias for Equivalence.Isomorphism
2018-04-09 18:10:39 +02:00
Frederik Hanghøj Iversen
04144db606
Simplifications and renaming
2018-04-09 18:02:39 +02:00
Frederik Hanghøj Iversen
735b25de23
Simplify proof and move propUnivalent to a more general setting
2018-04-09 16:03:43 +02:00
Frederik Hanghøj Iversen
69689e7b2a
Use a single version of \simeq
2018-04-06 18:27:24 +02:00
Frederik Hanghøj Iversen
36d92c7ceb
Make the category an index of PreCategory
2018-04-06 17:09:15 +02:00
Frederik Hanghøj Iversen
23b562a873
Provide preorder instance for some things - more work on product cat
2018-04-06 16:54:00 +02:00
Frederik Hanghøj Iversen
bbe9460647
Provide composition of isEquiv's
2018-04-05 20:41:14 +02:00
Frederik Hanghøj Iversen
be56027c37
Remove bad lemma for showing univalence
2018-04-05 15:23:50 +02:00
Frederik Hanghøj Iversen
e69ace21a0
Rename id-to-iso to idToIso
2018-04-05 15:21:54 +02:00
Frederik Hanghøj Iversen
b5f89322ac
Add notion of strict category
2018-04-05 15:13:59 +02:00
Frederik Hanghøj Iversen
6c5b68a8ac
Add notion of pre-category
2018-04-05 14:39:54 +02:00
Frederik Hanghøj Iversen
8276deb4aa
Rename proj. to fst and snd
2018-04-05 10:41:56 +02:00
Frederik Hanghøj Iversen
d78965d73f
Try to use lemma for proving univalence of product-category thing
2018-04-04 17:45:36 +02:00
Frederik Hanghøj Iversen
84f88ac2ae
Change what is needed
2018-04-04 12:01:29 +02:00
Frederik Hanghøj Iversen
f66d180ec3
[WIP] Stronger lemma for univalence
2018-04-04 11:27:03 +02:00
Frederik Hanghøj Iversen
172287f0a7
[QED] The ad-hoc product category has hom-sets that are h-sets
2018-04-03 15:23:11 +02:00
Frederik Hanghøj Iversen
1e5fb7d50a
[WIP] Arrows are sets in special product category
2018-04-03 14:46:36 +02:00
Frederik Hanghøj Iversen
467c5d9c0c
[WIP] Propositionality of products
2018-04-03 12:40:20 +02:00
Frederik Hanghøj Iversen
1c6d9ad2b5
Rename identity in category to ascii-name
2018-04-03 11:36:09 +02:00
Frederik Hanghøj Iversen
41b442c0d8
Merge remote-tracking branch 'Saizan/dev' into dev
2018-03-30 12:23:29 +02:00
34e633902f
Category.Product: Factor out use of arrowAreSets to shorten proofs
2018-03-30 11:06:45 +02:00
Frederik Hanghøj Iversen
ba80fe96dc
[WIP] Propositionality for products
2018-03-30 00:12:01 +02:00
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
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
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
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
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
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
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
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
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
Frederik Hanghøj Iversen
c0cf6789cd
Use propositions straight from the horses mouth
2018-03-12 13:56:49 +01:00
Frederik Hanghøj Iversen
a7214fcc66
Finish equality principle for categories
2018-03-12 13:51:29 +01:00
Frederik Hanghøj Iversen
35390c02d3
Stuff about univalence in the category of sets
2018-03-12 13:38:48 +01:00
Frederik Hanghøj Iversen
acb5ff4f2b
Closer to showing univalence for the category of sets
2018-03-08 14:44:23 +01:00
Frederik Hanghøj Iversen
52297d9073
Clean-up in the category of categories
2018-03-08 11:54:13 +01:00
Frederik Hanghøj Iversen
d01514cbdb
Do not use ugly ':'-syntax to disambiguate fields
2018-03-08 11:29:16 +01:00
Frederik Hanghøj Iversen
48672b01bd
Use dotted expression in Cat
2018-03-08 11:20:51 +01:00
Frederik Hanghøj Iversen
5ad506a09f
Rename func* and func-> to omap and fmap respectively
2018-03-08 11:03:56 +01:00
Frederik Hanghøj Iversen
2fcc583646
Add note
2018-03-08 10:50:18 +01:00
Frederik Hanghøj Iversen
63b5f5c68d
Use long name for product object
2018-03-08 10:46:28 +01:00
Andrea Vezzosi