CatDat/src/lib/commons/types.ts at f3645fb678b5cfabfda72f39920c352dbc60e1bc · ScriptRaccoon/CatDat · 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
156
157
158
159
160
161
162
163
164
export type Arrayed<T extends readonly unknown[]> = {
	[K in keyof T]: T[K][]
}

type Replace<T, R extends Partial<Record<keyof T, any>>> = Omit<T, keyof R> & R

export type CategoryDisplay = {
	id: string
	name: string
	notation: string
	objects: string
	morphisms: string
	description: string | null
	nlab_link: string | null
	dual_category_id: string | null
	dual_category_name: string | null
	dual_category_notation: string | null
}

export type CategoryShort = Pick<CategoryDisplay, 'id' | 'name'>

export type RelatedCategory = Pick<CategoryDisplay, 'id' | 'name' | 'notation'>

export type TagObject = { tag: string }

export type CommentObject = { id: number; comment: string }

export type ImplicationDB = {
	id: string
	is_equivalence: number
	reason: string
	assumptions: string
	conclusions: string
	is_deduced: number
	dualized_from?: string | null
}

export type ImplicationDisplay = Replace<
	ImplicationDB,
	{
		is_equivalence: boolean
		is_deduced: boolean
		assumptions: string[]
		conclusions: string[]
	}
>

export type PropertyDB = {
	id: string
	relation: string
	description: string
	dual_property_id: string | null
	nlab_link: string | null
	invariant_under_equivalences: number
}

export type PropertyDisplay = Replace<
	PropertyDB,
	{ invariant_under_equivalences: boolean }
>

export type PropertyShort = Pick<PropertyDB, 'id' | 'relation'>

export type DescriptionWithReason = {
	description: string
	reason: string | null
}

export type CategoryPropertyDB = {
	id: string
	reason: string | null
	relation: string
	is_deduced: number
}

export type CategoryProperty = Replace<CategoryPropertyDB, { is_deduced: boolean }>

export type SpecialObject = {
	type: string
	description: string
}

export type SpecialMorphism = {
	type: string
	description: string | null
	reason: string | null
}

export type Structure = 'categories' | 'functors'

export type FunctorShort = {
	id: string
	name: string
}

export type FunctorDB = {
	id: string
	name: string
	source: string
	target: string
	source_name: string
	target_name: string
	description: string
	nlab_link: string | null
}

export type FunctorPropertyDB = {
	id: string
	relation: string
	description: string
	nlab_link: string | null
	invariant_under_equivalences: number
	dual_property_id: string | null
}

export type FunctorPropertyShort = Pick<FunctorPropertyDB, 'id' | 'relation'>

export type FunctorProperty = Replace<
	FunctorPropertyDB,
	{
		invariant_under_equivalences: boolean
	}
>

export type FunctorImplicationDB = {
	id: string
	is_equivalence: number
	reason: string
	assumptions: string
	conclusions: string
	source_assumptions: string
	target_assumptions: string
	dualized_from?: string | null
}

export type FunctorImplicationDisplay = Replace<
	FunctorImplicationDB,
	{
		is_equivalence: boolean
		assumptions: string[]
		conclusions: string[]
		source_assumptions: string[]
		target_assumptions: string[]
	}
>

export type FunctorPropertyAssignmentDB = {
	id: string
	reason: string | null
	relation: string
	is_deduced: number
}

export type FunctorPropertyAssignment = Replace<
	FunctorPropertyAssignmentDB,
	{ is_deduced: boolean }
>

export type Lemma = {
	id: string
	title: string
	claim: string
	proof: string
}