-
Notifications
You must be signed in to change notification settings - Fork 1
/
README.agda
86 lines (57 loc) · 2.03 KB
/
README.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
module README where
-- Utilities
-- =========
-- standard library for directed containers
open import Utils
-- Basic Category Theory
-- =====================
-- functors, natural transformations
open import Functors
-- comonads, comonad morphisms
open import Comonads
-- Containers
-- ==========
-- containers, container morphisms, interpretation to functors and natural transformations, fully-faithfulness lemmas
open import Containers
-- Directed Containers
-- ===================
-- directed containers, directed container morphisms
open import DContainers
-- interpretation to comonads and comonad morphisms
open import DContainerExt
-- strict directed containers
open import StrictDirectedContainer
-- coproducts, functions from monoids to strict directed containers
open import DirectedContainerOperations
-- Directed Containers And Comonads
-- ===============================
-- containers ∩ comonads = directed containers
open import Comonad2DContainer
open import Comonad2DContainerHelper
open import Comonad2DContainerHelper2
open import Comonad2DContainerHelper3
-- containers ∩ comonad morphisms = directed container morphisms
open import ComonadMorph2DContainerMorph
open import ComonadMorph2DContainerMorphHelper
-- fully faithfulness of the interpretation to comonads
open import FullyFaithfulLem1
open import FullyFaithfulLem2
-- lemmas for interpretation to comonads
open import InterpretQuoteLem1
open import InterpretQuoteLem2
-- Examples
-- ========
-- lists as containers
open import Examples.ListContainer
-- different flavours of binary trees as directed containers
open import Examples.BinaryTreeDContainer1
open import Examples.BinaryTreeDContainer2
open import Examples.BinaryTreeDContainer3
-- lists as directed containers
open import Examples.ListDContainer
-- streams as directed containers
open import Examples.StreamDContainer
-- directed container morphisms between lists, streams and trees
open import Examples.Morphisms
-- focussing a container to get a directed container
open import Examples.FocusDContainer