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 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
|
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Tactics.
Global Set Primitive Projections.
Global Set Universe Polymorphism.
Global Unset Universe Minimization ToSet.
Class Category : Type :=
{
Obj : Type;
Hom : Obj -> Obj -> Type;
compose : forall {a b c : Obj}, (Hom a b) -> (Hom b c) -> (Hom a c);
id : forall {a : Obj}, Hom a a;
}.
Arguments Obj {_}, _.
Arguments id {_ _}, {_} _, _ _.
Arguments Hom {_} _ _, _ _ _.
Arguments compose {_} {_ _ _} _ _, _ {_ _ _} _ _, _ _ _ _ _ _.
Coercion Obj : Category >-> Sortclass.
Definition Opposite (C : Category) : Category :=
{|
Obj := Obj C;
Hom := fun a b => Hom b a;
compose :=
fun a b c (f : Hom b a) (g : Hom c b) => compose C c b a g f;
id := fun c => id C c;
|}.
Record Functor (C C' : Category) : Type :=
{
FO : C -> C';
FA : forall {a b}, Hom a b -> Hom (FO a) (FO b);
}.
Arguments FO {_ _} _ _.
Arguments FA {_ _} _ {_ _} _, {_ _} _ _ _ _.
Section Opposite_Functor.
Context {C D : Category} (F : Functor C D).
Program Definition Opposite_Functor : (Functor (Opposite C) (Opposite D)) :=
{|
FO := FO F;
FA := fun _ _ h => FA F h;
|}.
End Opposite_Functor.
Section Functor_Compose.
Context {C C' C'' : Category} (F : Functor C C') (F' : Functor C' C'').
Program Definition Functor_compose : Functor C C'' :=
{|
FO := fun c => FO F' (FO F c);
FA := fun c d f => FA F' (FA F f)
|}.
End Functor_Compose.
Section Algebras.
Context {C : Category} (T : Functor C C).
Record Algebra : Type :=
{
Alg_Carrier : C;
Constructors : Hom (FO T Alg_Carrier) Alg_Carrier
}.
Record Algebra_Hom (alg alg' : Algebra) : Type :=
{
Alg_map : Hom (Alg_Carrier alg) (Alg_Carrier alg');
Alg_map_com : compose (FA T Alg_map) (Constructors alg')
= compose (Constructors alg) Alg_map
}.
Arguments Alg_map {_ _} _.
Arguments Alg_map_com {_ _} _.
Program Definition Algebra_Hom_compose
{alg alg' alg'' : Algebra}
(h : Algebra_Hom alg alg')
(h' : Algebra_Hom alg' alg'')
: Algebra_Hom alg alg''
:=
{|
Alg_map := compose (Alg_map h) (Alg_map h')
|}.
Next Obligation. Proof. Admitted.
Lemma Algebra_Hom_eq_simplify (alg alg' : Algebra)
(ah ah' : Algebra_Hom alg alg')
: (Alg_map ah) = (Alg_map ah') -> ah = ah'.
Proof. Admitted.
Program Definition Algebra_Hom_id (alg : Algebra) : Algebra_Hom alg alg :=
{|
Alg_map := id
|}.
Next Obligation. Admitted.
Definition Algebra_Cat : Category :=
{|
Obj := Algebra;
Hom := Algebra_Hom;
compose := @Algebra_Hom_compose;
id := Algebra_Hom_id;
|}.
End Algebras.
Arguments Alg_Carrier {_ _} _.
Arguments Constructors {_ _} _.
Arguments Algebra_Hom {_ _} _ _.
Arguments Alg_map {_ _ _ _} _.
Arguments Alg_map_com {_ _ _ _} _.
Arguments Algebra_Hom_id {_ _} _.
Section CoAlgebras.
Context {C : Category}.
Definition CoAlgebra (T : Functor C C) :=
@Algebra (Opposite C) (Opposite_Functor T).
Definition CoAlgebra_Hom {T : Functor C C} :=
@Algebra_Hom (Opposite C) (Opposite_Functor T).
Definition CoAlgebra_Hom_id {T : Functor C C} :=
@Algebra_Hom_id (Opposite C) (Opposite_Functor T).
Definition CoAlgebra_Cat (T : Functor C C) :=
@Algebra_Cat (Opposite C) (Opposite_Functor T).
End CoAlgebras.
Program Definition Type_Cat : Category :=
{|
Obj := Type;
Hom := (fun A B => A -> B);
compose := fun A B C (g : A -> B) (h : B -> C) => fun (x : A) => h (g x);
id := fun A => fun x => x
|}.
Local Obligation Tactic := idtac.
Program Definition Prod_Cat (C C' : Category) : Category :=
{|
Obj := C * C';
Hom :=
fun a b =>
((Hom (fst a) (fst b)) * (Hom (snd a) (snd b)))%type;
compose :=
fun a b c f g =>
((compose (fst f) (fst g)), (compose (snd f)(snd g)));
id := fun c => (id, id)
|}.
Class Terminal (C : Category) : Type :=
{
terminal : C;
t_morph : forall (d : Obj), Hom d terminal;
t_morph_unique : forall (d : Obj) (f g : (Hom d terminal)), f = g
}.
Arguments terminal {_} _.
Arguments t_morph {_} _ _.
Arguments t_morph_unique {_} _ _ _ _.
Coercion terminal : Terminal >-> Obj.
Definition Initial (C : Category) := Terminal (Opposite C).
Existing Class Initial.
Record Product {C : Category} (c d : C) : Type :=
{
product : C;
Pi_1 : Hom product c;
Pi_2 : Hom product d;
Prod_morph_ex : forall (p' : Obj) (r1 : Hom p' c) (r2 : Hom p' d), (Hom p' product);
}.
Arguments Product _ _ _, {_} _ _.
Arguments Pi_1 {_ _ _ _}, {_ _ _} _.
Arguments Pi_2 {_ _ _ _}, {_ _ _} _.
Arguments Prod_morph_ex {_ _ _} _ _ _ _.
Coercion product : Product >-> Obj.
Definition Has_Products (C : Category) : Type := forall a b, Product a b.
Existing Class Has_Products.
Program Definition Prod_Func (C : Category) {HP : Has_Products C}
: Functor (Prod_Cat C C) C :=
{|
FO := fun x => HP (fst x) (snd x);
FA := fun a b f => Prod_morph_ex _ _ (compose Pi_1 (fst f)) (compose Pi_2 (snd f))
|}.
Arguments Prod_Func _ _, _ {_}.
Definition Sum (C : Category) := @Product (Opposite C).
Arguments Sum _ _ _, {_} _ _.
Definition Has_Sums (C : Category) : Type := forall (a b : C), (Sum a b).
Existing Class Has_Sums.
Program Definition sum_Sum (A B : Type) : (@Sum Type_Cat A B) :=
{|
product := (A + B)%type;
Prod_morph_ex :=
fun (p' : Type)
(r1 : A -> p')
(r2 : B -> p')
(X : A + B) =>
match X return p' with
| inl a => r1 a
| inr b => r2 b
end
|}.
Next Obligation. simpl; auto. Defined.
Next Obligation. simpl; auto. Defined.
#[export] Program Instance Type_Cat_Has_Sums : Has_Sums Type_Cat := sum_Sum.
Definition Sum_Func {C : Category} {HS : Has_Sums C} :
Functor (Prod_Cat C C) C := Opposite_Functor (Prod_Func (Opposite C) HS).
Arguments Sum_Func _ _, _ {_}.
#[export] Program Instance unit_Type_term : Terminal Type_Cat :=
{
terminal := unit;
t_morph := fun _ _=> tt
}.
Next Obligation. Proof. Admitted.
Program Definition term_id : Functor Type_Cat (Prod_Cat Type_Cat Type_Cat) :=
{|
FO := fun a => (@terminal Type_Cat _, a);
FA := fun a b f => (@id _ (@terminal Type_Cat _), f)
|}.
Definition S_nat_func : Functor Type_Cat Type_Cat :=
Functor_compose term_id (Sum_Func Type_Cat _).
Definition S_nat_alg_cat := Algebra_Cat S_nat_func.
CoInductive CoNat : Set :=
| CoO : CoNat
| CoS : CoNat -> CoNat
.
Definition S_nat_coalg_cat := @CoAlgebra_Cat Type_Cat S_nat_func.
Set Printing Universes.
Program Definition CoNat_alg_term : Initial S_nat_coalg_cat :=
{|
terminal := _;
t_morph := _
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Axiom Admit : False.
Next Obligation.
Proof.
intros d f g.
assert(H1 := (@Alg_map_com _ _ _ _ f)). clear.
assert (inl tt = inr tt) by (exfalso; apply Admit).
discriminate.
all: exfalso; apply Admit.
Show Universes.
Qed.
|