michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/hott): port Floris' category implementation

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-30 19:56:32 -05:00 committed by Leonardo de Moura
parent 93d5d43f71
commit 5fe8ee606f
6 changed files with 1425 additions and 516 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

79
library/hott/algebra/category/basic.lean Normal file
View file

@ -0,0 +1,79 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import hott.axioms.funext hott.trunc hott.equiv
open path truncation
inductive precategory [class] (ob : Type) : Type :=
mk : Π (hom : ob → ob → Type)
(homH : Π {a b : ob}, is_hset (hom a b))
(comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
(id : Π {a : ob}, hom a a),
(Π ⦃a b c d : ob⦄ {h : hom c d} {g : hom b c} {f : hom a b},
comp h (comp g f) ≈ comp (comp h g) f) →
(Π ⦃a b : ob⦄ {f : hom a b}, comp id f ≈ f) →
(Π ⦃a b : ob⦄ {f : hom a b}, comp f id ≈ f) →
precategory ob
namespace precategory
variables {ob : Type} [C : precategory ob]
variables {a b c d : ob}
include C
definition hom [reducible] : ob → ob → Type := rec (λ hom homH compose id assoc idr idl, hom) C
definition homH [instance] : Π {a b : ob}, is_hset (hom a b) := rec (λ hom homH compose id assoc idr idl, homH) C
-- note: needs to be reducible to typecheck composition in opposite category
definition compose [reducible] : Π {a b c : ob}, hom b c → hom a b → hom a c :=
rec (λ hom homH compose id assoc idr idl, compose) C
definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom homH compose id assoc idr idl, id) C
definition ID [reducible] (a : ob) : hom a a := id
infixr `∘` := compose
infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
theorem assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f :=
rec (λ hom homH comp id assoc idr idl, assoc) C
theorem id_left : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f ≈ f :=
rec (λ hom homH comp id assoc idl idr, idl) C
theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id ≈ f :=
rec (λ hom homH comp id assoc idl idr, idr) C
--the following is the only theorem for which "include C" is necessary if C is a variable (why?)
theorem id_compose (a : ob) : (ID a) ∘ id ≈ id := !id_left
theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f ≈ f) : i ≈ id :=
calc i ≈ i ∘ id : id_right
... ≈ id : H
theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i ≈ f) : i ≈ id :=
calc i ≈ id ∘ i : id_left
... ≈ id : H
end precategory
inductive Precategory : Type := mk : Π (ob : Type), precategory ob → Precategory
namespace precategory
definition Mk {ob} (C) : Precategory := Precategory.mk ob C
definition MK (a b c d e f g h) : Precategory := Precategory.mk a (precategory.mk b c d e f g h)
definition objects [coercion] [reducible] (C : Precategory) : Type
:= Precategory.rec (fun c s, c) C
definition category_instance [instance] [coercion] [reducible] (C : Precategory) : precategory (objects C)
:= Precategory.rec (fun c s, s) C
end precategory
open precategory
theorem Category.equal (C : Precategory) : Precategory.mk C C = C :=
Precategory.rec (λ ob c, rfl) C

355
library/hott/algebra/category/constructions.lean Normal file
View file

@ -0,0 +1,355 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn, Jakob von Raumer
-- This file contains basic constructions on precategories, including common categories
import .natural_transformation
import data.unit data.sigma data.prod data.empty data.bool
open eq eq.ops prod
namespace category
namespace opposite
section
definition opposite {ob : Type} (C : category ob) : category ob :=
mk (λa b, hom b a)
(λ a b c f g, g ∘ f)
(λ a, id)
(λ a b c d f g h, symm !assoc)
(λ a b f, !id_right)
(λ a b f, !id_left)
definition Opposite (C : Category) : Category := Mk (opposite C)
--direct construction:
-- MK C
-- (λa b, hom b a)
-- (λ a b c f g, g ∘ f)
-- (λ a, id)
-- (λ a b c d f g h, symm !assoc)
-- (λ a b f, !id_right)
-- (λ a b f, !id_left)
infixr `∘op`:60 := @compose _ (opposite _) _ _ _
variables {C : Category} {a b c : C}
theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := rfl
theorem op_op' {ob : Type} (C : category ob) : opposite (opposite C) = C :=
category.rec (λ hom comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C
theorem op_op : Opposite (Opposite C) = C :=
(@congr_arg _ _ _ _ (Category.mk C) (op_op' C)) ⬝ !Category.equal
end
end opposite
definition type_category : category Type :=
mk (λa b, a → b)
(λ a b c, function.compose)
(λ a, function.id)
(λ a b c d h g f, symm (function.compose_assoc h g f))
(λ a b f, function.compose_id_left f)
(λ a b f, function.compose_id_right f)
definition Type_category : Category := Mk type_category
section
open decidable unit empty
variables {A : Type} [H : decidable_eq A]
include H
definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
decidable.rec_on
(H b c)
(λ Hbc g, decidable.rec_on
(H a b)
(λ Hab f, rec_on_true (trans Hab Hbc) ⋆)
(λh f, empty.rec _ f) f)
(λh (g : empty), empty.rec _ g) g
omit H
definition discrete_category (A : Type) [H : decidable_eq A] : category A :=
mk (λa b, set_hom a b)
(λ a b c g f, set_compose g f)
(λ a, decidable.rec_on_true rfl ⋆)
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
end
section
open unit bool
definition category_one := discrete_category unit
definition Category_one := Mk category_one
definition category_two := discrete_category bool
definition Category_two := Mk category_two
end
namespace product
section
open prod
definition prod_category {obC obD : Type} (C : category obC) (D : category obD)
: category (obC × obD) :=
mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
(λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
(λ a, (id,id))
(λ a b c d h g f, pair_eq !assoc !assoc )
(λ a b f, prod.equal !id_left !id_left )
(λ a b f, prod.equal !id_right !id_right)
definition Prod_category (C D : Category) : Category := Mk (prod_category C D)
end
end product
namespace ops
notation `type`:max := Type_category
notation 1 := Category_one --it was confusing for me (Floris) that no ``s are needed here
notation 2 := Category_two
postfix `ᵒᵖ`:max := opposite.Opposite
infixr `×c`:30 := product.Prod_category
instance [persistent] type_category category_one
category_two product.prod_category
end ops
open ops
namespace opposite
section
open ops functor
definition opposite_functor {C D : Category} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
@functor.mk (Cᵒᵖ) (Dᵒᵖ)
(λ a, F a)
(λ a b f, F f)
(λ a, !respect_id)
(λ a b c g f, !respect_comp)
end
end opposite
namespace product
section
open ops functor
definition prod_functor {C C' D D' : Category} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a)))
(λ a b f, pair (F (pr1 f)) (G (pr2 f)))
(λ a, pair_eq !respect_id !respect_id)
(λ a b c g f, pair_eq !respect_comp !respect_comp)
end
end product
namespace ops
infixr `×f`:30 := product.prod_functor
infixr `ᵒᵖᶠ`:max := opposite.opposite_functor
end ops
section functor_category
variables (C D : Category)
definition functor_category : category (functor C D) :=
mk (λa b, natural_transformation a b)
(λ a b c g f, natural_transformation.compose g f)
(λ a, natural_transformation.id)
(λ a b c d h g f, !natural_transformation.assoc)
(λ a b f, !natural_transformation.id_left)
(λ a b f, !natural_transformation.id_right)
end functor_category
namespace slice
open sigma function
variables {ob : Type} {C : category ob} {c : ob}
protected definition slice_obs (C : category ob) (c : ob) := Σ(b : ob), hom b c
variables {a b : slice_obs C c}
protected definition to_ob (a : slice_obs C c) : ob := dpr1 a
protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl
protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a
-- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b)
-- (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b :=
-- sigma.equal H₁ H₂
protected definition slice_hom (a b : slice_obs C c) : Type :=
Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a
protected definition hom_hom (f : slice_hom a b) : hom (to_ob a) (to_ob b) := dpr1 f
protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := dpr2 f
-- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g :=
-- sigma.equal H !proof_irrel
definition slice_category (C : category ob) (c : ob) : category (slice_obs C c) :=
mk (λa b, slice_hom a b)
(λ a b c g f, dpair (hom_hom g ∘ hom_hom f)
(show ob_hom c ∘ (hom_hom g ∘ hom_hom f) = ob_hom a,
proof
calc
ob_hom c ∘ (hom_hom g ∘ hom_hom f) = (ob_hom c ∘ hom_hom g) ∘ hom_hom f : !assoc
... = ob_hom b ∘ hom_hom f : {commute g}
... = ob_hom a : {commute f}
qed))
(λ a, dpair id !id_right)
(λ a b c d h g f, dpair_eq !assoc !proof_irrel)
(λ a b f, sigma.equal !id_left !proof_irrel)
(λ a b f, sigma.equal !id_right !proof_irrel)
-- We use !proof_irrel instead of rfl, to give the unifier an easier time
-- definition slice_category {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c)
-- :=
-- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
-- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
-- (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a,
-- proof
-- calc
-- dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc
-- ... = dpr2 b ∘ dpr1 f : {dpr2 g}
-- ... = dpr2 a : {dpr2 f}
-- qed))
-- (λ a, dpair id !id_right)
-- (λ a b c d h g f, dpair_eq !assoc !proof_irrel)
-- (λ a b f, sigma.equal !id_left !proof_irrel)
-- (λ a b f, sigma.equal !id_right !proof_irrel)
-- We use !proof_irrel instead of rfl, to give the unifier an easier time
definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
open category.ops
instance [persistent] slice_category
variables {D : Category}
definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
functor.mk (λ a, to_ob a)
(λ a b f, hom_hom f)
(λ a, rfl)
(λ a b c g f, rfl)
definition postcomposition_functor {x y : D} (h : x ⟶ y)
: Slice_category D x ⇒ Slice_category D y :=
functor.mk (λ a, dpair (to_ob a) (h ∘ ob_hom a))
(λ a b f, dpair (hom_hom f)
(calc
(h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : assoc h (ob_hom b) (hom_hom f)⁻¹
... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
(λ a, rfl)
(λ a b c g f, dpair_eq rfl !proof_irrel)
-- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems
-- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
-- definition heq2.intro {A B : Type} {a : A} {b : B} (H : a == b) : heq2 (heq.type_eq H) a b := H
-- definition heq2.elim {A B : Type} {a : A} {b : B} (H : A = B) (H2 : heq2 H a b) : a == b := H2
-- definition heq2.proof_irrel {A B : Prop} (a : A) (b : B) (H : A = B) : heq2 H a b :=
-- hproof_irrel H a b
-- theorem functor.mk_eq2 {C D : Category} {obF obG : C → D} {homF homG idF idG compF compG}
-- (Hob : ∀x, obF x = obG x)
-- (Hmor : ∀(a b : C) (f : a ⟶ b), heq2 (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f) (homG a b f))
-- : functor.mk obF homF idF compF = functor.mk obG homG idG compG :=
-- hddcongr_arg4 functor.mk
-- (funext Hob)
-- (hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor))))
-- !proof_irrel
-- !proof_irrel
-- set_option pp.implicit true
-- set_option pp.coercions true
-- definition slice_functor : D ⇒ Category_of_categories :=
-- functor.mk (λ a, Category.mk (slice_obs D a) (slice_category D a))
-- (λ a b f, postcomposition_functor f)
-- (λ a, functor.mk_heq
-- (λx, sigma.equal rfl !id_left)
-- (λb c f, sigma.hequal sorry !heq.refl (hproof_irrel sorry _ _)))
-- (λ a b c g f, functor.mk_heq
-- (λx, sigma.equal (sorry ⬝ refl (dpr1 x)) sorry)
-- (λb c f, sorry))
--the error message generated here is really confusing: the type of the above refl should be
-- "@dpr1 D (λ (a_1 : D), a_1 ⟶ a) x = @dpr1 D (λ (a_1 : D), a_1 ⟶ c) x", but the second dpr1 is not even well-typed
end slice
-- section coslice
-- open sigma
-- definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom c b) :=
-- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
-- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
-- (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c,
-- proof
-- calc
-- (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm !assoc
-- ... = dpr1 g ∘ dpr2 b : {dpr2 f}
-- ... = dpr2 c : {dpr2 g}
-- qed))
-- (λ a, dpair id !id_left)
-- (λ a b c d h g f, dpair_eq !assoc !proof_irrel)
-- (λ a b f, sigma.equal !id_left !proof_irrel)
-- (λ a b f, sigma.equal !id_right !proof_irrel)
-- -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) :
-- -- coslice C c = opposite (slice (opposite C) c) :=
-- -- sorry
-- end coslice
section arrow
open sigma eq.ops
-- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob}
-- {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2}
-- {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2)
-- : f3 ∘ (g2 ∘ g1) = (h2 ∘ h1) ∘ f1 :=
-- calc
-- f3 ∘ (g2 ∘ g1) = (f3 ∘ g2) ∘ g1 : assoc
-- ... = (h2 ∘ f2) ∘ g1 : {H2}
-- ... = h2 ∘ (f2 ∘ g1) : symm assoc
-- ... = h2 ∘ (h1 ∘ f1) : {H1}
-- ... = (h2 ∘ h1) ∘ f1 : assoc
-- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), hom a b) :=
-- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)) (h : hom (dpr2' a) (dpr2' b)),
-- dpr3 b ∘ g = h ∘ dpr3 a)
-- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f) (concat_commutative_squares (dpr3 f) (dpr3 g))))
-- (λ a, dpair id (dpair id (id_right ⬝ (symm id_left))))
-- (λ a b c d h g f, dtrip_eq2 assoc assoc !proof_irrel)
-- (λ a b f, trip.equal2 id_left id_left !proof_irrel)
-- (λ a b f, trip.equal2 id_right id_right !proof_irrel)
-- make these definitions private?
variables {ob : Type} {C : category ob}
protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b
variables {a b : arrow_obs ob C}
protected definition src (a : arrow_obs ob C) : ob := dpr1 a
protected definition dst (a : arrow_obs ob C) : ob := dpr2' a
protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := dpr3 a
protected definition arrow_hom (a b : arrow_obs ob C) : Type :=
Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a
protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := dpr1 m
protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := dpr2' m
protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a
:= dpr3 m
definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
mk (λa b, arrow_hom a b)
(λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f)
(show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
proof
calc
to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc
... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g}
... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc
... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f}
... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc
qed)
))
(λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left))))
(λ a b c d h g f, ndtrip_eq !assoc !assoc !proof_irrel)
(λ a b f, ndtrip_equal !id_left !id_left !proof_irrel)
(λ a b f, ndtrip_equal !id_right !id_right !proof_irrel)
end arrow
end category
-- definition foo
-- : category (sorry) :=
-- mk (λa b, sorry)
-- (λ a b c g f, sorry)
-- (λ a, sorry)
-- (λ a b c d h g f, sorry)
-- (λ a b f, sorry)
-- (λ a b f, sorry)

149
library/hott/algebra/category/functor.lean Normal file
View file

@ -0,0 +1,149 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
import .basic
import hott.path
open function
open precategory path heq
inductive functor (C D : Precategory) : Type :=
mk : Π (obF : C → D) (homF : Π(a b : C), hom a b → hom (obF a) (obF b)),
(Π (a : C), homF a a (ID a) ≈ ID (obF a)) →
(Π (a b c : C) {g : hom b c} {f : hom a b}, homF a c (g ∘ f) ≈ homF b c g ∘ homF a b f) →
functor C D
infixl `⇒`:25 := functor
-- I think we only have a precategory of stict catetories.
-- Maybe better implement this using univalence.
namespace functor
variables {C D E : Precategory}
definition object [coercion] (F : functor C D) : C → D := rec (λ obF homF Hid Hcomp, obF) F
definition morphism [coercion] (F : functor C D) : Π⦃a b : C⦄, hom a b → hom (F a) (F b) :=
rec (λ obF homF Hid Hcomp, homF) F
theorem respect_id (F : functor C D) : Π (a : C), F (ID a) ≈ id :=
rec (λ obF homF Hid Hcomp, Hid) F
theorem respect_comp (F : functor C D) : Π ⦃a b c : C⦄ (g : hom b c) (f : hom a b),
F (g ∘ f) ≈ F g ∘ F f :=
rec (λ obF homF Hid Hcomp, Hcomp) F
protected definition compose (G : functor D E) (F : functor C D) : functor C E :=
functor.mk
(λx, G (F x))
(λ a b f, G (F f))
(λ a, calc
G (F (ID a)) ≈ G id : {respect_id F a} --not giving the braces explicitly makes the elaborator compute a couple more seconds
... ≈ id : respect_id G (F a))
(λ a b c g f, calc
G (F (g ∘ f)) ≈ G (F g ∘ F f) : respect_comp F g f
... ≈ G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
infixr `∘f`:60 := compose
/-
protected theorem assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) :
H ∘f (G ∘f F) ≈ (H ∘f G) ∘f F :=
sorry
-/
/-protected definition id {C : Precategory} : functor C C :=
mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
protected definition ID (C : Precategory) : functor C C := id
protected theorem id_left (F : functor C D) : id ∘f F ≈ F :=
functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F
protected theorem id_right (F : functor C D) : F ∘f id ≈ F :=
functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F-/
end functor
/-
namespace category
open functor
definition category_of_categories [reducible] : category Category :=
mk (λ a b, functor a b)
(λ a b c g f, functor.compose g f)
(λ a, functor.id)
(λ a b c d h g f, !functor.assoc)
(λ a b f, !functor.id_left)
(λ a b f, !functor.id_right)
definition Category_of_categories [reducible] := Mk category_of_categories
namespace ops
notation `Cat`:max := Category_of_categories
instance [persistent] category_of_categories
end ops
end category-/
namespace functor
-- open category.ops
-- universes l m
variables {C D : Precategory}
-- check hom C D
-- variables (F : C ⟶ D) (G : D ⇒ C)
-- check G ∘ F
-- check F ∘f G
-- variables (a b : C) (f : a ⟶ b)
-- check F a
-- check F b
-- check F f
-- check G (F f)
-- print "---"
-- -- check (G ∘ F) f --error
-- check (λ(x : functor C C), x) (G ∘ F) f
-- check (G ∘f F) f
-- print "---"
-- -- check (G ∘ F) a --error
-- check (G ∘f F) a
-- print "---"
-- -- check λ(H : hom C D) (x : C), H x --error
-- check λ(H : @hom _ Cat C D) (x : C), H x
-- check λ(H : C ⇒ D) (x : C), H x
-- print "---"
-- -- variables {obF obG : C → D} (Hob : ∀x, obF x = obG x) (homF : Π(a b : C) (f : a ⟶ b), obF a ⟶ obF b) (homG : Π(a b : C) (f : a ⟶ b), obG a ⟶ obG b)
-- -- check eq.rec_on (funext Hob) homF = homG
/-theorem mk_heq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x)
(Hmor : ∀(a b : C) (f : a ⟶ b), homF a b f == homG a b f)
: mk obF homF idF compF = mk obG homG idG compG :=
hddcongr_arg4 mk
(funext Hob)
(hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor))))
!proof_irrel
!proof_irrel
protected theorem hequal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x)
(Hmor : ∀a b (f : a ⟶ b), F f == G f), F = G :=
functor.rec
(λ obF homF idF compF,
functor.rec
(λ obG homG idG compG Hob Hmor, mk_heq Hob Hmor)
G)
F-/
-- theorem mk_eq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x)
-- (Hmor : ∀(a b : C) (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f)
-- = homG a b f)
-- : mk obF homF idF compF = mk obG homG idG compG :=
-- dcongr_arg4 mk
-- (funext Hob)
-- (funext (λ a, funext (λ b, funext (λ f, sorry ⬝ Hmor a b f))))
-- -- to fill this sorry use (a generalization of) cast_pull
-- !proof_irrel
-- !proof_irrel
-- protected theorem equal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x)
-- (Hmor : ∀a b (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (F f) = G f), F = G :=
-- functor.rec
-- (λ obF homF idF compF,
-- functor.rec
-- (λ obG homG idG compG Hob Hmor, mk_eq Hob Hmor)
-- G)
-- F
end functor

267
library/hott/algebra/category/morphism.lean Normal file
View file

@ -0,0 +1,267 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
import .basic
open path precategory
namespace morphism
variables {ob : Type} [C : precategory ob] include C
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
inductive is_section [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f ≈ id → is_section f
inductive is_retraction [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, f ∘ g ≈ id → is_retraction f
inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f ≈ id → f ∘ g ≈ id → is_iso f
definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H
definition section_of (f : a ⟶ b) [H : is_retraction f] : hom b a :=
is_retraction.rec (λg h, g) H
definition inverse (f : a ⟶ b) [H : is_iso f] : hom b a :=
is_iso.rec (λg h1 h2, g) H
postfix `⁻¹` := inverse
theorem inverse_compose (f : a ⟶ b) [H : is_iso f] : f⁻¹ ∘ f ≈ id :=
is_iso.rec (λg h1 h2, h1) H
theorem compose_inverse (f : a ⟶ b) [H : is_iso f] : f ∘ f⁻¹ ≈ id :=
is_iso.rec (λg h1 h2, h2) H
theorem retraction_compose (f : a ⟶ b) [H : is_section f] : retraction_of f ∘ f ≈ id :=
is_section.rec (λg h, h) H
theorem compose_section (f : a ⟶ b) [H : is_retraction f] : f ∘ section_of f ≈ id :=
is_retraction.rec (λg h, h) H
theorem iso_imp_retraction [instance] (f : a ⟶ b) [H : is_iso f] : is_section f :=
is_section.mk !inverse_compose
theorem iso_imp_section [instance] (f : a ⟶ b) [H : is_iso f] : is_retraction f :=
is_retraction.mk !compose_inverse
theorem id_is_iso [instance] : is_iso (ID a) :=
is_iso.mk !id_compose !id_compose
theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) :=
is_iso.mk !compose_inverse !inverse_compose
theorem left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a}
(Hl : g ∘ f ≈ id) (Hr : f ∘ g' ≈ id) : g ≈ g' :=
calc
g ≈ g ∘ id : !id_right
... ≈ g ∘ f ∘ g' : Hr
... ≈ (g ∘ f) ∘ g' : assoc
... ≈ id ∘ g' : Hl
... ≈ g' : id_left
theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ h ≈ id) : retraction_of f ≈ h
:= left_inverse_eq_right_inverse !retraction_compose H2
theorem section_eq_intro [H : is_retraction f] (H2 : h ∘ f ≈ id) : section_of f ≈ h
:= (left_inverse_eq_right_inverse H2 !compose_section)⁻¹
theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h ≈ id) : f⁻¹ ≈ h
:= left_inverse_eq_right_inverse !inverse_compose H2
theorem inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f ≈ id) : f⁻¹ ≈ h
:= (left_inverse_eq_right_inverse H2 !compose_inverse)⁻¹
theorem section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] :
retraction_of f ≈ section_of f :=
retraction_eq_intro !compose_section
theorem section_retraction_imp_iso (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f]
: is_iso f :=
is_iso.mk ((section_eq_retraction f) ▹ (retraction_compose f)) (compose_section f)
theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H ≈ @inverse _ _ _ _ f H' :=
inverse_eq_intro_left !inverse_compose
theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ ≈ f :=
inverse_eq_intro_right !inverse_compose
theorem retraction_of_id : retraction_of (ID a) ≈ id :=
retraction_eq_intro !id_compose
theorem section_of_id : section_of (ID a) ≈ id :=
section_eq_intro !id_compose
theorem iso_of_id : ID a⁻¹ ≈ id :=
inverse_eq_intro_left !id_compose
theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
: is_section (g ∘ f) :=
is_section.mk
(calc
(retraction_of f ∘ retraction_of g) ∘ g ∘ f
≈ retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc _ _ (g ∘ f)
... ≈ retraction_of f ∘ (retraction_of g ∘ g) ∘ f : assoc _ g f
... ≈ retraction_of f ∘ id ∘ f : retraction_compose g
... ≈ retraction_of f ∘ f : id_left f
... ≈ id : retraction_compose)
theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
: is_retraction (g ∘ f) :=
is_retraction.mk
(calc
(g ∘ f) ∘ section_of f ∘ section_of g ≈ g ∘ f ∘ section_of f ∘ section_of g : assoc
... ≈ g ∘ (f ∘ section_of f) ∘ section_of g : assoc f _ _
... ≈ g ∘ id ∘ section_of g : compose_section f
... ≈ g ∘ section_of g : id_left (section_of g)
... ≈ id : compose_section)
theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
!section_retraction_imp_iso
inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) [H : is_iso g], isomorphic a b
/-
namespace isomorphic
open relation
-- should these be coercions?
definition iso [coercion] (H : isomorphic a b) : a ⟶ b :=
isomorphic.rec (λg h, g) H
theorem is_iso [instance] (H : isomorphic a b) : is_iso (isomorphic.iso H) :=
isomorphic.rec (λg h, h) H
infix `≅`:50 := isomorphic
theorem refl (a : ob) : a ≅ a := mk id
theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H))
theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1)
theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
end isomorphic
-/
inductive is_mono [class] (f : a ⟶ b) : Type :=
mk : (∀c (g h : hom c a), f ∘ g ≈ f ∘ h → g ≈ h) → is_mono f
inductive is_epi [class] (f : a ⟶ b) : Type :=
mk : (∀c (g h : hom b c), g ∘ f ≈ h ∘ f → g ≈ h) → is_epi f
theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g ≈ f ∘ h) : g ≈ h
:= is_mono.rec (λH3, H3 c g h H2) H
theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f ≈ h ∘ f) : g ≈ h
:= is_epi.rec (λH3, H3 c g h H2) H
theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f :=
is_mono.mk
(λ c g h H,
calc
g ≈ id ∘ g : id_left
... ≈ (retraction_of f ∘ f) ∘ g : retraction_compose f
... ≈ retraction_of f ∘ f ∘ g : assoc
... ≈ retraction_of f ∘ f ∘ h : H
... ≈ (retraction_of f ∘ f) ∘ h : assoc
... ≈ id ∘ h : retraction_compose f
... ≈ h : id_left)
theorem retraction_is_epi [instance] (f : a ⟶ b) [H : is_retraction f] : is_epi f :=
is_epi.mk
(λ c g h H,
calc
g ≈ g ∘ id : id_right
... ≈ g ∘ f ∘ section_of f : compose_section f
... ≈ (g ∘ f) ∘ section_of f : assoc
... ≈ (h ∘ f) ∘ section_of f : H
... ≈ h ∘ f ∘ section_of f : assoc
... ≈ h ∘ id : compose_section f
... ≈ h : id_right)
--these theorems are now proven automatically using type classes
--should they be instances?
theorem id_is_mono : is_mono (ID a)
theorem id_is_epi : is_epi (ID a)
theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) :=
is_mono.mk
(λ d h₁ h₂ H,
have H2 : g ∘ (f ∘ h₁) ≈ g ∘ (f ∘ h₂), from (assoc g f h₁)⁻¹ ▹ (assoc g f h₂)⁻¹ ▹ H,
mono_elim (mono_elim H2))
theorem composition_is_epi [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi (g ∘ f) :=
is_epi.mk
(λ d h₁ h₂ H,
have H2 : (h₁ ∘ g) ∘ f ≈ (h₂ ∘ g) ∘ f, from assoc h₁ g f ▹ assoc h₂ g f ▹ H,
epi_elim (epi_elim H2))
end morphism
namespace morphism
--rewrite lemmas for inverses, modified from
--https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v
namespace iso
section
variables {ob : Type} [C : precategory ob] include C
variables {a b c d : ob} (f : b ⟶ a)
(r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b)
(g : d ⟶ c)
variable [Hq : is_iso q] include Hq
theorem compose_pV : q ∘ q⁻¹ ≈ id := !compose_inverse
theorem compose_Vp : q⁻¹ ∘ q ≈ id := !inverse_compose
theorem compose_V_pp : q⁻¹ ∘ (q ∘ p) ≈ p :=
calc
q⁻¹ ∘ (q ∘ p) ≈ (q⁻¹ ∘ q) ∘ p : assoc (q⁻¹) q p
... ≈ id ∘ p : inverse_compose q
... ≈ p : id_left p
theorem compose_p_Vp : q ∘ (q⁻¹ ∘ g) ≈ g :=
calc
q ∘ (q⁻¹ ∘ g) ≈ (q ∘ q⁻¹) ∘ g : assoc q (q⁻¹) g
... ≈ id ∘ g : compose_inverse q
... ≈ g : id_left g
theorem compose_pp_V : (r ∘ q) ∘ q⁻¹ ≈ r :=
calc
(r ∘ q) ∘ q⁻¹ ≈ r ∘ q ∘ q⁻¹ : assoc r q (q⁻¹)⁻¹
... ≈ r ∘ id : compose_inverse q
... ≈ r : id_right r
theorem compose_pV_p : (f ∘ q⁻¹) ∘ q ≈ f :=
calc
(f ∘ q⁻¹) ∘ q ≈ f ∘ q⁻¹ ∘ q : assoc f (q⁻¹) q⁻¹
... ≈ f ∘ id : inverse_compose q
... ≈ f : id_right f
theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ ≈ p⁻¹ ∘ q⁻¹ :=
have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p ≈ p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹,
have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) ≈ p⁻¹ ∘ p, from ap _ (compose_V_pp q p),
have H3 : p⁻¹ ∘ p ≈ id, from inverse_compose p,
inverse_eq_intro_left (H1 ⬝ H2 ⬝ H3)
--the proof using calc is hard for the unifier (needs ~90k steps)
-- inverse_eq_intro_left
-- (calc
-- (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹
-- ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p)
-- ... = id : inverse_compose p)
theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ ≈ g⁻¹ ∘ q := inverse_involutive q ▹ inv_pp (q⁻¹) g
theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ ≈ f ∘ q⁻¹ := inverse_involutive f ▹ inv_pp q (f⁻¹)
theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ ≈ r ∘ q := inverse_involutive r ▹ inv_Vp q (r⁻¹)
end
section
variables {ob : Type} {C : precategory ob} include C
variables {d c b a : ob}
{i : b ⟶ c} {f : b ⟶ a}
{r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b}
{g : d ⟶ c} {h : c ⟶ b}
{x : b ⟶ d} {z : a ⟶ c}
{y : d ⟶ b} {w : c ⟶ a}
variable [Hq : is_iso q] include Hq
theorem moveR_Mp (H : y ≈ q⁻¹ ∘ g) : q ∘ y ≈ g := H⁻¹ ▹ compose_p_Vp q g
theorem moveR_pM (H : w ≈ f ∘ q⁻¹) : w ∘ q ≈ f := H⁻¹ ▹ compose_pV_p f q
theorem moveR_Vp (H : z ≈ q ∘ p) : q⁻¹ ∘ z ≈ p := H⁻¹ ▹ compose_V_pp q p
theorem moveR_pV (H : x ≈ r ∘ q) : x ∘ q⁻¹ ≈ r := H⁻¹ ▹ compose_pp_V r q
theorem moveL_Mp (H : q⁻¹ ∘ g ≈ y) : g ≈ q ∘ y := moveR_Mp (H⁻¹)⁻¹
theorem moveL_pM (H : f ∘ q⁻¹ ≈ w) : f ≈ w ∘ q := moveR_pM (H⁻¹)⁻¹
theorem moveL_Vp (H : q ∘ p ≈ z) : p ≈ q⁻¹ ∘ z := moveR_Vp (H⁻¹)⁻¹
theorem moveL_pV (H : r ∘ q ≈ x) : r ≈ x ∘ q⁻¹ := moveR_pV (H⁻¹)⁻¹
theorem moveL_1V (H : h ∘ q ≈ id) : h ≈ q⁻¹ := inverse_eq_intro_left H⁻¹
theorem moveL_V1 (H : q ∘ h ≈ id) : h ≈ q⁻¹ := inverse_eq_intro_right H⁻¹
theorem moveL_1M (H : i ∘ q⁻¹ ≈ id) : i ≈ q := moveL_1V H ⬝ inverse_involutive q
theorem moveL_M1 (H : q⁻¹ ∘ i ≈ id) : i ≈ q := moveL_V1 H ⬝ inverse_involutive q
theorem moveR_1M (H : id ≈ i ∘ q⁻¹) : q ≈ i := moveL_1M (H⁻¹)⁻¹
theorem moveR_M1 (H : id ≈ q⁻¹ ∘ i) : q ≈ i := moveL_M1 (H⁻¹)⁻¹
theorem moveR_1V (H : id ≈ h ∘ q) : q⁻¹ ≈ h := moveL_1V (H⁻¹)⁻¹
theorem moveR_V1 (H : id ≈ q ∘ h) : q⁻¹ ≈ h := moveL_V1 (H⁻¹)⁻¹
end
end iso
end morphism

54
library/hott/algebra/category/natural_transformation.lean Normal file
View file

@ -0,0 +1,54 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn, Jakob von Raumer
import .functor hott.axioms.funext
open precategory path functor
inductive natural_transformation {C D : Precategory} (F G : C ⇒ D) : Type :=
mk : Π (η : Π (a : C), hom (F a) (G a))
(nat : Π {a b : C} (f : hom a b), G f ∘ η a ≈ η b ∘ F f),
natural_transformation F G
infixl `⟹`:25 := natural_transformation -- \==>
namespace natural_transformation
variables {C D : Precategory} {F G H I : functor C D}
definition natural_map [coercion] (η : F ⟹ G) : Π(a : C), F a ⟶ G a :=
rec (λ x y, x) η
theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a ≈ η b ∘ F f :=
rec (λ x y, y) η
protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
natural_transformation.mk
(λ a, η a ∘ θ a)
(λ a b f,
calc
H f ∘ (η a ∘ θ a) ≈ (H f ∘ η a) ∘ θ a : assoc
... ≈(η b ∘ G f) ∘ θ a : naturality η f
... ≈ η b ∘ (G f ∘ θ a) : assoc
... ≈ η b ∘ (θ b ∘ F f) : naturality θ f
... ≈ (η b ∘ θ b) ∘ F f : assoc)
--congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24)
infixr `∘n`:60 := compose
definition foo (C : Precategory) (a b : C) (f g : hom a b) (p q : f ≈ g) : p ≈ q :=
@truncation.is_hset.elim _ !homH f g p q
protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext : funext.{l_1 l_4}] :
η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ :=
dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) sorry
protected definition id {C D : Precategory} {F : functor C D} : natural_transformation F F :=
mk (λa, id) (λa b f, !id_right ⬝ (!id_left⁻¹))
protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F := id
protected theorem id_left (η : F ⟹ G) [fext : funext] : natural_transformation.compose id η ≈ η :=
rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_left)) sorry) η
protected theorem id_right (η : F ⟹ G) [fext : funext] : natural_transformation.compose η id ≈ η :=
rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_right)) sorry) η
end natural_transformation

1037
library/hott/path.lean
View file

File diff suppressed because it is too large Load diff