Created
October 26, 2020 15:42
-
-
Save zampino/18bd319946e6bb601bf7c4366033565f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "nbformat": 4, | |
| "nbformat_minor": 4, | |
| "metadata": { | |
| "kernelspec": { | |
| "display_name": "Agda", | |
| "language": "agda", | |
| "name": "agda" | |
| }, | |
| "nextjournal": { | |
| "nodes-edn": "{\"db7fd314-1f67-450b-ba82-2a3c5df5f20b\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"db7fd314-1f67-450b-ba82-2a3c5df5f20b\", :compute-ref #uuid \"9cf9943c-1e9d-42bc-a647-3bd95d331060\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2192}, \"432de536-51da-469a-9c3c-2541262984d2\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"432de536-51da-469a-9c3c-2541262984d2\", :compute-ref #uuid \"cf76a891-e2a6-439b-8642-7fe846376179\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 1928}, \"9867a420-7cf9-407b-94a8-49313db6201e\" {:name nil, :output-log-lines {:stdout 1}, :language \"agda\", :id \"9867a420-7cf9-407b-94a8-49313db6201e\", :compute-ref #uuid \"24ba892a-37bd-4d32-b874-b325296af3df\", :runtime [:runtime \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\"], :kind \"code\", :error nil, :exec-duration 530}, \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\" {:name \"FDS.List.AllPairs.Lemmas\", :docker/environment-image \"docker.nextjournal.com/environment@sha256:1cbbd5d8d2fc475f5cf40c11db3399770f66244241f1e09d2261fc1cc633a78f\", :output-log-lines nil, :environment/visibility :public, :type :jupyter, :environment? true, :language \"agda\", :id \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\", :compute-ref #uuid \"cbc4dff6-a165-4397-829b-743e29301ae1\", :kind \"runtime\", :error {:message \"Agda process went out of memory. You can assign this runtime more memory in the runtime settings and shutdown and restart the runner.\"}, :environment [:environment \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\"], :resources {:machine-type \"n1-standard-2\"}, :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"09347a78-fbf2-4f43-8741-24b9534840f4\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"09347a78-fbf2-4f43-8741-24b9534840f4\", :compute-ref #uuid \"d592881a-217d-4c55-b850-709817ca2853\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 5916}, \"1f966dd7-dbaf-45d7-976f-cd5818dd7433\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"1f966dd7-dbaf-45d7-976f-cd5818dd7433\", :compute-ref #uuid \"424b8432-2938-448a-aaa1-dbdcda509fe4\", :runtime [:runtime \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\"], :kind \"code\", :error nil, :exec-duration 1590}, \"3228cbec-4b4b-4109-a844-b267e275c63d\" {:name \"cover-⊤\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"3228cbec-4b4b-4109-a844-b267e275c63d\", :compute-ref #uuid \"7ba2d99f-faee-49b8-ac66-b843e90fba6b\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 1631}, \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\" {:name \"FDS.Properties\", :docker/environment-image \"docker.nextjournal.com/environment@sha256:2288edb9be491013107779064cc61f4fe716f43fb9d7a252660f6385c81aa410\", :output-log-lines nil, :environment/visibility :public, :type :jupyter, :environment? true, :language \"agda\", :id \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\", :compute-ref #uuid \"af6a2033-e5da-407c-bea0-6b70040ee12f\", :kind \"runtime\", :error {:message \"Agda process went out of memory. You can assign this runtime more memory in the runtime settings and shutdown and restart the runner.\"}, :environment [:environment \"001a638e-cb6d-4949-8089-555770a114f0\"], :resources {:machine-type \"n1-standard-2\"}, :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"332fd3a1-f6ce-4ecd-b71c-f3706cef54c7\" {:stdout-collapsed? true, :output-log-lines {:stdout 4}, :language \"agda\", :id \"332fd3a1-f6ce-4ecd-b71c-f3706cef54c7\", :compute-ref #uuid \"698baea0-6a23-48e6-974f-c5a9b9ba2438\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 1278}, \"8ebd828f-a633-42c5-b754-36eedbdad4ce\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"8ebd828f-a633-42c5-b754-36eedbdad4ce\", :compute-ref #uuid \"5cd716d2-ea34-4f0a-a12e-7b845cec1949\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 35660}, \"79ab93ae-44bf-4080-9d48-642fc6356085\" {:id \"79ab93ae-44bf-4080-9d48-642fc6356085\", :kind \"code\", :language \"agda\", :output-log-lines {:stdout 1}, :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :compute-ref #uuid \"b872853d-6c02-4c6c-8704-8d04401be1c1\", :exec-duration 2105, :error nil}, \"a7571efc-153d-4e69-807f-7e9de036cef8\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"a7571efc-153d-4e69-807f-7e9de036cef8\", :compute-ref #uuid \"079432a4-c990-4ace-982e-94cedb4fbd49\", :runtime [:runtime \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\"], :kind \"code\", :error nil, :exec-duration 1546}, \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\" {:name \"FDS.Subset.Helpers\", :docker/environment-image \"docker.nextjournal.com/environment@sha256:3bece0a7ac451ab4711847dcb20a18febba9aec0577e4d75dd17326119458bc4\", :output-log-lines nil, :environment/visibility :public, :type :jupyter, :environment? true, :language \"agda\", :id \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\", :compute-ref #uuid \"9d82a783-5f14-4242-a424-17f3364b9762\", :kind \"runtime\", :error {:message \"Agda process went out of memory. You can assign this runtime more memory in the runtime settings and shutdown and restart the runner.\"}, :environment [:environment {:article/nextjournal.id #uuid \"02b5e9b4-9ab0-4adb-9164-9a36ba7b17a1\", :change/nextjournal.id #uuid \"5f06c7c3-9cd8-4e40-becf-4e76cca439cb\", :node/id \"3159bc83-58eb-4c79-8f37-f0429767a98a\", :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}], :resources {:machine-type \"n1-standard-2\"}, :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"5bc6d40b-dffc-4987-9148-0be957b2407f\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"5bc6d40b-dffc-4987-9148-0be957b2407f\", :compute-ref #uuid \"627ec104-b974-4549-9baf-ce17f07771af\", :runtime [:runtime \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\"], :kind \"code\", :error nil, :exec-duration 1631}, \"23f5b511-9787-48c3-b73c-d71df2ab89a9\" {:output-log-lines {:stdout 1}, :start 5374, :language \"agda\", :id \"23f5b511-9787-48c3-b73c-d71df2ab89a9\", :compute-ref #uuid \"3168c580-ad5d-4507-af49-ca158a71a56e\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :end 5375, :exec-duration 3023, :completions []}, \"58000243-64e0-4956-ac43-2a5330e25091\" {:name \"syntax\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"58000243-64e0-4956-ac43-2a5330e25091\", :compute-ref #uuid \"bad65c6c-e35c-466e-a501-7f0167345e2b\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2213}, \"7944fb03-1305-44ad-a6b1-642118139fb5\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"7944fb03-1305-44ad-a6b1-642118139fb5\", :compute-ref #uuid \"88e1f708-a9d5-4520-b944-600007c3c30b\", :runtime [:runtime \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\"], :kind \"code\", :error nil, :exec-duration 1177}, \"636ff5d4-f933-4fe8-b462-6e1557a46545\" {:name \"Disj definition\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"636ff5d4-f933-4fe8-b462-6e1557a46545\", :compute-ref #uuid \"1e415be5-d2fe-4bc4-bf3e-a91798c3f883\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 1396}, \"8bfadc34-97fa-4e59-83e3-ad6f6486bc8b\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"8bfadc34-97fa-4e59-83e3-ad6f6486bc8b\", :compute-ref #uuid \"74b07c76-3e95-4bbf-bce5-ce821e0f453c\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 1439}, \"8521ca04-11bc-415a-a978-223e5a445de4\" {:output-log-lines {:stdout 4}, :language \"agda\", :id \"8521ca04-11bc-415a-a978-223e5a445de4\", :compute-ref #uuid \"8575d5ac-fc2f-4347-a1d9-eb031ad705ad\", :runtime [:runtime \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\"], :kind \"code\", :error nil, :exec-duration 1496}, \"70bbc7da-0599-49b7-8ee2-76c333392b76\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"70bbc7da-0599-49b7-8ee2-76c333392b76\", :compute-ref #uuid \"81d0c8d8-103d-4486-a40e-a9feae0ba205\", :runtime [:runtime \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\"], :kind \"code\", :error nil, :exec-duration 1822}, \"ba6971d4-9a9d-4a65-9a71-bc86a85edab6\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"ba6971d4-9a9d-4a65-9a71-bc86a85edab6\", :compute-ref #uuid \"5666894a-9c6b-4d7e-a003-899a28deb9c6\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2753}, \"8de73dc8-efc8-4731-99b4-ddd2ab7cead8\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"8de73dc8-efc8-4731-99b4-ddd2ab7cead8\", :compute-ref #uuid \"98d0f8dd-f150-4aa2-82c1-d6bfcd9d42d8\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2150}, \"dcb3f93a-82bc-4a9e-ac58-8eb836de95bf\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"dcb3f93a-82bc-4a9e-ac58-8eb836de95bf\", :compute-ref #uuid \"1369ff10-ff06-4dbe-8090-bb0cd272b393\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 3007}, \"689e0354-5c1f-4973-b747-2bb53787aa7b\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"689e0354-5c1f-4973-b747-2bb53787aa7b\", :compute-ref #uuid \"39987aa5-0835-408f-8580-226dc0bba3b8\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 1997}, \"0379159b-5a4e-461f-b7f3-e5c208b93157\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"0379159b-5a4e-461f-b7f3-e5c208b93157\", :compute-ref #uuid \"92875cd1-6cff-4185-98cb-6700a699f37e\", :runtime [:runtime \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\"], :kind \"code\", :error nil, :exec-duration 1602}, \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\" {:name \"FDS.Characterisation\", :output-log-lines nil, :type :jupyter, :language \"agda\", :id \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\", :compute-ref #uuid \"4cbd821b-927d-41d9-be40-bbb72ce9fee5\", :kind \"runtime\", :error nil, :environment [:environment \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"b4bc070d-80b1-4141-b8ad-4f42fc63f913\" {:name nil, :output-log-lines {:stdout 1}, :language \"agda\", :id \"b4bc070d-80b1-4141-b8ad-4f42fc63f913\", :compute-ref #uuid \"a926429b-21e5-4baf-b905-40445e40c508\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 23278}, \"8e8dc164-9aa7-44c7-8441-c15fd7d099c4\" {:name \"∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"8e8dc164-9aa7-44c7-8441-c15fd7d099c4\", :compute-ref #uuid \"947c3820-52f2-4d8e-a5d8-501a058eb50f\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 2310}, \"38916189-075c-43d2-a5c9-9e790e9f9204\" {:name nil, :output-log-lines {:stdout 1}, :language \"agda\", :id \"38916189-075c-43d2-a5c9-9e790e9f9204\", :compute-ref #uuid \"0fb955d9-79c3-481d-90b9-66e1579400ed\", :runtime [:runtime \"001a638e-cb6d-4949-8089-555770a114f0\"], :kind \"code\", :error nil, :exec-duration 484}, \"553541d9-b9f5-4634-a4c9-2b042ba723d7\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"553541d9-b9f5-4634-a4c9-2b042ba723d7\", :compute-ref #uuid \"cc79b2a3-ac2b-4c92-9730-3f313708d22e\", :runtime [:runtime \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\"], :kind \"code\", :error nil, :exec-duration 16570}, \"001a638e-cb6d-4949-8089-555770a114f0\" {:name \"FDS\", :docker/environment-image \"docker.nextjournal.com/environment@sha256:c07e4cdd473c9c4116e843ad7728526fe6bdcae88980a6d0123056898477767b\", :output-log-lines nil, :environment/visibility :public, :type :jupyter, :environment? true, :language \"agda\", :id \"001a638e-cb6d-4949-8089-555770a114f0\", :compute-ref #uuid \"4c6ccd7f-297d-4060-b7de-48f4c4417847\", :kind \"runtime\", :error {:message \"Agda process went out of memory. You can assign this runtime more memory in the runtime settings and shutdown and restart the runner.\"}, :environment [:environment \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :resources {:machine-type \"n1-standard-2\"}, :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"2326fb0f-f24a-4cf1-bfad-72e9c7c0c41b\" {:id \"2326fb0f-f24a-4cf1-bfad-72e9c7c0c41b\", :kind \"code\", :language \"agda\", :output-log-lines {:stdout 1}, :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :compute-ref #uuid \"e580361d-395b-4055-8287-2bb97cfc4135\", :exec-duration 2005, :error nil}, \"b6095d83-f7b4-4911-a324-aa0929c769a1\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"b6095d83-f7b4-4911-a324-aa0929c769a1\", :compute-ref #uuid \"ca47cc15-0d05-48e7-bbf6-e720a137cabb\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2525}, \"452eea9a-fed2-439d-bf17-b79338acd886\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"452eea9a-fed2-439d-bf17-b79338acd886\", :compute-ref #uuid \"9b05c6ac-d177-46ed-9ce5-9ca300e79543\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :kind \"code\", :error nil, :exec-duration 2651}, \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\" {:name \"FDS.Fin.Subset.Lemmas\", :docker/environment-image \"docker.nextjournal.com/environment@sha256:8beca6329ffe93d9b16a31e17d06db66b5ee89832d2540c79d494113618794f9\", :output-log-lines nil, :environment/visibility :public, :type :jupyter, :environment? true, :language \"agda\", :id \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\", :compute-ref #uuid \"0e06886b-addf-49cc-a5c2-6d48582fc532\", :kind \"runtime\", :error nil, :environment [:environment \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\"], :resources {:machine-type \"n1-standard-2\"}, :jupyter/kernelspec {:argv [\"/opt/conda/bin/python\" \"-m\" \"agda_kernel\" \"-f\" \"{connection_file}\"], :display_name \"agda\", :language \"agda\", :name \"agda\"}}, \"faf28a9e-2687-495a-96a9-8e4667e27639\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"faf28a9e-2687-495a-96a9-8e4667e27639\", :compute-ref #uuid \"19286154-d432-4714-99ba-ef7741bb708b\", :runtime [:runtime \"92ff9e06-7e90-41fc-a62f-1ef7534b4fcd\"], :kind \"code\", :error nil, :exec-duration 35290}, \"89a498df-ba4b-4c23-a391-6b0c0602746e\" {:name \"∣p⊍q∣≡∣p∣+∣q∣ proof\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"89a498df-ba4b-4c23-a391-6b0c0602746e\", :compute-ref #uuid \"73882362-b5ca-442d-be2a-c647efc95e3d\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 2105}, \"00093044-b75b-4cdc-ac53-28e6b7fc6c27\" {:id \"00093044-b75b-4cdc-ac53-28e6b7fc6c27\", :kind \"code\", :language \"agda\", :runtime [:runtime \"7099ac9a-afc5-485c-b08b-2f37ad1545a5\"], :error nil, :compute-ref #uuid \"4db496c8-86cb-4059-98f6-455f6966a4f2\", :exec-duration 1978, :output-log-lines {:stdout 1}}, \"c42de863-b99d-4a32-bd3c-c96793d14799\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"c42de863-b99d-4a32-bd3c-c96793d14799\", :compute-ref #uuid \"3f26e12a-ec73-4837-8601-3239846a7d26\", :runtime [:runtime \"a10b7940-19c8-4a97-a73a-d26d1e7ac221\"], :kind \"code\", :error nil, :exec-duration 1564}, \"03b65d11-f63b-4fac-ab54-9ec7285c9736\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"03b65d11-f63b-4fac-ab54-9ec7285c9736\", :compute-ref #uuid \"8636a7e8-7f8a-4a9c-b434-38ab45b81b80\", :runtime [:runtime \"67d22448-1b7d-47b6-bd49-89c8179e8d1a\"], :kind \"code\", :error nil, :exec-duration 1498}, \"9dddb353-d466-4cc1-bb3e-65fe37271813\" {:id \"9dddb353-d466-4cc1-bb3e-65fe37271813\", :kind \"code\", :language \"agda\", :output-log-lines {:stdout 1}, :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :compute-ref #uuid \"0825917f-a823-4457-8a6e-d35fffde9b81\", :exec-duration 2352, :error nil}, \"89d4309c-5c73-402b-b8f9-3fed03766704\" {:name \"imports\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"89d4309c-5c73-402b-b8f9-3fed03766704\", :compute-ref #uuid \"9c00e940-85f7-4aa8-b20c-842b9b58a7fd\", :runtime [:runtime \"001a638e-cb6d-4949-8089-555770a114f0\"], :kind \"code\", :error nil, :exec-duration 1286}, \"a8f87b36-6be7-47f3-9528-b921b43fdf61\" {:output-log-lines {:stdout 1}, :language \"agda\", :id \"a8f87b36-6be7-47f3-9528-b921b43fdf61\", :compute-ref #uuid \"b04f9398-ff8e-4eeb-9280-1880652a1c12\", :runtime [:runtime \"83835ee6-d21b-4cbc-b7ce-50733984ab5f\"], :kind \"code\", :error nil, :exec-duration 1701}, \"55768a75-d0c3-4b08-8b18-24b922b75e63\" {:name \"FinDecEq\", :output-log-lines {:stdout 1}, :language \"agda\", :id \"55768a75-d0c3-4b08-8b18-24b922b75e63\", :compute-ref #uuid \"8763cb1f-7231-4957-844a-80b840248283\", :runtime [:runtime \"001a638e-cb6d-4949-8089-555770a114f0\"], :kind \"code\", :error nil, :exec-duration 1334}}", | |
| "runtime-id": "7099ac9a-afc5-485c-b08b-2f37ad1545a5", | |
| "url": "https://staging.nextjournal.com/zampino/finite-decidable-setoids" | |
| } | |
| }, | |
| "cells": [ | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# Finite Decidable Setoids\n\n<h2 class=\"pm-node nj-subtitle\">An Agda exploration of decidable equivalence relations over finite sets</h2>\n\n*In set-based mathematics a finite equivalence relation can be fully characterised in terms of subset-membership in equivalence classes. This is trivial to prove on paper, less so to be formalised in Agda. This short writing is an attempt in that direction. The main motivation behind this is the formalisation of combinatory results when dealing with invariants of algebraic structures: the paradigmatic example here is the [orbital equation from Group Theory](https://github.com/zampino/ggt#orbital-correspondance) applied to the finite case.*\n\nGiven an equivalence relation $\\omega\n$ over a finite set $F$then $F$ is the *disjoint union* of all classes in a set of *canonical representatives* $T$\n\n$$\nF = \\bigcup_{\\alpha\\in T}[\\,\\alpha\\,]_\\omega\n$$\nand in particular \n\n$$\n\\mid F\\mid = \\Sigma_{\\alpha\\in T}\\mid [\\,\\alpha\\,]_\\omega\\mid\n$$\n# Definitions" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module FDS where" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "38916189-075c-43d2-a5c9-9e790e9f9204", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Level renaming (suc to lsuc; zero to lzero)\nopen import Relation.Nullary\nopen import Relation.Binary\nopen import Data.Nat.Base\nopen import Data.Fin\nopen import Data.List\nopen import Data.List.Relation.Unary.Any\nopen import Data.List.Relation.Unary.AllPairs\nopen import Data.Vec as Vec\nopen import Data.Fin.Subset\nopen import Function.Base using (_∘_)\nopen import FDS.Fin.Subset.Lemmas" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "89d4309c-5c73-402b-b8f9-3fed03766704", | |
| "kind": "code", | |
| "language": "agda" | |
| }, | |
| "jupyter": { | |
| "source_hidden": true | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "record FinDecEq {a} (n : ℕ) : Set (lsuc a) where\n field\n _ω_ : Rel (Fin n) a\n isDecEq : IsDecEquivalence _ω_\n\n std : DecSetoid _ _\n std = record { Carrier = (Fin n) ;\n _≈_ = _ω_ ;\n isDecEquivalence = isDecEq }\n\n open DecSetoid std\n renaming (_≟_ to _ω?_ ;\n refl to ω-refl ;\n sym to ω-sym ;\n trans to ω-transitive ;\n Carrier to F)\n public\n\n [_]ω : (Fin n) → Subset n\n [ o ]ω = Vec.tabulate (does ∘ (_ω? o))" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "55768a75-d0c3-4b08-8b18-24b922b75e63", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "define a separate module for proving properties\n\n# Properties of Finite Decidable Setoids\n\nThe following module reads as *take a natural* number $n$ *and a* *finite decidable setoid $FDS$ over a set of $n$ elements, then ...*" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Level\nopen import Data.Nat.Base\nopen import FDS using (FinDecEq)\n\nmodule FDS.Properties {a : Level} {n : ℕ} {FDS : FinDecEq {a} n} where\n\nopen import FDS.Fin.Subset.Lemmas\nopen import FDS.List.AllPairs.Lemmas" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "8ebd828f-a633-42c5-b754-36eedbdad4ce", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Data.Product\nopen import Function.Base\nopen import Data.Bool.Base hiding (_≤_)\nopen import Data.Fin.Subset\nopen import Data.Fin.Subset.Properties\nopen import Data.Unit hiding (_≟_;⊤)\nopen import Data.Vec as Vec\nopen import Data.Vec.Properties\nopen import Data.List as List\nopen import Data.List.Properties\nopen import Data.List.Relation.Unary.Any as Any hiding (index)\nopen import Data.List.Relation.Unary.Any.Properties as AnyProps\nopen import Data.List.Relation.Unary.AllPairs as AllPairs\nopen import Data.List.Relation.Unary.AllPairs.Properties as AllPairsProps\nopen import Relation.Nullary\nopen import Relation.Nullary.Decidable\nopen import Relation.Unary hiding (_∈_;_⊆_;Empty;_∩_;⋃)\nopen import Relation.Binary.PropositionalEquality as Eq\nopen Eq.≡-Reasoning\nopen import Data.Fin using (_≟_)" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "dcb3f93a-82bc-4a9e-ac58-8eb836de95bf", | |
| "kind": "code", | |
| "language": "agda" | |
| }, | |
| "jupyter": { | |
| "source_hidden": true | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "by opening the record type, within this module $FinDecEq$ definitions are directly available. Note we distinguish $\\in$ subset-membership from $\\in_\\ell$ list-membership. Also note that in the following $F$denotes the (type of) the finite set with $n$ elements." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open FinDecEq FDS\nimport Data.List.Membership.Propositional\nmodule MP = Data.List.Membership.Propositional {A = F}\nopen MP renaming (_∈_ to _∈ℓ_)\nopen import Data.List.Membership.Propositional.Properties\n\nlmap = List.map\nsyntax lmap (λ x → B) L = ⟦ B ∣ x ∈ℓ L ⟧\nFˡ = List.allFin n" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "58000243-64e0-4956-ac43-2a5330e25091", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "First basic fact: to be in relation means to belong to equivalence class." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "ω⇒∈ : ∀ {x y} → x ω y → x ∈ [ y ]ω\nω⇒∈ {x} {y} xωy = let lkp = begin \n Vec.lookup [ y ]ω x ≡⟨ lookup∘tabulate _ x ⟩\n does (x ω? y) ≡⟨ dec-true (x ω? y) xωy ⟩\n true ∎\n in lookup⇒[]= x [ y ]ω lkp" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "432de536-51da-469a-9c3c-2541262984d2", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "In particular every class is non empty as a consequence of reflexivity." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "o∈[o]ω : ∀ { o : F } → o ∈ [ o ]ω\no∈[o]ω = ω⇒∈ ω-refl" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "00093044-b75b-4cdc-ac53-28e6b7fc6c27", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "Now, the converse is also true:" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "∈⇒ω : ∀ {x y} → x ∈ [ y ]ω → x ω y\n∈⇒ω {x} {y} x∈[y] = \n let w = begin\n isYes (x ω? y) ≡⟨ isYes≗does _ ⟩ \n does (x ω? y) ≡˘⟨ lookup∘tabulate _ x ⟩\n Vec.lookup [ y ]ω x ≡⟨ []=⇒lookup x∈[y] ⟩\n true ∎\n ≡→T : ∀ {b : Bool} → b ≡ true → T b\n ≡→T = λ { refl → tt }\n r : True (x ω? y)\n r = ≡→T w\n in toWitness r" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "689e0354-5c1f-4973-b747-2bb53787aa7b", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "and by symmetry we have the desired equivalent formulation" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "ω⇒⊆ : ∀ {x y} → x ω y → [ x ]ω ⊆ [ y ]ω\nω⇒⊆ {x} {y} xωy s∈[x] = ω⇒∈ (ω-transitive (∈⇒ω s∈[x]) xωy )\n\nω⇒≡ : ∀ {x y} → x ω y → [ x ]ω ≡ [ y ]ω\nω⇒≡ {x} {y} xωy = ⊆-antisym (ω⇒⊆ xωy) (ω⇒⊆ (ω-sym xωy))" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "09347a78-fbf2-4f43-8741-24b9534840f4", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Canonical Representatives\n\nNow the questions we want to answer next is *how many classes does an equivalence* and *do such classes partition the carrier set*? Or again *can we find a subset on which $x\\mapsto[x]_\\omega$ is a bijection? Can we find a prescribed set of (computationally) well-behaved representatives for the equivalence classes.*\n\nWe first introduce a *canonical choice* $cc\\colon F\\to F$ with the following properties:\n\n* $x\\,\\omega\\,(cc\\, x)\n $ for all $x$\n* $x\\,\\omega\\,y$ *if and only if* $cc\\, x = cc\\,y $\n* $cc$ is *idempotent*\n\nIn a finite setting, given any family of nonempty sets it is possible to find a (decidable!) choice-function: just take the minimum element in effect $cc$ is a finite choice over the family of equivalence classes:" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "cc : F → F\ncc f = index {n} [ f ]ω ( f , o∈[o]ω )\n\nccx∈[x] : ∀ (x : F) → (cc x) ∈ [ x ]ω\nccx∈[x] x = proj₁ (proj₂ (index* [ x ]ω ( x , o∈[o]ω )))\n\nxωccx : ∀ (x : F) → x ω (cc x)\nxωccx x = ω-sym (∈⇒ω (ccx∈[x] x))\n\nc⇒ω : ∀ {x y} → cc x ≡ cc y → x ω y\nc⇒ω {x} {y} ccx≡ccy = let P = λ q → q ∈ [ y ]ω\n w : (cc x) ∈ [ y ]ω\n w = subst P (sym ccx≡ccy) (ccx∈[x] y)\n in ω-transitive (xωccx x) (∈⇒ω w)\n\nω⇒c : ∀ {x y} → x ω y → cc x ≡ cc y\nω⇒c {x} {y} xωy = index-unique _ _ _ _ (ω⇒≡ xωy)\n\ncc-idempt : (x : F) → cc (cc x) ≡ cc x\ncc-idempt x = ω⇒c {cc x} {x} (ω-sym (xωccx x))" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "8de73dc8-efc8-4731-99b4-ddd2ab7cead8", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "A *canonical representative* is *the* minimal element in an equivalence class with respect to the natural order on $F$. This is a decidable property. A transversal of $F$is the set of all canonical representatives (recall that $Fˡ$ is the set $F$represented as List)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "cr : (i : F) → Set\ncr i = i ≡ (cc i)\n\ncr? : Decidable cr\ncr? = λ i → i ≟ (cc i)\n\nTransversal : List F\nTransversal = (List.filter cr? Fˡ)" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "db7fd314-1f67-450b-ba82-2a3c5df5f20b", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Covering\n\nfor all $x$ in $F$there exists an equivalence class of a canonical representative which $x$ belongs to:" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "Covering : ∀ (x : F) → Any (x ∈_) ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧\nCovering x = let\n cover : ∀ (x : F) → (∃ λ k → cr k × x ω k)\n cover t = (cc t) , sym (cc-idempt t) , xωccx t\n (k , crk , xωk) = cover x\n k∈ℓFˡ : k ∈ℓ Fˡ\n k∈ℓFˡ = ∈-allFin {n} k\n k∈ℓTr : k ∈ℓ Transversal\n k∈ℓTr = ∈-filter⁺ cr? k∈ℓFˡ crk\n a : Any (x ω_) Transversal\n a = lose k∈ℓTr xωk\n b : Any ((x ∈_) ∘ [_]ω) Transversal\n b = Any.map ω⇒∈ a\n -- AnyProps.map⁺ : Any (P ∘ f) xs → Any P (List.map f xs)\n in AnyProps.map⁺ b" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "452eea9a-fed2-439d-bf17-b79338acd886", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Disjointness\n\nAny two distinct canonical classes are disjoint" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "Disjointness : AllPairs Disj ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧\nDisjointness = \n let ap₁ : AllPairs _≢_ Fˡ\n ap₁ = AllPairsProps.tabulate⁺ id\n cr-injective : ∀ {x y} → (cr x) → (cr y) → x ≢ y → ¬ x ω y\n cr-injective {x} {y} crx cry x≢y xωy = x≢y (begin x ≡⟨ crx ⟩\n cc x ≡⟨ ω⇒c xωy ⟩\n cc y ≡˘⟨ cry ⟩\n y ∎)\n ω-disj : ∀ {x y} → ¬ (x ω y) → Empty ([ x ]ω ∩ [ y ]ω)\n ω-disj {x} {y} ¬xωy f∈∩ = let f , [x]∩[y] = f∈∩\n l , r = x∈p∩q⁻ _ _ [x]∩[y]\n xωf = ω-sym (∈⇒ω l)\n fωy = ∈⇒ω r\n in ¬xωy (ω-transitive xωf fωy)\n ω-Disj : ∀ {x y} → ¬ x ω y → Disj [ x ]ω [ y ]ω\n ω-Disj ¬xωy = Empty-unique (ω-disj ¬xωy)\n ap₂ : AllPairs (λ x y → ¬ x ω y) Transversal\n ap₂ = filter⁺₃ cr? cr-injective ap₁\n ap₃ = AllPairs.map ω-Disj ap₂ \n in AllPairsProps.map⁺ ap₃" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "b6095d83-f7b4-4911-a324-aa0929c769a1", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Conclusions\n\nNow we can transpose the above results in the language of subsets finding first that the union of all canonical classes gives back the whole finite set $F$." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "CoverAll : ⊤ ≡ ⋃ ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧ \n\nCoverAll = cover-⊤ ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧ Covering" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "23f5b511-9787-48c3-b73c-d71df2ab89a9", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "and furthermore since canonical classes are disjoint" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "Cardinality : n ≡ List.sum ⟦ ∣ [ x ]ω ∣ ∣ x ∈ℓ Transversal ⟧\n\nCardinality = \n let c = ∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧ Disjointness\n d = map-compose {g = ∣_∣} {f = [_]ω} Transversal\n sum = List.sum\n in begin \n n ≡˘⟨ ∣⊤∣≡n n ⟩\n ∣ ⊤ {n} ∣ ≡⟨ cong ∣_∣ CoverAll ⟩\n ∣ ⋃ ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧ ∣ ≡⟨ c ⟩ \n sum (List.map ∣_∣ ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧) ≡˘⟨ cong sum d ⟩\n sum ⟦ ∣ [ x ]ω ∣ ∣ x ∈ℓ Transversal ⟧ ∎" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "ba6971d4-9a9d-4a65-9a71-bc86a85edab6", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# Partitions" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module FDS.Characterisation where\nopen import FDS\nimport FDS.Properties\nopen import FDS.Fin.Subset.Lemmas" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "1f966dd7-dbaf-45d7-976f-cd5818dd7433", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Level renaming (suc to sucℓ)\nopen import Relation.Binary\nopen import Data.Nat.Base as ℕ\nopen import Data.Product\nopen import Data.Fin\nopen import Data.Fin.Subset\nopen import Data.List\nopen import Data.List.Relation.Unary.AllPairs\nopen import Data.List.Relation.Unary.Any as Any" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "faf28a9e-2687-495a-96a9-8e4667e27639", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "record Partition (n : ℕ) : Set (sucℓ 0ℓ) where\n field\n parts : List (Subset n)\n disj : AllPairs Disj parts\n cover : ∀ (x : Fin n) → Any (x ∈_) parts\n \n _ωP_ : Rel (Fin n) 0ℓ\n x ωP y = Any (λ s → x ∈ s × y ∈ s) parts" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "a7571efc-153d-4e69-807f-7e9de036cef8", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "FDS⇒Partition : ∀ {ℓ n} → FinDecEq {ℓ} n → Partition n\nFDS⇒Partition FDS = \n record { parts = ⟦ [ x ]ω ∣ x ∈ℓ Transversal ⟧ ;\n disj = Disjointness ;\n cover = Covering } where\n open FinDecEq FDS\n open FDS.Properties {FDS = FDS}" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "5bc6d40b-dffc-4987-9148-0be957b2407f", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "Partition⇒FDS : ∀ {n} → Partition n → FinDecEq n\nPartition⇒FDS P = \n record { _ω_ = _ωP_ ;\n isDecEq = itis }\n where \n open Partition P\n ωRefl : Reflexive _ωP_\n ωRefl {x} = Any.map {P = λ s → x ∈ s} (λ z → z , z) (cover x)\n ωSym : Symmetric _ωP_\n ωSym = ?\n ωTrans : Transitive _ωP_\n ωTrans = ?\n isEq : IsEquivalence _ωP_\n isEq = record {\n refl = ωRefl ;\n sym = ωSym ; \n trans = ωTrans }\n itis : IsDecEquivalence _ωP_\n itis = record {\n isEquivalence = isEq ;\n _≟_ = ? }" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "8521ca04-11bc-415a-a978-223e5a445de4", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# Subset Lemmas" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module FDS.Fin.Subset.Lemmas where\nopen import FDS.Subset.Helpers" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "b4bc070d-80b1-4141-b8ad-4f42fc63f913", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Level hiding (suc)\nopen import Relation.Unary hiding (_∈_;_⊆_;_∩_;_∪_;⋃;∁)\nopen import Relation.Binary\n\nopen import Data.Nat.Base as ℕ using (ℕ ;_+_; zero; suc; _<_; z≤n; s≤s)\nopen import Data.Nat.Properties using (+-comm)\nopen import Data.Fin \n renaming (zero to fzero; suc to fsuc)\n hiding (fold; _+_; _<_)\nopen import Data.Fin.Properties\nopen import Data.Fin.Subset\nopen import Data.Fin.Subset.Properties\n\nopen import Function.Base\n\nopen import Data.Product\nopen import Data.Sum renaming ([_,_] to _⊞_)\n\nopen import Data.Vec\n\nopen import Data.List renaming ([] to <>;map to lmap; foldr to fold)\nopen import Data.List.Relation.Unary.Any as Any hiding (index)\nopen import Data.List.Relation.Unary.All as All\nopen import Data.List.Relation.Unary.AllPairs\nopen import Data.List.Membership.Propositional renaming (_∈_ to _∈ℓ_)\n\nimport Algebra.Properties.BooleanAlgebra\n\nopen import Relation.Binary.PropositionalEquality as Eq\nopen Eq.≡-Reasoning" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "8bfadc34-97fa-4e59-83e3-ad6f6486bc8b", | |
| "kind": "code", | |
| "language": "agda" | |
| }, | |
| "jupyter": { | |
| "source_hidden": true | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "We'll start with a covering lemma\n\nWe'll work with the following notion of disjointness" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "Disj : ∀ {n} → Subset n → Subset n → Set\nDisj S T = S ∩ T ≡ ⊥\n\nDisj-sym : ∀ {n} → Symmetric (Disj {n = n})\nDisj-sym {n} {S} {T} S∩T≡⊥ = begin T ∩ S ≡⟨ ∩-comm T S ⟩ S ∩ T ≡⟨ S∩T≡⊥ ⟩ ⊥ ∎" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "636ff5d4-f933-4fe8-b462-6e1557a46545", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "We borrow the following proof from x" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "⋃-remove : ∀ {n} {L : List (Subset n)} → ∀ s → (s∈L : s ∈ℓ L) →\n ⋃ L ≡ s ∪ ⋃ (L Any.─ s∈L)\n⋃-remove {n} {<>} _ = λ ()\n⋃-remove {n} {x ∷ xs} s (here px) =\n begin\n ⋃ (x ∷ xs) ≡⟨ refl ⟩\n x ∪ (⋃ xs) ≡˘⟨ cong (_∪ _) px ⟩\n s ∪ (⋃ xs) ≡⟨ cong (_ ∪_) refl ⟩\n s ∪ ⋃ ((x ∷ xs) Any.─ (here {P = P} px)) ∎\n where\n P : Pred (Subset n) Level.zero\n P = s ≡_\n\n⋃-remove {n} {x ∷ xs} s (there s∈L) =\n begin\n x ∪ (⋃ xs) ≡⟨ cong (x ∪_) (⋃-remove {L = xs} s s∈L) ⟩\n x ∪ (s ∪ ⋃ (xs Any.─ s∈L)) ≡˘⟨ ∪-assoc _ _ _ ⟩ -- TODO: -- use solver\n (x ∪ s) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ cong (_∪ _) (∪-comm x s) ⟩\n (s ∪ x) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ ∪-assoc _ _ _ ⟩\n s ∪ (x ∪ ⋃ (xs Any.─ s∈L)) ≡⟨ refl ⟩\n s ∪ ⋃ ((x ∷ xs) Any.─ (there s∈L)) ∎" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "a8f87b36-6be7-47f3-9528-b921b43fdf61", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "We'll also make use of the following covering lemma: if a family of sets covers the whole carrier then its union is the whole set" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "cover-⊤ : ∀ {n} → (L : List (Subset n)) →\n (∀ (x : Fin n) → Any (x ∈_) L ) →\n ⊤ {n} ≡ ⋃ L\n\ncover-⊤ {n} L ∃lx∈l = ⊆-antisym ⊤⊆⋃L (⊆-max (⋃ L)) where\n ⊤⊆⋃L : ⊤ ⊆ (⋃ L)\n ⊤⊆⋃L {x} _ = let\n (l , l∈ℓL , x∈l) = find {P = x ∈_} (∃lx∈l x)\n l⊆l∪* = p⊆p∪q {p = l} (⋃ (L Any.─ l∈ℓL))\n x∈l∪* = l⊆l∪* {x} x∈l\n in subst₂ _∈_ refl (sym (⋃-remove l l∈ℓL)) x∈l∪*" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "3228cbec-4b4b-4109-a844-b267e275c63d", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "∣p⊍q∣≡∣p∣+∣q∣ : ∀ {n} → ∀ (p q : Subset n) → \n Disj p q → ∣ p ∪ q ∣ ≡ ∣ p ∣ + ∣ q ∣ " | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "332fd3a1-f6ce-4ecd-b71c-f3706cef54c7", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "we skip the proof for brevity" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "∣p⊍q∣≡∣p∣+∣q∣ {zero} [] [] d = refl\n∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (outside ∷ q) d = \n begin\n -- ∣ (outside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨⟩\n ∣ p ∪ q ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {outside} d) ⟩\n -- ∣ p ∣ + ∣ q ∣ ≡⟨⟩\n ∣ (outside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎\n\n∣p⊍q∣≡∣p∣+∣q∣ {suc n} (inside ∷ p) (outside ∷ q) d = \n begin -- {! !} -- begin\n ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ refl ⟩ -- cong suc refl ⟩\n -- suc ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ cong suc {! !} ⟩ \n -- cong suc refl ⟩\n suc ∣ p ∪ q ∣ ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {inside} {outside} d)) ⟩\n suc (∣ p ∣ + ∣ q ∣) ≡⟨⟩\n (suc ∣ p ∣) + ∣ q ∣ ≡⟨⟩\n ∣ (inside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎\n\n∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (inside ∷ q) d = \n begin\n ∣ (outside ∷ p) ∪ (inside ∷ q) ∣ ≡⟨ refl ⟩\n suc ∣ p ∪ q ∣ ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {inside} d)) ⟩\n suc (∣ p ∣ + ∣ q ∣) ≡⟨ cong suc (+-comm ∣ p ∣ ∣ q ∣) ⟩\n suc (∣ q ∣ + ∣ p ∣) ≡⟨ refl ⟩\n (suc ∣ q ∣) + ∣ p ∣ ≡⟨⟩\n ∣ (inside ∷ q) ∣ + ∣ (outside ∷ p) ∣ ≡⟨ +-comm ∣ (inside ∷ q) ∣ ∣ (outside ∷ p) ∣ ⟩\n ∣ (outside ∷ p) ∣ + ∣ (inside ∷ q) ∣ ∎" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "89a498df-ba4b-4c23-a391-6b0c0602746e", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ : ∀ {n} → (C : List (Subset n)) → AllPairs Disj C →\n ∣ ⋃ C ∣ ≡ fold _+_ 0 (lmap ∣_∣ C)\n\n∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} <> Δℓ = begin\n ∣ ⋃ {n} <> ∣ ≡⟨⟩\n -- ∣ fold (_∪_ {n}) ⊥ <> ∣ ≡⟨⟩\n ∣ ⊥ {n} ∣ ≡⟨ ∣⊥∣≡0 n ⟩\n 0 ≡⟨⟩\n fold _+_ 0 <> ∎\n∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} (s ∷ C) (h ∷ t) = \n begin\n ∣ ⋃ (s ∷ C) ∣ ≡⟨⟩\n ∣ s ∪ (⋃ C) ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ s (⋃ C) (Disj-sym DisjUCs) ⟩\n ∣ s ∣ + ∣ ⋃ C ∣ ≡⟨ cong (∣ s ∣ +_) (∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} C t ) ⟩\n ∣ s ∣ + (fold _+_ 0 (lmap ∣_∣ C)) ≡⟨⟩\n fold _+_ 0 (lmap ∣_∣ (s ∷ C)) ∎\n where\n a : All (λ x → x ⊆ ∁ s) C\n a = All.map (disj⇒⊆∁ ∘ Disj-sym) h\n c : ⋃ C ⊆ ∁ s\n c = pᵢ⊆q⇒⋃pᵢ⊆q (∁ s) C a\n DisjUCs : Disj (⋃ C) s\n DisjUCs = ⊆∁⇒disj c" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "8e8dc164-9aa7-44c7-8441-c15fd7d099c4", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "we conclude with a proof of existence for a finite choice function" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "fsuc∈ : ∀ {n} → {p : Subset n} → {x : Fin n} → {s : Side} → \n (x ∈ p) → (fsuc x) ∈ (s ∷ p)\nfsuc∈ here = there here\nfsuc∈ (there x∈p) = there (fsuc∈ x∈p)" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "79ab93ae-44bf-4080-9d48-642fc6356085", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "Since finite sets carry a natural order we can always find the smallest element in a non empty subset. Note how Agda type checker eliminates obvious non matching patterns given we're dealing with non-empty sets only." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "index* : ∀ {n} → (s : Subset n) → Nonempty s →\n ∃ (λ x → ( x ∈ s × (∀ {y} → (y ∈ s) → x ≤ y )))\nindex* {suc n} (inside ∷ rest) _ = (fzero , here , λ _ → z≤n )\nindex* {suc n} (outside ∷ rest) ne with (∃-toSum ne)\n... | inj₂ b = let w = drop-there (proj₂ b)\n z = (proj₁ b , w)\n ( a , bb , c ) = (index* rest z)\n in (fsuc a , fsuc∈ bb , λ { (there y∈s) → s≤s (c y∈s) } )\n\nindex : ∀ {n} → (s : Subset n) → Nonempty s → Fin n\nindex s ne = proj₁ (index* s ne)" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "2326fb0f-f24a-4cf1-bfad-72e9c7c0c41b", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "index-unique : ∀ {n} → ∀ (s t : Subset n) → (ns : Nonempty s) →\n (nt : Nonempty t) →\n s ≡ t → (index s ns) ≡ (index t nt)\n\nindex-unique s t ns nt s≡t = let fs , fs∈s , fs≤ = index* s ns\n ft , ft∈t , ft≤ = index* t nt\n ft∈s : ft ∈ s\n ft∈s = subst _ (sym s≡t) ft∈t\n fs∈t : fs ∈ t\n fs∈t = subst _ s≡t fs∈s\n in ≤-antisym (fs≤ ft∈s) (ft≤ fs∈t)" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "9dddb353-d466-4cc1-bb3e-65fe37271813", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# Missing Parts: List Properties" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module FDS.List.AllPairs.Lemmas where" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "9867a420-7cf9-407b-94a8-49313db6201e", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "open import Relation.Nullary\nopen import Relation.Nullary.Decidable\nopen import Relation.Unary\nopen import Relation.Binary hiding (Decidable)\nopen import Data.Product\nopen import Data.List.Base\nopen import Data.List.Relation.Unary.All as All\nopen import Data.List.Relation.Unary.All.Properties\nopen import Data.List.Relation.Unary.AllPairs" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "553541d9-b9f5-4634-a4c9-2b042ba723d7", | |
| "kind": "code", | |
| "language": "agda" | |
| }, | |
| "jupyter": { | |
| "source_hidden": true | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "We need an alternative form of filter introduction rule for the AllPairs predicate, namely " | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module _ {a ℓ ℓ₁ ℓ₂} {A : Set a}\n {R : Rel A ℓ₁} {S : Rel A ℓ₂}\n {P : Pred A ℓ} (P? : Decidable P) where\n\n filter⁺₃ : ∀ {xs} → (∀ {x y} → P x → P y → R x y → S x y) →\n AllPairs R xs → AllPairs S (filter P? xs)\n filter⁺₃ {[]} _ _ = []\n filter⁺₃ {x ∷ xs} Δ (h ∷ t) with (P? x)\n ... | no ¬p = filter⁺₃ {xs} Δ t\n ... | yes p = let\n hf : All (R x) (filter P? xs)\n hf = filter⁺ P? h\n ap : All P (filter P? xs)\n ap = all-filter P? xs\n w : All (P ∩ R x) (filter P? xs)\n w = All.zip ( ap , hf )\n y : P ∩ R x ⊆ S x\n y = λ z → Δ p (proj₁ z) (proj₂ z)\n z : All (S x) (filter P? xs)\n z = All.map y w\n in z ∷ filter⁺₃ {xs} Δ t" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "03b65d11-f63b-4fac-ab54-9ec7285c9736", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# References\n\n#### `[Cohen]` [Pragmatic Quotient Types in Coq](https://perso.crans.org/cohen/papers/quotients.pdf)\n\n#### \\[\\] Definable Quotients in Type Theory\n\n# Appendix: Subset Helpers" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "module FDS.Subset.Helpers where" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "0379159b-5a4e-461f-b7f3-e5c208b93157", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "-- open import Level\n-- open import Data.Nat\n-- open import Relation.Nullary.Decidable\n-- open import Data.Vec.Properties\nopen import Data.Nat.Base as ℕ using (ℕ; zero)\nopen import Data.Product\nopen import Data.Sum renaming ([_,_] to _⊞_)\nopen import Data.Vec as V using (_∷_; [])\nopen import Data.List renaming ([] to <>)\nopen import Data.List.Relation.Unary.All\nopen import Data.Fin.Subset\nopen import Data.Fin.Subset.Properties\n\nopen import Relation.Binary.PropositionalEquality as Eq\nopen Eq.≡-Reasoning\n\nimport Algebra.Properties.BooleanAlgebra" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "7944fb03-1305-44ad-a6b1-642118139fb5", | |
| "kind": "code", | |
| "language": "agda" | |
| }, | |
| "jupyter": { | |
| "source_hidden": true | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "∩-⊆-stable : ∀ {n} → ∀ {p q} → (r : Subset n) → p ⊆ q → (p ∩ r) ⊆ (q ∩ r)\n∩-⊆-stable {_} {p} {q} r p⊆q x∈p∩r = \n let\n x∈p = proj₁ (x∈p∩q⁻ p r x∈p∩r)\n x∈r = proj₂ (x∈p∩q⁻ p r x∈p∩r)\n in x∈p∩q⁺ ( p⊆q x∈p , x∈r )\n\nidʳ⇒⊆ : ∀ {n} → (S T : Subset n) → (S ∪ T) ≡ T → S ⊆ T\nidʳ⇒⊆ {n} S T sut≡t = subst₂ _⊆_ refl sut≡t (p⊆p∪q T)\n\np∩∁p≡⊥ : ∀ {n} → (p : Subset n) → p ∩ ∁ p ≡ ⊥\np∩∁p≡⊥ [] = refl\np∩∁p≡⊥ (outside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)\np∩∁p≡⊥ (inside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)\n\np⊆q⇒p∩∁q≡⊥ : ∀ {n} → {S T : Subset n} → S ⊆ T → S ∩ (∁ T) ≡ ⊥\np⊆q⇒p∩∁q≡⊥ {_} {S} {T} s⊆t = let\n a = p∩∁p≡⊥ _\n b : S ∩ (∁ T) ⊆ T ∩ (∁ T)\n b = ∩-⊆-stable (∁ T) s⊆t\n c = subst₂ _⊆_ refl a b\n in ⊆-antisym c (⊆-min _)\n\ndisj⇒⊆∁ : ∀ {n} → {S T : Subset n} → S ∩ T ≡ ⊥ → S ⊆ (∁ T)\ndisj⇒⊆∁ {n} {S} {T} dst = \n let ct≡suct = begin\n ∁ T ≡˘⟨ ∪-identityˡ _ ⟩\n ⊥ ∪ (∁ T) ≡˘⟨ cong (_∪ (∁ T)) dst ⟩\n (S ∩ T) ∪ (∁ T) ≡⟨ ∪-distribʳ-∩ _ _ _ ⟩\n (S ∪ (∁ T)) ∩ (T ∪ (∁ T)) ≡⟨ cong ((S ∪ (∁ T)) ∩_) (p∪∁p≡⊤ T) ⟩\n (S ∪ (∁ T)) ∩ ⊤ ≡⟨ ∩-identityʳ _ ⟩\n S ∪ (∁ T) ∎\n in idʳ⇒⊆ S (∁ T) (sym ct≡suct)\n\n⊆∁⇒disj : ∀ {n} → {S T : Subset n} → S ⊆ (∁ T) → S ∩ T ≡ ⊥\n⊆∁⇒disj {n} {S} {T} s⊆∁t = \n begin\n S ∩ T ≡˘⟨ cong (S ∩_) (¬-involutive T ) ⟩\n S ∩ (∁ (∁ T)) ≡⟨ p⊆q⇒p∩∁q≡⊥ s⊆∁t ⟩\n ⊥ ∎\n where open Algebra.Properties.BooleanAlgebra (∪-∩-booleanAlgebra n) " | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "c42de863-b99d-4a32-bd3c-c96793d14799", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| }, | |
| { | |
| "cell_type": "code", | |
| "outputs": [], | |
| "execution_count": 1, | |
| "source": [ | |
| "p⊆r×q⊆r⇒p∪q⊆r : ∀ {n} → { p q r : Subset n} → (p ⊆ r) × (q ⊆ r) → (p ∪ q) ⊆ r\np⊆r×q⊆r⇒p∪q⊆r {n} {p} {q} {r} (p⊆r , q⊆r) x∈p∪q = \n let y = x∈p∪q⁻ {n} p q x∈p∪q\n in (p⊆r ⊞ q⊆r) y\n\npᵢ⊆q⇒⋃pᵢ⊆q : ∀ {n} → ∀ S → ∀ (L : List (Subset n)) →\n All (_⊆ S) L → (⋃ L) ⊆ S\npᵢ⊆q⇒⋃pᵢ⊆q S <> _ = ⊆-min S\npᵢ⊆q⇒⋃pᵢ⊆q S (x ∷ xs) (h ∷ t) = \n subst₂ _⊆_ refl refl (p⊆r×q⊆r⇒p∪q⊆r ( h , pᵢ⊆q⇒⋃pᵢ⊆q S xs t ))\n \ndrop-disj : ∀ {n} → {x y : Side} → {p q : Subset n} → \n (x ∷ p) ∩ (y ∷ q) ≡ ⊥ → p ∩ q ≡ ⊥\ndrop-disj {zero} {_} {_} {[]} {[]} _ = refl\ndrop-disj d = cong V.tail d" | |
| ], | |
| "metadata": { | |
| "nextjournal": { | |
| "id": "70bbc7da-0599-49b7-8ee2-76c333392b76", | |
| "kind": "code", | |
| "language": "agda" | |
| } | |
| } | |
| } | |
| ] | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment