-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathOurEverything.agda
150 lines (122 loc) · 5.4 KB
/
OurEverything.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
-----------------------------------------------------------------------------------------------
-- The TheoriesAndDataStructures library
--
-- All library modules, along with short descriptions
--
-- Other experimental approaches can be found in the directory Experiments/
--
-- We are using Agda 2.6.0 with standard library version 1.0.1.
-- Items marked with “‼” are not yet up to date and so have been commented out.
-----------------------------------------------------------------------------------------------
module OurEverything where
-- Creates forgetful functors from single sorted algebras to |Set|
--
import Helpers.Forget
import Helpers.Categorical
import Helpers.Hardy
-- ============================================================================================
-- Variations on Sets
-- ============================================================================================
-- “The” one-object one-arrow category, along with general free, forgetful, and adjoint constructions.
--
-- Arrows in the one-object one-arrow category correspond to the functions to a singleton set.
-- ‼ open import Structures.OneCat
-- Category of algebras consisting of an index set and a family of sets on the index set.
-- Along with forgetful functor to Sets with heterogenous equality and free functor, think “Σ”.
--
-- Currently has a hole.
-- ‼ open import Structures.Dependent
-- Category of heterogenous relations along with a few forgetful and (co)free functors and
-- associated adjunction proofs.
--
open import Structures.Rel
-- Category of algebras of a predicate furnished type; c.f., Dependents.
-- Along with a forgetful functor to Sets.
--
-- Many simple-looking holes.
-- ‼ open import Structures.DistinguishedSubset
-- Category of pairs of sets with a few (co)free constructions.
-- Along with a proof that sum is adjoint to squaring which is adjoint to product.
--
open import Structures.TwoSorted
-- Category of pointed sets along with adjuntions with Sets and OneCat.
--
open import Structures.Pointed
-- ============================================================================================
-- Unary Algebras
-- ============================================================================================
-- Category of algebras consisting of a type endowed with an operator; along with
-- adjunctions with Sets.
-- The free structure corresponds to “performing a method” a number of times.
--
open import Structures.UnaryAlgebra
-- Category of involutive algebras with a forgetful functor to Sets,
-- adjunctions, and (co)monads.
--
open import Structures.InvolutiveAlgebra
-- Category of algebras consisting of a carrier with a family of operations on it; i.e., actions.
-- Along with a forgetful functor to Sets and an initial algebra.
--
--
open import Structures.IndexedUnaryAlgebra
-- ============================================================================================
-- Algebras with binary operators, Boom Hierarchy
-- ============================================================================================
-- Interface for multisets over a given type, along with a free construction
-- via sequences.
--
-- ‼ open import Structures.Baguette
-- Category of Magmas along with explicit toolkit of operations for binary trees.
-- Also initial & terminal objects, along with adjunctions with OneCat.
--
open import Structures.Magma
-- Category of semigroups and an explicit theory of operators for non-empty lists.
-- Along with adjunctions with Sets, Magmas, and OneCat.
-- Also an involved proof of the non-existence of a certain adjunction:
-- There cannot be a (free) associative “extension” of an arbitrary binary operator.
--
-- Contains a postulate.
open import Structures.Semigroup
-- Category of setoid-based commutative monoids over a given type, with a forgetful functor.
-- Free constructions can be found in baguette.lagda .
--
-- ‼ open import Structures.CommMonoid
-- Category of monoids with adjunctions with Sets and OneCat.
-- There are holes left intentionally for exposition purposes.
--
open import Structures.Monoid
-- A theory of bags; intend to be the free multisets.
-- ( A difficult read! )
--
-- ‼ open import Structures.SequencesAsBags
-- The category of Set-based Abelian groups, forgetful functor to Sets.
-- Work towards free construction; no free functor yet.
--
-- Contains a postulate.
-- ‼ open import Structures.AbelianGroup
-- ============================================================================================
-- ============================================================================================
-- ============================================================================================
-- Helpers
--
-- The remaining modules are mostly technical ones needed for the structure-theory relationships.
-- ============================================================================================
-- Re-exports all equality-related concepts
--
import Helpers.EqualityCombinators
-- Contains properties about sums and products not found in standard library
--
import Helpers.DataProperties
-- Implicit function application.
--
open import Helpers.Function2
{-
-- Files that asssit baguette.lagda ;; they are from previous work.
-- Mostly laws about Fin and type isomorphisms for it.
--
open import Helpers.TypeEquiv
open import Helpers.FinEquivPlusTimes
open import Helpers.LeqLemmas
open import Helpers.FinNatLemmas
open import Helpers.FinEquivTypeEquiv
-}