catt-agda/Everything.agda at master · alexarice/catt-agda · GitHub

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
151
152
153
154
155
module Everything where

import Catt.Prelude
import Catt.Prelude.Properties

import Catt.Syntax.Base
import Catt.Syntax
import Catt.Syntax.Bundles
import Catt.Syntax.Properties
import Catt.Syntax.Complexity

import Catt.Variables
import Catt.Variables.Properties

import Catt.Globular
import Catt.Globular.Properties

import Catt.Pasting
import Catt.Pasting.Properties

import Catt.Suspension
import Catt.Suspension.Properties
import Catt.Suspension.Pasting

import Catt.Wedge
import Catt.Wedge.Properties
import Catt.Wedge.Pasting

import Catt.Discs
import Catt.Discs.Properties
import Catt.Discs.Pasting

import Catt.Tree
import Catt.Tree.Properties
import Catt.Tree.Pasting

import Catt.Tree.Path
import Catt.Tree.Path.Properties

import Catt.Tree.Structured
import Catt.Tree.Structured.Properties
import Catt.Tree.Structured.Globular
import Catt.Tree.Structured.Globular.Properties
import Catt.Tree.Structured.Construct
import Catt.Tree.Structured.Construct.Properties
import Catt.Tree.Structured.ToTerm

import Catt.Tree.Boundary
import Catt.Tree.Boundary.Properties

import Catt.Tree.Standard
import Catt.Tree.Standard.Properties

import Catt.Tree.Insertion
import Catt.Tree.Insertion.Properties

import Catt.Dyck
import Catt.Dyck.Properties
import Catt.Dyck.Pasting
import Catt.Dyck.Support
import Catt.Dyck.Pruning
import Catt.Dyck.Pruning.Properties
import Catt.Dyck.FromTree
import Catt.Dyck.Pruning.FromInsertion

import Catt.Typing.Base
import Catt.Typing
import Catt.Typing.Rule
import Catt.Typing.Rule.Properties
import Catt.Typing.Properties.Base
import Catt.Typing.Properties.Weakening
import Catt.Typing.Properties.Substitution
import Catt.Typing.Properties.Substitution.Suspended
import Catt.Typing.Properties
import Catt.Typing.Properties.Preservation

import Catt.Globular.Typing
import Catt.Pasting.Typing
import Catt.Suspension.Typing
import Catt.Wedge.Typing
import Catt.Discs.Typing
import Catt.Tree.Typing
import Catt.Tree.Path.Typing
import Catt.Tree.Structured.Typing
import Catt.Tree.Structured.Typing.Properties
import Catt.Tree.Structured.Typing.Preservation
import Catt.Tree.Boundary.Typing
import Catt.Tree.Standard.Typing
import Catt.Tree.Insertion.Typing
import Catt.Dyck.Typing
import Catt.Dyck.Pruning.Typing


import Catt.Typing.DiscRemoval.Rule
import Catt.Typing.DiscRemoval
import Catt.Typing.DiscRemoval.Properties
import Catt.Typing.DiscRemoval.Typed
import Catt.Typing.Properties
import Catt.Typing.EndoCoherenceRemoval.Rule
import Catt.Typing.EndoCoherenceRemoval
import Catt.Typing.EndoCoherenceRemoval.Properties
import Catt.Typing.EndoCoherenceRemoval.Typed
import Catt.Typing.Insertion.Rule
import Catt.Typing.Insertion
import Catt.Typing.Insertion.Equality
import Catt.Typing.Insertion.Typed
import Catt.Typing.Pruning.Rule
import Catt.Typing.Pruning
import Catt.Typing.Pruning.Typed

import Catt.Ops
import Catt.Ops.Pruning
import Catt.Ops.Insertion
import Catt.Ops.All
import Catt.Ops.Regular

import Catt.Support
import Catt.Support.Typing
import Catt.Support.Properties
import Catt.Support.Context

import Catt.Suspension.Support
import Catt.Wedge.Support
import Catt.Discs.Support
import Catt.Dyck.Support
import Catt.Dyck.Pruning.Support
import Catt.Tree.Support
import Catt.Tree.Path.Support
import Catt.Tree.Structured.Support
import Catt.Tree.Structured.Construct.Support
import Catt.Tree.Boundary.Support
import Catt.Tree.Standard.Support
import Catt.Tree.Insertion.Support
import Catt.Tree.Insertion.Boundary.Support

import Catt.Typing.Properties.Support
import Catt.Typing.Structured.Support
import Catt.Typing.DiscRemoval.Support
import Catt.Typing.EndoCoherenceRemoval.Support
import Catt.Typing.Insertion.Support
import Catt.Typing.Pruning.Support

import Catt.Typing.Weak
import Catt.Typing.Strict.DR
import Catt.Typing.Strict.Units
import Catt.Typing.Strict.UA

import Deprecated.Ops.Tree
import Deprecated.Tree.Support
import Deprecated.Tree.Structured.Support
import Deprecated.Tree.Structured.Support.Properties
import Deprecated.Tree.Structured.Construct.Support
import Deprecated.Tree.Standard.Support
import Deprecated.Typing.Structured.Support
import Deprecated.Typing.Insertion.Support