annotate free-monoid.agda @ 155:d9cbaa749be6

Monoids done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Aug 2013 21:30:00 +0900
parents 744be443e232
children b15c1435cfcc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
155
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
1 -- {-# OPTIONS --universe-polymorphism #-}
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
2
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category -- https://github.com/konn/category-agda
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Level
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 module free-monoid { c c₁ c₂ ℓ : Level } where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Category.Sets
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Category.Cat
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import HomReasoning
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import cat-utility
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Binary.Core
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary.PropositionalEquality
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 A = Sets {c₁}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 B = CAT
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 infixr 40 _::_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 data List (A : Set ) : Set where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 [] : List A
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 _::_ : A -> List A -> List A
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 infixl 30 _++_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 _++_ : {A : Set } -> List A -> List A -> List A
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 [] ++ ys = ys
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 (x :: xs) ++ ys = x :: (xs ++ ys)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 data ListObj : Set where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * : ListObj
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 ≡-cong = Relation.Binary.PropositionalEquality.cong
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_ _++_ []
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 isListCategory A = record { isEquivalence = isEquivalence1 {A}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ; identityL = list-id-l
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ; identityR = list-id-r
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ; o-resp-≈ = o-resp-≈ {A}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 list-id-l : { A : Set } -> { x : List A } -> [] ++ x ≡ x
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 list-id-l {_} {_} = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 list-id-r : { A : Set } -> { x : List A } -> x ++ [] ≡ x
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 list-id-r {_} {[]} = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 list-id-r {A} {x :: xs} = ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 list-assoc : {A : Set} -> { xs ys zs : List A } ->
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 list-assoc {_} {[]} {_} {_} = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( \y -> x :: y )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 ( list-assoc {A} {xs} {ys} {zs} )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 o-resp-≈ : {A : Set} -> {f g : List A } → {h i : List A } →
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 o-resp-≈ {A} refl refl = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A } _≡_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 isEquivalence1 {A} = -- this is the same function as A's equivalence but has different types
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 record { refl = refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ; sym = sym
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ; trans = trans
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ListCategory : (A : Set) -> Category _ _ _
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 ListCategory A =
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 record { Obj = ListObj
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 ; Hom = \a b -> List A
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 ; _o_ = _++_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 ; _≈_ = _≡_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ; Id = []
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ; isCategory = ( isListCategory A )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 open import Algebra.FunctionProperties using (Op₁; Op₂)
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 open import Algebra.Structures
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 record ≡-Monoid : Set (suc c) where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 infixl 7 _∙_
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 field
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 Carrier : Set c
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 _∙_ : Op₂ Carrier
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 ε : Carrier
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 isMonoid : IsMonoid _≡_ _∙_ ε
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 open ≡-Monoid
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 field
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 morph : Carrier a -> Carrier b
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 identity : morph (ε a) ≡ ε b
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 mdistr : ∀{x y} -> morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 open Monomorph
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
155
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
93 _+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
94 _+_ {a} {b} {c} f g = record {
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 morph = \x -> morph f ( morph g x ) ;
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 identity = identity1 ;
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 mdistr = mdistr1
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 } where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 identity1 : morph f ( morph g (ε a) ) ≡ ε c
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 -- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 -- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 mdistr1 : ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 -- ∀{x y} -> morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 -- ∀{x y} -> morph f ( ( _∙_ c (morph g x )) (morph g y) ) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 mdistr1 = trans (≡-cong (morph f ) ( mdistr g) ) ( mdistr f )
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
155
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
108 M-id : { a : ≡-Monoid } -> Monomorph a a
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
109 M-id = record { morph = \x -> x ; identity = refl ; mdistr = refl }
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
155
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
111 _==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
112 _==_ f g = morph f ≡ morph g
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
113
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
114 isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id)
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
115 isMonoidCategory = record { isEquivalence = isEquivalence1
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
116 ; identityL = refl
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
117 ; identityR = refl
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
118 ; associative = refl
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
119 ; o-resp-≈ = \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
120 }
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
121 where
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
122 o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } →
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
123 f == g → h == i → (h + f) == (i + g)
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
124 o-resp-≈ {A} refl refl = refl
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
125 isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b} _==_
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
126 isEquivalence1 = -- this is the same function as A's equivalence but has different types
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
127 record { refl = refl
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
128 ; sym = sym
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
129 ; trans = trans
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
130 }
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
131 MonoidCategory : Category _ _ _
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
132 MonoidCategory =
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
133 record { Obj = ≡-Monoid
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
134 ; Hom = Monomorph
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
135 ; _o_ = _+_
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
136 ; _≈_ = _==_
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
137 ; Id = M-id
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
138 ; isCategory = isMonoidCategory
d9cbaa749be6 Monoids done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 154
diff changeset
139 }
154
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 -- open Functor
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 -- U : Functor B A
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 -- U = record {
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 -- FObj = \c -> Obj c ;
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 -- FMap = \f -> (\x -> FMap f x) ;
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 -- isFunctor = record {
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 -- ≈-cong = ≈-cong
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 -- ; identity = identity1
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 -- ; distr = distr1
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 -- }
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 -- } where
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 -- identity1 : {a : Obj B} → A [ FMap identityFunctor ≈ ( \x -> x ) ]
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 -- identity1 {a} = _≡_.refl
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 -- ≈-cong : {a b : Obj B} {f g : Hom B a b} → B [ f ≈ g ] → ?
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 -- ≈-cong {a} {b} {f} {g} = ?
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 -- distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → A [ ( FMap ( g ○ f )) ≈ ( \x -> FMap g (FMap f x )) ]
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 -- distr1 {a} {b} {c} {f} {g} = ?
744be443e232 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162