Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Set-enriched categories #1467

Open
wants to merge 62 commits into
base: master
Choose a base branch
from
Open

Set-enriched categories #1467

Changes from 1 commit
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
d884132
Uniqueness of general products (up to isomorphism)
langston-barrett Oct 21, 2018
0d97d7f
Associativity of binary products
langston-barrett Oct 21, 2018
b222d1f
Fix notation conflict
langston-barrett Oct 21, 2018
c13d72e
monoidal structure on categories with products
langston-barrett Oct 22, 2018
e629c8b
Migrate proof of binary product associativity to binproducts.v
langston-barrett Oct 28, 2018
dabdc7b
Add Cartesian.v to CONTENTS.md
langston-barrett Oct 28, 2018
ca9bf06
fix errors
umedaikiti Nov 23, 2021
38574c7
Merge branch 'master' into univalence-slices
nmvdw Feb 13, 2022
2d319b9
Merge pull request #1457 from nmvdw/univalence-slices
benediktahrens Feb 14, 2022
096421b
Street (op)fibs in Cat
nmvdw Feb 14, 2022
70324d3
Merge branch 'master' into street-fib-in-cat
nmvdw Feb 14, 2022
d2273bf
Merge pull request #1458 from nmvdw/street-fib-in-cat
benediktahrens Feb 14, 2022
d04c63d
try to get the unicode notation table to look nice in ASCII viewing mode
DanGrayson Feb 17, 2022
36b3874
Merge branch 'master' of github.com:UniMath/UniMath
DanGrayson Feb 17, 2022
5ff1ae2
add some remarks about emacs to USAGE.md
DanGrayson Feb 17, 2022
c725e07
try to get the unicode notation table to look nice in ASCII viewing m…
DanGrayson Feb 17, 2022
f3bb66e
Duality involutions, rework discrete bicats
nmvdw Feb 18, 2022
393e08c
Merge branch 'master' into duality-involution
nmvdw Feb 18, 2022
fc49805
Whoops....
nmvdw Feb 18, 2022
d239668
Remove comments
nmvdw Feb 18, 2022
368f71d
Forgot to add a file
nmvdw Feb 18, 2022
91d2bb0
Merge pull request #1460 from nmvdw/duality-involution
benediktahrens Feb 18, 2022
6cc9f2e
Uniqueness of general products (up to isomorphism)
langston-barrett Oct 21, 2018
8018188
Associativity of binary products
langston-barrett Oct 21, 2018
e1dd9d7
Fix notation conflict
langston-barrett Oct 21, 2018
6c4c07b
monoidal structure on categories with products
langston-barrett Oct 22, 2018
7e7b846
Migrate proof of binary product associativity to binproducts.v
langston-barrett Oct 28, 2018
740c86e
Add Cartesian.v to CONTENTS.md
langston-barrett Oct 28, 2018
2eeccd0
fix errors
umedaikiti Nov 23, 2021
503a80e
remove obsolete file Cats.v with def of precat of cats
benediktahrens Feb 20, 2022
b76613d
dissolve DispCat/Aux
benediktahrens Feb 20, 2022
c08e9d4
Merge pull request #1461 from benediktahrens/issue-1404
DanGrayson Feb 21, 2022
0da7f1c
Merge branch 'master' into issue-1421-sq
benediktahrens Feb 21, 2022
9abbfb0
Merge pull request #1462 from benediktahrens/issue-1421-sq
DanGrayson Feb 21, 2022
ac60705
remove duplicate z_iso_inv_mor
benediktahrens Feb 22, 2022
9ff746c
remove duplicate z_iso_is_z_isomorphism2
benediktahrens Feb 22, 2022
bb95381
remove comments
benediktahrens Feb 22, 2022
f0da7e2
arguments now implicit
benediktahrens Feb 22, 2022
c5f099d
arguments now implicit II
benediktahrens Feb 22, 2022
78e12b4
arguments now implicit III
benediktahrens Feb 22, 2022
b089c47
arguments now implicit IV
benediktahrens Feb 22, 2022
5362f3a
Merge pull request #1463 from benediktahrens/issue-948
benediktahrens Feb 23, 2022
ff504a7
mention tags-search in the INSTALL file
DanGrayson Mar 2, 2022
e4111db
move tags-search discussion from USAGE to INSTALL
DanGrayson Mar 2, 2022
dbda0c0
remove autorewrite
umedaikiti Mar 4, 2022
6d7c516
Merge branch 'cartesian-monoidal' of github.com:umedaikiti/UniMath in…
umedaikiti Mar 4, 2022
2ac52f4
add correspondence between HSET-enriched and ordinary categories
umedaikiti Mar 5, 2022
126a7e9
improve proofs
umedaikiti Mar 5, 2022
39ea615
Merge branch 'UniMath:master' into cartesian-monoidal
umedaikiti Mar 5, 2022
ea2e038
Merge branch 'UniMath:master' into cartesian-monoidal
umedaikiti Mar 5, 2022
0a08dae
remove auto and autorewrite
umedaikiti Mar 5, 2022
16ae6a5
move some parts to UniMath/Bicategories/EnrichedCategories
umedaikiti Mar 7, 2022
18f4a6c
Merge branch 'master' into cartesian-monoidal
benediktahrens Mar 11, 2022
7166753
Merge branch 'master' into cartesian-monoidal
benediktahrens Oct 18, 2022
70c125f
Update UniMath/CategoryTheory/limits/binproducts.v
benediktahrens Nov 7, 2022
9788301
Update UniMath/CategoryTheory/limits/binproducts.v
benediktahrens Nov 7, 2022
2a7cdc5
Update UniMath/CategoryTheory/limits/binproducts.v
benediktahrens Nov 7, 2022
5d42579
Update UniMath/CategoryTheory/limits/binproducts.v
benediktahrens Nov 7, 2022
7c41460
Update UniMath/CategoryTheory/limits/binproducts.v
benediktahrens Nov 7, 2022
98f0cc6
Merge branch 'master' into cartesian-monoidal
benediktahrens Nov 7, 2022
41339c6
Merge branch 'master' into cartesian-monoidal
benediktahrens Nov 18, 2022
9d5e0e4
Update UniMath/CategoryTheory/Monoidal/Cartesian.v
benediktahrens Nov 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix notation conflict
  • Loading branch information
@langston-barrett @umedaikiti
langston-barrett authored and umedaikiti committed Nov 22, 2021
commit b222d1f2da3ee1567e18af0858c3d8b6a4d4e696
36 changes: 18 additions & 18 deletions UniMath/CategoryTheory/limits/binproducts.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -842,12 +842,12 @@ Section Assoc.
Context (BPC : BinProducts C).
Context (hsC : has_homsets C).

Local Notation "c '⊗' d" := (BinProductObject C (BPC c d)) (at level 75) : cat.
Let π1 {x y} : C⟦x ⊗ y,x⟧ := BinProductPr1 _ (BPC x y).
Let π2 {x y} : C⟦x ⊗ y,y⟧ := BinProductPr2 _ (BPC x y).
Definition binprod_assoc (x y z : C) : C⟦(x ⊗ y) ⊗ z,x ⊗ (y ⊗ z)⟧ :=
Local Notation "c '⊠' d" := (BinProductObject C (BPC c d)) (at level 40) : cat.
Let π1 {x y} : C⟦x ⊠ y,x⟧ := BinProductPr1 _ (BPC x y).
Let π2 {x y} : C⟦x ⊠ y,y⟧ := BinProductPr2 _ (BPC x y).
Definition binprod_assoc (x y z : C) : C⟦(x ⊠ y) ⊠ z, x ⊠ (y ⊠ z)⟧ :=
BinProductArrow _ _ (π1 · π1) (BinProductArrow _ _ (π1 · π2) π2).
Let α {x y z} : C⟦(x ⊗ y) ⊗ z,x ⊗ (y ⊗ z)⟧ := binprod_assoc x y z.
Let α {x y z} : C⟦(x ⊠ y) ⊠ z, x ⊠ (y ⊠ z)⟧ := binprod_assoc x y z.

(** A type with three inhabitants, used for indexing ternary products *)
Let three : UU := coprod unit bool.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's already a type like this in Combinatorics/StandardFiniteSets.v

Expand All @@ -872,12 +872,12 @@ Section Assoc.
+ exact pc.
Defined.

Local Definition l_pr1 {x y z : C} : C ⟦(x ⊗ y) ⊗ z, x⟧ := π1 · π1.
Local Definition l_pr2 {x y z : C} : C ⟦(x ⊗ y) ⊗ z, y⟧ := π1 · π2.
Local Definition l_pr3 {x y z : C} : C ⟦(x ⊗ y) ⊗ z, z⟧ := π2.
Local Definition l_pr1 {x y z : C} : C ⟦(x ⊠ y) ⊠ z, x⟧ := π1 · π1.
Local Definition l_pr2 {x y z : C} : C ⟦(x ⊠ y) ⊠ z, y⟧ := π1 · π2.
Local Definition l_pr3 {x y z : C} : C ⟦(x ⊠ y) ⊠ z, z⟧ := π2.

Lemma left_assoc_ternary_product :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be good to make parts of this construction opaque.

∏ a b c : C, isProduct _ _ (three_rec a b c) ((a ⊗ b) ⊗ c)
∏ a b c : C, isProduct _ _ (three_rec a b c) ((a ⊠ b) ⊠ c)
(three_ind l_pr1 l_pr2 l_pr3).
Proof.
intros a b c.
Expand Down Expand Up @@ -915,12 +915,12 @@ Section Assoc.
Defined.


Local Definition r_pr1 {x y z : C} : C ⟦x ⊗ (y ⊗ z), x⟧ := π1.
Local Definition r_pr2 {x y z : C} : C ⟦x ⊗ (y ⊗ z), y⟧ := π2 · π1.
Local Definition r_pr3 {x y z : C} : C ⟦x ⊗ (y ⊗ z), z⟧ := π2 · π2.
Local Definition r_pr1 {x y z : C} : C ⟦x ⊠ (y ⊠ z), x⟧ := π1.
Local Definition r_pr2 {x y z : C} : C ⟦x ⊠ (y ⊠ z), y⟧ := π2 · π1.
Local Definition r_pr3 {x y z : C} : C ⟦x ⊠ (y ⊠ z), z⟧ := π2 · π2.

Lemma right_assoc_ternary_product :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be good to make parts of this construction opaque.

∏ a b c : C, isProduct _ _ (three_rec a b c) (a ⊗ (b ⊗ c))
∏ a b c : C, isProduct _ _ (three_rec a b c) (a ⊠ (b ⊠ c))
(three_ind r_pr1 r_pr2 r_pr3).
Proof.
intros a b c.
Expand Down Expand Up @@ -957,15 +957,15 @@ Section Assoc.
apply hsC.
Defined.

Lemma binproduct_assoc_iso : ∏ a b c : C, iso (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c).
Lemma binproduct_assoc_iso : ∏ a b c : C, iso (a ⊠ (b ⊠ c)) ((a ⊠ b) ⊠ c).
Proof.
intros.
pose (p1 := mk_Product _ _ _ (a ⊗ (b ⊗ c)) _
pose (p1 := mk_Product _ _ _ (a ⊠ (b ⊠ c)) _
ltac:(apply right_assoc_ternary_product)).
pose (p2 := mk_Product _ _ _ ((a ⊗ b) ⊗ c) _
pose (p2 := mk_Product _ _ _ ((a ⊠ b) ⊠ c) _
ltac:(apply left_assoc_ternary_product)).
replace (a ⊗ (b ⊗ c)) with (ProductObject _ _ p1) by reflexivity.
replace ((a ⊗ b) ⊗ c) with (ProductObject _ _ p2) by reflexivity.
replace (a ⊠ (b ⊠ c)) with (ProductObject _ _ p1) by reflexivity.
replace ((a ⊠ b) ⊠ c) with (ProductObject _ _ p2) by reflexivity.
eapply mk_iso.
eapply product_unique.
Qed.
Expand Down