-
Notifications
You must be signed in to change notification settings - Fork 2
/
Everything.agda
71 lines (62 loc) · 1.83 KB
/
Everything.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
module Everything where
-- basic utilities
open import Library
open import Isomorphism
-- basic category theory
open import Categories
open import Categories.Sets
open import Categories.Families
open import Categories.Initial
open import Categories.Terminal
open import Categories.CoProducts
open import Categories.PushOuts
open import Categories.Setoids -- should be replaced by standard libary def
open import Functors
open import Functors.Fin
open import Functors.FullyFaithful
open import Naturals
-- basic examples
open import Monoids
open import FunctorCat
-- ordinary monads
open import Monads
open import Monads.MonadMorphs
open import Adjunctions
open import Adjunctions.Adj2Mon
open import Monads.Kleisli
open import Monads.Kleisli.Functors
open import Monads.Kleisli.Adjunction
open import Monads.EM
open import Monads.EM.Functors
open import Monads.EM.Adjunction
open import Monads.CatofAdj
open import Monads.CatofAdj.InitAdj
open import Monads.CatofAdj.TermAdjObj
open import Monads.CatofAdj.TermAdjHom
open import Monads.CatofAdj.TermAdjUniq
open import Monads.CatofAdj.TermAdj
-- relative monads
open import RMonads
open import RMonads.RMonadMorphs
open import RAdjunctions
open import RAdjunctions.RAdj2RMon
open import RMonads.REM
open import RMonads.REM.Functors
open import RMonads.REM.Adjunction
open import RMonads.RKleisli
open import RMonads.RKleisli.Functors
open import RMonads.RKleisli.Adjunction
open import RMonads.Restriction
open import RMonads.SpecialCase
open import RMonads.CatofRAdj
open import RMonads.CatofRAdj.InitRAdj
open import RMonads.CatofRAdj.TermRAdjObj
open import RMonads.CatofRAdj.TermRAdjHom
open import RMonads.CatofRAdj.TermRAdj
open import RMonads.Modules
-- rmonad examples
open import WellScopedTerms
open import WellScopedTermsModel
open import WellTypedTerms
open import WellTypedTermsModel
open import Lawvere