feat(library): changes in eq.lean sigma.lean and category.lean
in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5 in sigma.lean, finish proving equality of triples in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator
This commit is contained in:
Floris van Doorn
parent
05fb3aa060
commit
3a95734fae
3 changed files with 285 additions and 141 deletions
|
|
@ -8,7 +8,7 @@ import data.unit data.sigma data.prod
|
|||
import algebra.function
|
||||
import logic.axioms.funext
|
||||
|
||||
open eq
|
||||
open eq eq_ops
|
||||
|
||||
inductive category [class] (ob : Type) : Type :=
|
||||
mk : Π (mor : ob → ob → Type) (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
|
||||
|
|
@ -37,6 +37,7 @@ namespace category
|
|||
|
||||
precedence `∘` : 60
|
||||
infixr `∘` := compose
|
||||
infixl `=>`:25 := mor
|
||||
|
||||
theorem assoc : Π {A B C D : ob} {h : mor C D} {g : mor B C} {f : mor A B},
|
||||
h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
|
||||
|
|
@ -52,7 +53,7 @@ namespace category
|
|||
|
||||
theorem left_id_unique (i : mor A A) (H : Π{B} {f : mor B A}, i ∘ f = f) : i = id :=
|
||||
calc
|
||||
i = i ∘ id : eq.symm id_right
|
||||
i = i ∘ id : symm id_right
|
||||
... = id : H
|
||||
|
||||
theorem right_id_unique (i : mor A A) (H : Π{B} {f : mor A B}, f ∘ i = f) : i = id :=
|
||||
|
|
@ -193,42 +194,6 @@ namespace category
|
|||
|
||||
end
|
||||
|
||||
section
|
||||
open unit
|
||||
definition one [instance] : category unit :=
|
||||
category.mk (λa b, unit) (λ a b c f g, star) (λ a, star) (λ a b c d f g h, unit.equal _ _)
|
||||
(λ a b f, unit.equal _ _) (λ a b f, unit.equal _ _)
|
||||
end
|
||||
|
||||
section
|
||||
parameter {ob : Type}
|
||||
definition opposite (C : category ob) : category ob :=
|
||||
category.mk (λa b, mor 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)
|
||||
precedence `∘op` : 60
|
||||
infixr `∘op` := @compose _ (opposite _) _ _ _
|
||||
|
||||
parameters {C : category ob} {a b c : ob}
|
||||
|
||||
theorem compose_op {f : @mor ob C a b} {g : mor b c} : f ∘op g = g ∘ f :=
|
||||
rfl
|
||||
|
||||
theorem op_op {C : category ob} : opposite (opposite C) = C :=
|
||||
rec (λ mor comp id assoc idl idr, rfl) C
|
||||
|
||||
end
|
||||
|
||||
definition Opposite (C : Category) : Category :=
|
||||
Category.mk (objects C) (opposite (category_instance C))
|
||||
|
||||
|
||||
section
|
||||
--need extensionality
|
||||
-- definition type_cat : category Type :=
|
||||
-- mk (λA B, A → B) (λ a b c f g, function.compose f g) (λ a, function.id) (λ a b c d f g h, sorry)
|
||||
-- (λ a b f, sorry) (λ a b f, sorry)
|
||||
end
|
||||
|
||||
end category
|
||||
|
||||
open category
|
||||
|
|
@ -262,7 +227,7 @@ namespace functor
|
|||
|
||||
section category_functor
|
||||
|
||||
definition compose {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
|
||||
protected definition compose {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
|
||||
(G : D ⇒ E) (F : C ⇒ D) : C ⇒ E :=
|
||||
functor.mk C E
|
||||
(λx, G (F x))
|
||||
|
|
@ -277,34 +242,23 @@ namespace functor
|
|||
precedence `∘∘` : 60
|
||||
infixr `∘∘` := compose
|
||||
|
||||
-- theorem congr_functor {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
|
||||
-- {m m' : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
|
||||
-- (Hm : ∀{a b : obC} {f : mor a b}, m f = m' f)
|
||||
-- : functor.mk C D o m i c = functor.mk C D o m' i' c' :=
|
||||
-- sorry
|
||||
|
||||
-- theorem congr_functor_refl {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
|
||||
-- {m : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
|
||||
-- : functor.mk C D o m i c = functor.mk C D o m i' c' :=
|
||||
-- rfl
|
||||
|
||||
theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
|
||||
{C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
|
||||
protected theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
|
||||
{C : category obC} {D : category obD} {H : C ⇒ D} {G : B ⇒ C} {F : A ⇒ B} :
|
||||
H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
|
||||
rfl
|
||||
|
||||
-- later check whether we want implicit or explicit arguments here. For the moment, define both
|
||||
definition id {ob : Type} {C : category ob} : functor C C :=
|
||||
protected definition id {ob : Type} {C : category ob} : functor C C :=
|
||||
mk C C (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
|
||||
definition ID {ob : Type} (C : category ob) : functor C C := id
|
||||
definition Id {C : Category} : Functor C C := Functor.mk id
|
||||
definition iD (C : Category) : Functor C C := Functor.mk id
|
||||
protected definition ID {ob : Type} (C : category ob) : functor C C := id
|
||||
protected definition Id {C : Category} : Functor C C := Functor.mk id
|
||||
protected definition iD (C : Category) : Functor C C := Functor.mk id
|
||||
|
||||
theorem id_left {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
|
||||
protected theorem id_left {obC obB : Type} {B : category obB} {C : category obC} {F : B ⇒ C}
|
||||
: id ∘∘ F = F :=
|
||||
rec (λ obF morF idF compF, rfl) F
|
||||
|
||||
theorem id_right {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
|
||||
protected theorem id_right {obC obB : Type} {B : category obB} {C : category obC} {F : B ⇒ C}
|
||||
: F ∘∘ id = F :=
|
||||
rec (λ obF morF idF compF, rfl) F
|
||||
|
||||
|
|
@ -315,7 +269,7 @@ namespace functor
|
|||
definition Functor_functor {C D : Category} (F : Functor C D) : functor (category_instance C) (category_instance D) :=
|
||||
Functor.rec (λ x, x) F
|
||||
|
||||
definition Compose {C D E : Category} (G : Functor D E) (F : Functor C D) : Functor C E :=
|
||||
protected definition Compose {C D E : Category} (G : Functor D E) (F : Functor C D) : Functor C E :=
|
||||
Functor.mk (compose (Functor_functor G) (Functor_functor F))
|
||||
|
||||
-- namespace Functor
|
||||
|
|
@ -323,17 +277,17 @@ namespace functor
|
|||
infixr `∘∘` := Compose
|
||||
-- end Functor
|
||||
|
||||
definition Assoc {A B C D : Category} (H : Functor C D) (G : Functor B C) (F : Functor A B)
|
||||
protected definition Assoc {A B C D : Category} {H : Functor C D} {G : Functor B C} {F : Functor A B}
|
||||
: H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
|
||||
rfl
|
||||
|
||||
theorem Id_left {B : Category} {C : Category} (F : Functor B C)
|
||||
protected theorem Id_left {B : Category} {C : Category} {F : Functor B C}
|
||||
: Id ∘∘ F = F :=
|
||||
Functor.rec (λ f, subst (id_left f) rfl) F
|
||||
Functor.rec (λ f, subst id_left rfl) F
|
||||
|
||||
theorem Id_right {B : Category} {C : Category} (F : Functor B C)
|
||||
protected theorem Id_right {B : Category} {C : Category} {F : Functor B C}
|
||||
: F ∘∘ Id = F :=
|
||||
Functor.rec (λ f, subst (id_right f) rfl) F
|
||||
Functor.rec (λ f, subst id_right rfl) F
|
||||
|
||||
end Functor
|
||||
|
||||
|
|
@ -343,56 +297,161 @@ open functor
|
|||
|
||||
inductive natural_transformation {obC obD : Type} {C : category obC} {D : category obD}
|
||||
(F G : functor C D) : Type :=
|
||||
mk : Π (η : Π(a : obC), mor (object F a) (object G a)), Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f
|
||||
mk : Π (η : Π(a : obC), mor (object F a) (object G a)), (Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f)
|
||||
→ natural_transformation F G
|
||||
|
||||
inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
|
||||
mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
|
||||
-- inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
|
||||
-- mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
|
||||
|
||||
namespace natural_tranformation
|
||||
infixl `==>`:25 := natural_transformation
|
||||
|
||||
-- todo
|
||||
namespace natural_transformation
|
||||
section
|
||||
parameters {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
|
||||
|
||||
end natural_tranformation
|
||||
definition natural_map [coercion] (η : F ==> G) :
|
||||
Π(a : obC), mor (object F a) (object G a) :=
|
||||
rec (λ x y, x) η
|
||||
|
||||
definition naturality (η : F ==> G) :
|
||||
Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f :=
|
||||
rec (λ x y, y) η
|
||||
end
|
||||
|
||||
section
|
||||
parameters {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
|
||||
protected definition compose (η : G ==> H) (θ : F ==> G) : F ==> H :=
|
||||
natural_transformation.mk
|
||||
(λ a, η a ∘ θ a)
|
||||
(λ a b f,
|
||||
calc
|
||||
morphism H f ∘ (η a ∘ θ a) = (morphism H f ∘ η a) ∘ θ a : assoc
|
||||
... = (η b ∘ morphism G f) ∘ θ a : {naturality η f}
|
||||
... = η b ∘ (morphism G f ∘ θ a) : symm assoc
|
||||
... = η b ∘ (θ b ∘ morphism F f) : {naturality θ f}
|
||||
... = (η b ∘ θ b) ∘ morphism F f : assoc)
|
||||
end
|
||||
precedence `∘n` : 60
|
||||
infixr `∘n` := compose
|
||||
section
|
||||
protected theorem assoc {obC obD : Type} {C : category obC} {D : category obD} {F₄ F₃ F₂ F₁ : C ⇒ D} {η₃ : F₃ ==> F₄} {η₂ : F₂ ==> F₃} {η₁ : F₁ ==> F₂} : η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
|
||||
congr_arg2_dep mk (funext (take x, assoc)) proof_irrel
|
||||
|
||||
--TODO: check whether some of the below identities are superfluous
|
||||
protected definition id {obC obD : Type} {C : category obC} {D : category obD} {F : C ⇒ D}
|
||||
: natural_transformation F F :=
|
||||
mk (λa, id) (λa b f, id_right ⬝ symm id_left)
|
||||
protected definition ID {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D)
|
||||
: natural_transformation F F := id
|
||||
-- protected definition Id {C D : Category} {F : Functor C D} : Natural_transformation F F :=
|
||||
-- Natural_transformation.mk id
|
||||
-- protected definition iD {C D : Category} (F : Functor C D) : Natural_transformation F F :=
|
||||
-- Natural_transformation.mk id
|
||||
|
||||
protected theorem id_left {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
|
||||
{η : F ==> G} : natural_transformation.compose id η = η :=
|
||||
rec (λf H, congr_arg2_dep mk (funext (take x, id_left)) proof_irrel) η
|
||||
|
||||
protected theorem id_right {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
|
||||
{η : F ==> G} : natural_transformation.compose η id = η :=
|
||||
rec (λf H, congr_arg2_dep mk (funext (take x, id_right)) proof_irrel) η
|
||||
|
||||
end
|
||||
end natural_transformation
|
||||
|
||||
-- examples of categories / basic constructions (TODO: move to separate file)
|
||||
|
||||
open functor
|
||||
namespace category
|
||||
section
|
||||
open unit
|
||||
definition one [instance] : category unit :=
|
||||
category.mk (λa b, unit) (λ a b c f g, star) (λ a, star) (λ a b c d f g h, unit.equal _ _)
|
||||
(λ a b f, unit.equal _ _) (λ a b f, unit.equal _ _)
|
||||
end
|
||||
|
||||
section
|
||||
parameter {ob : Type}
|
||||
definition opposite (C : category ob) : category ob :=
|
||||
category.mk (λa b, mor 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)
|
||||
precedence `∘op` : 60
|
||||
infixr `∘op` := @compose _ (opposite _) _ _ _
|
||||
|
||||
parameters {C : category ob} {a b c : ob}
|
||||
|
||||
theorem compose_op {f : @mor ob C a b} {g : mor b c} : f ∘op g = g ∘ f :=
|
||||
rfl
|
||||
|
||||
theorem op_op {C : category ob} : opposite (opposite C) = C :=
|
||||
category.rec (λ mor comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C
|
||||
end
|
||||
|
||||
definition Opposite (C : Category) : Category :=
|
||||
Category.mk (objects C) (opposite (category_instance C))
|
||||
|
||||
|
||||
section
|
||||
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)
|
||||
end
|
||||
|
||||
section cat_Cat
|
||||
|
||||
definition Cat : category Category :=
|
||||
mk (λ a b, Functor a b) (λ a b c g f, Compose g f) (λ a, Id)
|
||||
(λ a b c d h g f, Assoc h g f) (λ a b f, Id_left f) (λ a b f, Id_right f)
|
||||
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)
|
||||
|
||||
end cat_Cat
|
||||
|
||||
section functor_category
|
||||
parameters {obC obD : Type} (C : category obC) (D : category obD)
|
||||
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
|
||||
|
||||
|
||||
section slice
|
||||
open sigma
|
||||
|
||||
definition slice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor b c) :=
|
||||
mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
|
||||
(λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
|
||||
(calc
|
||||
dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : assoc
|
||||
... = dpr2 b ∘ dpr1 f : {dpr2 g}
|
||||
... = dpr2 a : {dpr2 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)
|
||||
--replacing proof_irrel with rfl confuses the unifier
|
||||
-- We give proof_irrel instead of rfl, to give the unifier an easier time
|
||||
end slice
|
||||
|
||||
|
||||
section coslice
|
||||
open sigma
|
||||
|
||||
definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor c b) :=
|
||||
mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
|
||||
(λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
|
||||
(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}))
|
||||
(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)
|
||||
|
|
@ -418,29 +477,73 @@ namespace category
|
|||
|
||||
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), mor a b) :=
|
||||
mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)) (h : mor (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)
|
||||
(calc
|
||||
dpr3 c ∘ (dpr1 g ∘ dpr1 f) = (dpr3 c ∘ dpr1 g) ∘ dpr1 f : assoc
|
||||
... = (dpr2' g ∘ dpr3 b) ∘ dpr1 f : {dpr3 g}
|
||||
... = dpr2' g ∘ (dpr3 b ∘ dpr1 f) : symm assoc
|
||||
... = dpr2' g ∘ (dpr2' f ∘ dpr3 a) : {dpr3 f}
|
||||
... = (dpr2' g ∘ dpr2' f) ∘ dpr3 a : assoc)))
|
||||
-- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), mor a b) :=
|
||||
-- mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)) (h : mor (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)
|
||||
|
||||
definition arrow_obs (ob : Type) (C : category ob) :=
|
||||
Σ(a b : ob), mor a b
|
||||
|
||||
definition src {ob : Type} {C : category ob} (a : arrow_obs ob C) : ob :=
|
||||
dpr1 a
|
||||
|
||||
definition dst {ob : Type} {C : category ob} (a : arrow_obs ob C) : ob :=
|
||||
dpr2' a
|
||||
|
||||
definition to_mor {ob : Type} {C : category ob} (a : arrow_obs ob C) : mor (src a) (dst a) :=
|
||||
dpr3 a
|
||||
|
||||
definition arrow_mor (ob : Type) (C : category ob) (a b : arrow_obs ob C) : Type :=
|
||||
Σ (g : mor (src a) (src b)) (h : mor (dst a) (dst b)), to_mor b ∘ g = h ∘ to_mor a
|
||||
|
||||
definition mor_src {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) : mor (src a) (src b) :=
|
||||
dpr1 m
|
||||
|
||||
definition mor_dst {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) : mor (dst a) (dst b) :=
|
||||
dpr2' m
|
||||
|
||||
definition commute {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) :
|
||||
to_mor b ∘ (mor_src m) = (mor_dst m) ∘ to_mor a :=
|
||||
dpr3 m
|
||||
|
||||
definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
|
||||
mk (λa b, arrow_mor ob C a b)
|
||||
(λ a b c g f, dpair (mor_src g ∘ mor_src f) (dpair (mor_dst g ∘ mor_dst f)
|
||||
(show to_mor c ∘ (mor_src g ∘ mor_src f) = (mor_dst g ∘ mor_dst f) ∘ to_mor a,
|
||||
proof
|
||||
calc
|
||||
to_mor c ∘ (mor_src g ∘ mor_src f) = (to_mor c ∘ mor_src g) ∘ mor_src f : assoc
|
||||
... = (mor_dst g ∘ to_mor b) ∘ mor_src f : {commute g}
|
||||
... = mor_dst g ∘ (to_mor b ∘ mor_src f) : symm assoc
|
||||
... = mor_dst g ∘ (mor_dst f ∘ to_mor a) : {commute f}
|
||||
... = (mor_dst g ∘ mor_dst f) ∘ to_mor a : assoc
|
||||
qed)
|
||||
))
|
||||
(λ 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)
|
||||
-- (λ a b c d h g f, dpair_eq assoc sorry)
|
||||
-- (λ a b f, sigma.equal id_left sorry)
|
||||
-- (λ a b f, sigma.equal id_right sorry)
|
||||
(λ a b c d h g f, dtrip_eq_ndep assoc assoc proof_irrel)
|
||||
(λ a b f, trip.equal_ndep id_left id_left proof_irrel)
|
||||
(λ a b f, trip.equal_ndep id_right id_right proof_irrel)
|
||||
|
||||
end arrow
|
||||
|
||||
|
||||
-- definition foo {obC obD : Type} (C : category obC) (D : category obD)
|
||||
-- : category (obC × obD) :=
|
||||
-- definition foo
|
||||
-- : category (sorry) :=
|
||||
-- mk (λa b, sorry)
|
||||
-- (λ a b c g f, sorry)
|
||||
-- (λ a, sorry)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||
import logic.core.inhabited logic.core.eq
|
||||
open inhabited eq_ops
|
||||
|
||||
|
|
@ -27,7 +27,7 @@ section
|
|||
|
||||
theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
|
||||
dpair a₁ b₁ = dpair a₂ b₂ :=
|
||||
congr_arg2 dpair H₁ H₂
|
||||
congr_arg2_dep dpair H₁ H₂
|
||||
|
||||
protected theorem equal {p₁ p₂ : Σx : A, B x} :
|
||||
∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
|
||||
|
|
@ -50,36 +50,22 @@ section trip_quad
|
|||
definition dpr3' (x : Σ a b c, D a b c) := dpr1 (dpr2 (dpr2 x))
|
||||
definition dpr4 (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
|
||||
|
||||
-- theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
|
||||
-- (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
|
||||
-- dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
|
||||
-- eq.rec_on H₁
|
||||
-- (λ (b₂ : B a₁) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂)
|
||||
-- (x : (eq (eq.rec_on (congr_arg2 C H₁ H₂) c₁) c₂)), sorry
|
||||
-- -- have H : dpair b₁ c₁ = dpair b₂ c₂, from
|
||||
-- -- dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
|
||||
-- -- eq.subst H rfl
|
||||
-- )
|
||||
-- b₂ c₂ H₁ H₂ H₃
|
||||
theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
|
||||
(H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
|
||||
dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
|
||||
congr_arg3_dep dtrip H₁ H₂ H₃
|
||||
end trip_quad
|
||||
|
||||
theorem dtrip_eq2 {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
|
||||
theorem dtrip_eq_ndep {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
|
||||
{c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
|
||||
(H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂) :
|
||||
(H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
|
||||
dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
|
||||
eq.rec_on H₁
|
||||
(λ (b₂ : B) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : b₁ = b₂)
|
||||
(H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂),
|
||||
have H : dpair b₁ c₁ = dpair b₂ c₂, from
|
||||
dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
|
||||
eq.subst H rfl
|
||||
)
|
||||
b₂ c₂ H₁ H₂ H₃
|
||||
congr_arg3_ndep_dep dtrip H₁ H₂ H₃
|
||||
|
||||
theorem trip.equal2 {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
|
||||
theorem trip.equal_ndep {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
|
||||
∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
|
||||
(H₃ : eq.rec_on H₂ (eq.rec_on H₁ (dpr3 p₁)) = dpr3 p₂), p₁ = p₂ :=
|
||||
(H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
|
||||
destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
|
||||
(take b₂ c₂ H₁ H₂ H₃, dtrip_eq2 H₁ H₂ H₃))))
|
||||
(take b₂ c₂ H₁ H₂ H₃, dtrip_eq_ndep H₁ H₂ H₃))))
|
||||
|
||||
end sigma
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
|
||||
|
||||
-- logic.connectives.eq
|
||||
-- ====================
|
||||
|
|
@ -18,12 +18,15 @@ refl : eq a a
|
|||
infix `=` := eq
|
||||
definition rfl {A : Type} {a : A} := eq.refl a
|
||||
|
||||
-- proof irrelevance is built in
|
||||
theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
|
||||
|
||||
namespace eq
|
||||
theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) :=
|
||||
rfl
|
||||
proof_irrel
|
||||
|
||||
theorem irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 :=
|
||||
rfl
|
||||
proof_irrel
|
||||
|
||||
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
|
||||
rec H2 H1
|
||||
|
|
@ -48,14 +51,27 @@ open eq_ops
|
|||
|
||||
namespace eq
|
||||
-- eq_rec with arguments swapped, for transporting an element of a dependent type
|
||||
definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
|
||||
eq.rec H2 H1
|
||||
|
||||
theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
|
||||
-- definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
|
||||
-- eq.rec H2 H1
|
||||
|
||||
definition rec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H1 : a = a') (H2 : B a (refl a)) : B a' H1 :=
|
||||
eq.rec (λH1 : a = a, show B a H1, from H2) H1 H1
|
||||
|
||||
theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : rec_on H b = b :=
|
||||
refl (rec_on rfl b)
|
||||
|
||||
theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : rec_on H b = b :=
|
||||
rec_on H (λ(H' : a = a), rec_on_id H' b) H
|
||||
|
||||
theorem rec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b :=
|
||||
rec_on_constant H₁ b ⬝ rec_on_constant H₂ b ⁻¹
|
||||
|
||||
theorem rec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : rec_on H b = rec_on H' b :=
|
||||
rec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
|
||||
|
||||
theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
|
||||
rec_on_id H b
|
||||
id_refl H⁻¹ ▸ refl (eq.rec b (refl a))
|
||||
|
||||
theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
|
||||
(u : P a) :
|
||||
|
|
@ -65,13 +81,43 @@ namespace eq
|
|||
H2
|
||||
end eq
|
||||
|
||||
open eq
|
||||
|
||||
theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
|
||||
H ▸ rfl
|
||||
|
||||
theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
|
||||
H ▸ rfl
|
||||
|
||||
theorem congr_arg2 {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
|
||||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
|
||||
f a = g b :=
|
||||
H1 ▸ H2 ▸ rfl
|
||||
|
||||
theorem congr_arg2 {A B C : Type} {a a' : A} {b b' : B} (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
|
||||
congr (congr_arg f Ha) Hb
|
||||
|
||||
theorem congr_arg3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' :=
|
||||
congr (congr_arg2 f Ha Hb) Hc
|
||||
|
||||
theorem congr_arg4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' :=
|
||||
congr (congr_arg3 f Ha Hb Hc) Hd
|
||||
|
||||
theorem congr_arg5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f : A → B → C → D → E → F) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f a' b' c' d' e' :=
|
||||
congr (congr_arg4 f Ha Hb Hc Hd) He
|
||||
|
||||
theorem congr2 {A B C : Type} {a a' : A} {b b' : B} (f f' : A → B → C) (Hf : f = f') (Ha : a = a') (Hb : b = b') : f a b = f' a' b' :=
|
||||
Hf ▸ congr_arg2 f Ha Hb
|
||||
|
||||
theorem congr3 {A B C D : Type} {a a' : A} {b b' : B} {c c' : C} (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f' a' b' c' :=
|
||||
Hf ▸ congr_arg3 f Ha Hb Hc
|
||||
|
||||
theorem congr4 {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f f' : A → B → C → D → E) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f' a' b' c' d' :=
|
||||
Hf ▸ congr_arg4 f Ha Hb Hc Hd
|
||||
|
||||
theorem congr5 {A B C D E F : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f f' : A → B → C → D → E → F) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') : f a b c d e = f' a' b' c' d' e' :=
|
||||
Hf ▸ congr_arg5 f Ha Hb Hc Hd He
|
||||
|
||||
theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
|
||||
{b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
|
||||
f a₁ b₁ = f a₂ b₂ :=
|
||||
eq.rec_on H₁
|
||||
|
|
@ -81,9 +127,21 @@ theorem congr_arg2 {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
|
|||
... = f a₁ b₂ : {H₂})
|
||||
b₂ H₁ H₂
|
||||
|
||||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
|
||||
f a = g b :=
|
||||
H1 ▸ H2 ▸ rfl
|
||||
theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
|
||||
(H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
|
||||
f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
|
||||
eq.rec_on H₁
|
||||
(λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂)
|
||||
(H₃ : (rec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
|
||||
have H₃' : eq.rec_on H₂ c₁ = c₂,
|
||||
from (rec_on_irrel H₂ (congr_arg2_dep C (refl a₁) H₂) c₁⁻¹) ▸ H₃,
|
||||
congr_arg2_dep (f a₁) H₂ H₃')
|
||||
b₂ H₂ c₂ H₃
|
||||
|
||||
theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D)
|
||||
(H₁ : a₁ = a₂) (H₂ : b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
|
||||
f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
|
||||
congr_arg3_dep f H₁ (rec_on_constant H₁ b₁ ⬝ H₂) H₃
|
||||
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
|
||||
take x, congr_fun H x
|
||||
|
|
@ -109,9 +167,6 @@ assume Ha, H2 ▸ (H1 Ha)
|
|||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 ▸ Ha)
|
||||
|
||||
-- proof irrelevance is built in the kernel
|
||||
theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
|
||||
|
||||
-- ne
|
||||
-- --
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue