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

chore(hott) fix the types and algebra

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-12 14:19:06 -05:00 committed by Leonardo de Moura
parent 341a3d4411
commit 503048226e
14 changed files with 394 additions and 395 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/algebra/binary.hlean
View file

@ -10,7 +10,7 @@ General properties of binary operations.
open eq
namespace path_binary
namespace binary
section
variable {A : Type}
variables (op₁ : A → A → A) (inv : A → A) (one : A)
@ -71,4 +71,4 @@ namespace path_binary
... = a*((b*c)*d) : H_assoc
end
end path_binary
end binary

5
hott/algebra/category/basic.hlean
View file

@ -3,9 +3,8 @@
-- Author: Jakob von Raumer
import ..precategory.basic ..precategory.morphism ..precategory.iso
import hott.equiv hott.trunc
open precategory morphism is_equiv path truncation nat sigma sigma.ops
open precategory morphism is_equiv eq truncation nat sigma sigma.ops
-- A category is a precategory extended by a witness,
-- that the function assigning to each isomorphism a path,
@ -21,7 +20,7 @@ namespace category
-- TODO: Unsafe class instance?
instance [persistent] iso_of_path_equiv
definition path_of_iso {a b : ob} : a ≅ b → a ≈ b :=
definition path_of_iso {a b : ob} : a ≅ b → a = b :=
iso_of_path⁻¹
definition ob_1_type : is_trunc nat.zero .+1 ob :=

371
hott/algebra/group.hlean
View file

@ -8,10 +8,9 @@ Authors: Jeremy Avigad, Leonardo de Moura
Various multiplicative and additive structures. Partially modeled on Isabelle's library.
-/
import hott.path hott.trunc data.unit data.sigma data.prod
import hott.algebra.binary
import algebra.binary
open path truncation path_binary -- note: ⁻¹ will be overloaded
open eq truncation binary -- note: ⁻¹ will be overloaded
namespace path_algebra
@ -48,81 +47,81 @@ notation 0 := !has_zero.zero
structure semigroup [class] (A : Type) extends has_mul A :=
(carrier_hset : is_hset A)
(mul_assoc : ∀a b c, mul (mul a b) c ≈ mul a (mul b c))
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c ≈ a * (b * c) :=
theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
!semigroup.mul_assoc
structure comm_semigroup [class] (A : Type) extends semigroup A :=
(mul_comm : ∀a b, mul a b ≈ mul b a)
(mul_comm : ∀a b, mul a b = mul b a)
theorem mul_comm [s : comm_semigroup A] (a b : A) : a * b ≈ b * a :=
theorem mul_comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
!comm_semigroup.mul_comm
theorem mul_left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) ≈ b * (a * c) :=
path_binary.left_comm (@mul_comm A s) (@mul_assoc A s) a b c
theorem mul_left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
binary.left_comm (@mul_comm A s) (@mul_assoc A s) a b c
theorem mul_right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c ≈ (a * c) * b :=
path_binary.right_comm (@mul_comm A s) (@mul_assoc A s) a b c
theorem mul_right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
binary.right_comm (@mul_comm A s) (@mul_assoc A s) a b c
structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_left_cancel : ∀a b c, mul a b ≈ mul a c → b ≈ c)
(mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
theorem mul_left_cancel [s : left_cancel_semigroup A] {a b c : A} :
a * b ≈ a * c → b ≈ c :=
a * b = a * c → b = c :=
!left_cancel_semigroup.mul_left_cancel
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_right_cancel : ∀a b c, mul a b ≈ mul c b → a ≈ c)
(mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
theorem mul_right_cancel [s : right_cancel_semigroup A] {a b c : A} :
a * b ≈ c * b → a ≈ c :=
a * b = c * b → a = c :=
!right_cancel_semigroup.mul_right_cancel
/- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A :=
(add_assoc : ∀a b c, add (add a b) c ≈ add a (add b c))
(add_assoc : ∀a b c, add (add a b) c = add a (add b c))
theorem add_assoc [s : add_semigroup A] (a b c : A) : a + b + c ≈ a + (b + c) :=
theorem add_assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
!add_semigroup.add_assoc
structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
(add_comm : ∀a b, add a b ≈ add b a)
(add_comm : ∀a b, add a b = add b a)
theorem add_comm [s : add_comm_semigroup A] (a b : A) : a + b ≈ b + a :=
theorem add_comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
!add_comm_semigroup.add_comm
theorem add_left_comm [s : add_comm_semigroup A] (a b c : A) :
a + (b + c) ≈ b + (a + c) :=
path_binary.left_comm (@add_comm A s) (@add_assoc A s) a b c
a + (b + c) = b + (a + c) :=
binary.left_comm (@add_comm A s) (@add_assoc A s) a b c
theorem add_right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c ≈ (a + c) + b :=
path_binary.right_comm (@add_comm A s) (@add_assoc A s) a b c
theorem add_right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
binary.right_comm (@add_comm A s) (@add_assoc A s) a b c
structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_left_cancel : ∀a b c, add a b ≈ add a c → b ≈ c)
(add_left_cancel : ∀a b c, add a b = add a c → b = c)
theorem add_left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
a + b ≈ a + c → b ≈ c :=
a + b = a + c → b = c :=
!add_left_cancel_semigroup.add_left_cancel
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_right_cancel : ∀a b c, add a b ≈ add c b → a ≈ c)
(add_right_cancel : ∀a b c, add a b = add c b → a = c)
theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
a + b ≈ c + b → a ≈ c :=
a + b = c + b → a = c :=
!add_right_cancel_semigroup.add_right_cancel
/- monoid -/
structure monoid [class] (A : Type) extends semigroup A, has_one A :=
(mul_left_id : ∀a, mul one a ≈ a) (mul_right_id : ∀a, mul a one ≈ a)
(mul_left_id : ∀a, mul one a = a) (mul_right_id : ∀a, mul a one = a)
theorem mul_left_id [s : monoid A] (a : A) : 1 * a ≈ a := !monoid.mul_left_id
theorem mul_left_id [s : monoid A] (a : A) : 1 * a = a := !monoid.mul_left_id
theorem mul_right_id [s : monoid A] (a : A) : a * 1 ≈ a := !monoid.mul_right_id
theorem mul_right_id [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_right_id
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
@ -130,11 +129,11 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
/- additive monoid -/
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
(add_left_id : ∀a, add zero a ≈ a) (add_right_id : ∀a, add a zero ≈ a)
(add_left_id : ∀a, add zero a = a) (add_right_id : ∀a, add a zero = a)
theorem add_left_id [s : add_monoid A] (a : A) : 0 + a ≈ a := !add_monoid.add_left_id
theorem add_left_id [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.add_left_id
theorem add_right_id [s : add_monoid A] (a : A) : a + 0 ≈ a := !add_monoid.add_right_id
theorem add_right_id [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_right_id
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
@ -143,7 +142,7 @@ structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semi
/- group -/
structure group [class] (A : Type) extends monoid A, has_inv A :=
(mul_left_inv : ∀a, mul (inv a) a ≈ one)
(mul_left_inv : ∀a, mul (inv a) a = one)
-- Note: with more work, we could derive the axiom mul_left_id
@ -152,125 +151,125 @@ section group
variable [s : group A]
include s
theorem mul_left_inv (a : A) : a⁻¹ * a ≈ 1 := !group.mul_left_inv
theorem mul_left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) ≈ b :=
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
calc
a⁻¹ * (a * b) ≈ a⁻¹ * a * b : mul_assoc
... ≈ 1 * b : mul_left_inv
... ≈ b : mul_left_id
a⁻¹ * (a * b) = a⁻¹ * a * b : mul_assoc
... = 1 * b : mul_left_inv
... = b : mul_left_id
theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b ≈ a :=
theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b = a :=
calc
a * b⁻¹ * b ≈ a * (b⁻¹ * b) : mul_assoc
... ≈ a * 1 : mul_left_inv
... ≈ a : mul_right_id
a * b⁻¹ * b = a * (b⁻¹ * b) : mul_assoc
... = a * 1 : mul_left_inv
... = a : mul_right_id
theorem inv_unique {a b : A} (H : a * b ≈ 1) : a⁻¹ ≈ b :=
theorem inv_unique {a b : A} (H : a * b = 1) : a⁻¹ = b :=
calc
a⁻¹ ≈ a⁻¹ * 1 : mul_right_id
... ≈ a⁻¹ * (a * b) : H
... ≈ b : inv_mul_cancel_left
a⁻¹ = a⁻¹ * 1 : mul_right_id
... = a⁻¹ * (a * b) : H
... = b : inv_mul_cancel_left
theorem inv_one : 1⁻¹ ≈ 1 := inv_unique (mul_left_id 1)
theorem inv_one : 1⁻¹ = 1 := inv_unique (mul_left_id 1)
theorem inv_inv (a : A) : (a⁻¹)⁻¹ ≈ a := inv_unique (mul_left_inv a)
theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_unique (mul_left_inv a)
theorem inv_inj {a b : A} (H : a⁻¹ ≈ b⁻¹) : a ≈ b :=
theorem inv_inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
calc
a ≈ (a⁻¹)⁻¹ : inv_inv
... ≈ b : inv_unique (H⁻¹ ▹ (mul_left_inv _))
a = (a⁻¹)⁻¹ : inv_inv
... = b : inv_unique (H⁻¹ ▹ (mul_left_inv _))
--theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ ≈ b⁻¹ ↔ a ≈ b :=
--theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
--iff.intro (assume H, inv_inj H) (assume H, congr_arg _ H)
--theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ ≈ 1 ↔ a ≈ 1 :=
--theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
--inv_one ▹ !inv_eq_inv_iff_eq
theorem eq_inv_imp_eq_inv {a b : A} (H : a ≈ b⁻¹) : b ≈ a⁻¹ :=
theorem eq_inv_imp_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
H⁻¹ ▹ (inv_inv b)⁻¹
--theorem eq_inv_iff_eq_inv (a b : A) : a ≈ b⁻¹ ↔ b ≈ a⁻¹ :=
--theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
--iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv
theorem mul_right_inv (a : A) : a * a⁻¹ ≈ 1 :=
theorem mul_right_inv (a : A) : a * a⁻¹ = 1 :=
calc
a * a⁻¹ ≈ (a⁻¹)⁻¹ * a⁻¹ : inv_inv
... ≈ 1 : mul_left_inv
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv
... = 1 : mul_left_inv
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) ≈ b :=
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
calc
a * (a⁻¹ * b) ≈ a * a⁻¹ * b : mul_assoc
... ≈ 1 * b : mul_right_inv
... ≈ b : mul_left_id
a * (a⁻¹ * b) = a * a⁻¹ * b : mul_assoc
... = 1 * b : mul_right_inv
... = b : mul_left_id
theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ ≈ a :=
theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ = a :=
calc
a * b * b⁻¹ ≈ a * (b * b⁻¹) : mul_assoc
... ≈ a * 1 : mul_right_inv
... ≈ a : mul_right_id
a * b * b⁻¹ = a * (b * b⁻¹) : mul_assoc
... = a * 1 : mul_right_inv
... = a : mul_right_id
theorem inv_mul (a b : A) : (a * b)⁻¹ ≈ b⁻¹ * a⁻¹ :=
theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
inv_unique
(calc
a * b * (b⁻¹ * a⁻¹) ≈ a * (b * (b⁻¹ * a⁻¹)) : mul_assoc
... ≈ a * a⁻¹ : mul_inv_cancel_left
... ≈ 1 : mul_right_inv)
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul_assoc
... = a * a⁻¹ : mul_inv_cancel_left
... = 1 : mul_right_inv)
theorem mul_inv_eq_one_imp_eq {a b : A} (H : a * b⁻¹ ≈ 1) : a ≈ b :=
theorem mul_inv_eq_one_imp_eq {a b : A} (H : a * b⁻¹ = 1) : a = b :=
calc
a ≈ a * b⁻¹ * b : inv_mul_cancel_right
... ≈ 1 * b : H
... ≈ b : mul_left_id
a = a * b⁻¹ * b : inv_mul_cancel_right
... = 1 * b : H
... = b : mul_left_id
-- TODO: better names for the next eight theorems? (Also for additive ones.)
theorem mul_eq_imp_eq_mul_inv {a b c : A} (H : a * b ≈ c) : a ≈ c * b⁻¹ :=
theorem mul_eq_imp_eq_mul_inv {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
H ▹ !mul_inv_cancel_right⁻¹
theorem mul_eq_imp_eq_inv_mul {a b c : A} (H : a * b ≈ c) : b ≈ a⁻¹ * c :=
theorem mul_eq_imp_eq_inv_mul {a b c : A} (H : a * b = c) : b = a⁻¹ * c :=
H ▹ !inv_mul_cancel_left⁻¹
theorem eq_mul_imp_inv_mul_eq {a b c : A} (H : a ≈ b * c) : b⁻¹ * a ≈ c :=
theorem eq_mul_imp_inv_mul_eq {a b c : A} (H : a = b * c) : b⁻¹ * a = c :=
H⁻¹ ▹ !inv_mul_cancel_left
theorem eq_mul_imp_mul_inv_eq {a b c : A} (H : a ≈ b * c) : a * c⁻¹ ≈ b :=
theorem eq_mul_imp_mul_inv_eq {a b c : A} (H : a = b * c) : a * c⁻¹ = b :=
H⁻¹ ▹ !mul_inv_cancel_right
theorem mul_inv_eq_imp_eq_mul {a b c : A} (H : a * b⁻¹ ≈ c) : a ≈ c * b :=
theorem mul_inv_eq_imp_eq_mul {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
!inv_inv ▹ (mul_eq_imp_eq_mul_inv H)
theorem inv_mul_eq_imp_eq_mul {a b c : A} (H : a⁻¹ * b ≈ c) : b ≈ a * c :=
theorem inv_mul_eq_imp_eq_mul {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
!inv_inv ▹ (mul_eq_imp_eq_inv_mul H)
theorem eq_inv_mul_imp_mul_eq {a b c : A} (H : a ≈ b⁻¹ * c) : b * a ≈ c :=
theorem eq_inv_mul_imp_mul_eq {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
!inv_inv ▹ (eq_mul_imp_inv_mul_eq H)
theorem eq_mul_inv_imp_mul_eq {a b c : A} (H : a ≈ b * c⁻¹) : a * c ≈ b :=
theorem eq_mul_inv_imp_mul_eq {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
!inv_inv ▹ (eq_mul_imp_mul_inv_eq H)
--theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b ≈ c ↔ b ≈ a⁻¹ * c :=
--theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
--iff.intro mul_eq_imp_eq_inv_mul eq_inv_mul_imp_mul_eq
--theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b ≈ c ↔ a ≈ c * b⁻¹ :=
--theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
--iff.intro mul_eq_imp_eq_mul_inv eq_mul_inv_imp_mul_eq
definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A :=
left_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b ≈ a * c,
assume H : a * b = a * c,
calc
b ≈ a⁻¹ * (a * b) : inv_mul_cancel_left
... ≈ a⁻¹ * (a * c) : H
... ≈ c : inv_mul_cancel_left)
b = a⁻¹ * (a * b) : inv_mul_cancel_left
... = a⁻¹ * (a * c) : H
... = c : inv_mul_cancel_left)
definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A :=
right_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b ≈ c * b,
assume H : a * b = c * b,
calc
a ≈ (a * b) * b⁻¹ : mul_inv_cancel_right
... ≈ (c * b) * b⁻¹ : H
... ≈ c : mul_inv_cancel_right)
a = (a * b) * b⁻¹ : mul_inv_cancel_right
... = (c * b) * b⁻¹ : H
... = c : mul_inv_cancel_right)
end group
@ -280,127 +279,127 @@ structure comm_group [class] (A : Type) extends group A, comm_monoid A
/- additive group -/
structure add_group [class] (A : Type) extends add_monoid A, has_neg A :=
(add_left_inv : ∀a, add (neg a) a ≈ zero)
(add_left_inv : ∀a, add (neg a) a = zero)
section add_group
variables [s : add_group A]
include s
theorem add_left_inv (a : A) : -a + a ≈ 0 := !add_group.add_left_inv
theorem add_left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
theorem neg_add_cancel_left (a b : A) : -a + (a + b) ≈ b :=
theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
calc
-a + (a + b) ≈ -a + a + b : add_assoc
... ≈ 0 + b : add_left_inv
... ≈ b : add_left_id
-a + (a + b) = -a + a + b : add_assoc
... = 0 + b : add_left_inv
... = b : add_left_id
theorem neg_add_cancel_right (a b : A) : a + -b + b ≈ a :=
theorem neg_add_cancel_right (a b : A) : a + -b + b = a :=
calc
a + -b + b ≈ a + (-b + b) : add_assoc
... ≈ a + 0 : add_left_inv
... ≈ a : add_right_id
a + -b + b = a + (-b + b) : add_assoc
... = a + 0 : add_left_inv
... = a : add_right_id
theorem neg_unique {a b : A} (H : a + b ≈ 0) : -a ≈ b :=
theorem neg_unique {a b : A} (H : a + b = 0) : -a = b :=
calc
-a ≈ -a + 0 : add_right_id
... ≈ -a + (a + b) : H
... ≈ b : neg_add_cancel_left
-a = -a + 0 : add_right_id
... = -a + (a + b) : H
... = b : neg_add_cancel_left
theorem neg_zero : -0 ≈ 0 := neg_unique (add_left_id 0)
theorem neg_zero : -0 = 0 := neg_unique (add_left_id 0)
theorem neg_neg (a : A) : -(-a) ≈ a := neg_unique (add_left_inv a)
theorem neg_neg (a : A) : -(-a) = a := neg_unique (add_left_inv a)
theorem neg_inj {a b : A} (H : -a ≈ -b) : a ≈ b :=
theorem neg_inj {a b : A} (H : -a = -b) : a = b :=
calc
a ≈ -(-a) : neg_neg
... ≈ b : neg_unique (H⁻¹ ▹ (add_left_inv _))
a = -(-a) : neg_neg
... = b : neg_unique (H⁻¹ ▹ (add_left_inv _))
--theorem neg_eq_neg_iff_eq (a b : A) : -a ≈ -b ↔ a ≈ b :=
--theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
--iff.intro (assume H, neg_inj H) (assume H, congr_arg _ H)
--theorem neg_eq_zero_iff_eq_zero (a b : A) : -a ≈ 0 ↔ a ≈ 0 :=
--theorem neg_eq_zero_iff_eq_zero (a b : A) : -a = 0 ↔ a = 0 :=
--neg_zero ▹ !neg_eq_neg_iff_eq
theorem eq_neg_imp_eq_neg {a b : A} (H : a ≈ -b) : b ≈ -a :=
theorem eq_neg_imp_eq_neg {a b : A} (H : a = -b) : b = -a :=
H⁻¹ ▹ (neg_neg b)⁻¹
--theorem eq_neg_iff_eq_neg (a b : A) : a ≈ -b ↔ b ≈ -a :=
--theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
--iff.intro !eq_neg_imp_eq_neg !eq_neg_imp_eq_neg
theorem add_right_inv (a : A) : a + -a ≈ 0 :=
theorem add_right_inv (a : A) : a + -a = 0 :=
calc
a + -a ≈ -(-a) + -a : neg_neg
... ≈ 0 : add_left_inv
a + -a = -(-a) + -a : neg_neg
... = 0 : add_left_inv
theorem add_neg_cancel_left (a b : A) : a + (-a + b) ≈ b :=
theorem add_neg_cancel_left (a b : A) : a + (-a + b) = b :=
calc
a + (-a + b) ≈ a + -a + b : add_assoc
... ≈ 0 + b : add_right_inv
... ≈ b : add_left_id
a + (-a + b) = a + -a + b : add_assoc
... = 0 + b : add_right_inv
... = b : add_left_id
theorem add_neg_cancel_right (a b : A) : a + b + -b ≈ a :=
theorem add_neg_cancel_right (a b : A) : a + b + -b = a :=
calc
a + b + -b ≈ a + (b + -b) : add_assoc
... ≈ a + 0 : add_right_inv
... ≈ a : add_right_id
a + b + -b = a + (b + -b) : add_assoc
... = a + 0 : add_right_inv
... = a : add_right_id
theorem neg_add (a b : A) : -(a + b) ≈ -b + -a :=
theorem neg_add (a b : A) : -(a + b) = -b + -a :=
neg_unique
(calc
a + b + (-b + -a) ≈ a + (b + (-b + -a)) : add_assoc
... ≈ a + -a : add_neg_cancel_left
... ≈ 0 : add_right_inv)
a + b + (-b + -a) = a + (b + (-b + -a)) : add_assoc
... = a + -a : add_neg_cancel_left
... = 0 : add_right_inv)
theorem add_eq_imp_eq_add_neg {a b c : A} (H : a + b ≈ c) : a ≈ c + -b :=
theorem add_eq_imp_eq_add_neg {a b c : A} (H : a + b = c) : a = c + -b :=
H ▹ !add_neg_cancel_right⁻¹
theorem add_eq_imp_eq_neg_add {a b c : A} (H : a + b ≈ c) : b ≈ -a + c :=
theorem add_eq_imp_eq_neg_add {a b c : A} (H : a + b = c) : b = -a + c :=
H ▹ !neg_add_cancel_left⁻¹
theorem eq_add_imp_neg_add_eq {a b c : A} (H : a ≈ b + c) : -b + a ≈ c :=
theorem eq_add_imp_neg_add_eq {a b c : A} (H : a = b + c) : -b + a = c :=
H⁻¹ ▹ !neg_add_cancel_left
theorem eq_add_imp_add_neg_eq {a b c : A} (H : a ≈ b + c) : a + -c ≈ b :=
theorem eq_add_imp_add_neg_eq {a b c : A} (H : a = b + c) : a + -c = b :=
H⁻¹ ▹ !add_neg_cancel_right
theorem add_neg_eq_imp_eq_add {a b c : A} (H : a + -b ≈ c) : a ≈ c + b :=
theorem add_neg_eq_imp_eq_add {a b c : A} (H : a + -b = c) : a = c + b :=
!neg_neg ▹ (add_eq_imp_eq_add_neg H)
theorem neg_add_eq_imp_eq_add {a b c : A} (H : -a + b ≈ c) : b ≈ a + c :=
theorem neg_add_eq_imp_eq_add {a b c : A} (H : -a + b = c) : b = a + c :=
!neg_neg ▹ (add_eq_imp_eq_neg_add H)
theorem eq_neg_add_imp_add_eq {a b c : A} (H : a ≈ -b + c) : b + a ≈ c :=
theorem eq_neg_add_imp_add_eq {a b c : A} (H : a = -b + c) : b + a = c :=
!neg_neg ▹ (eq_add_imp_neg_add_eq H)
theorem eq_add_neg_imp_add_eq {a b c : A} (H : a ≈ b + -c) : a + c ≈ b :=
theorem eq_add_neg_imp_add_eq {a b c : A} (H : a = b + -c) : a + c = b :=
!neg_neg ▹ (eq_add_imp_add_neg_eq H)
--theorem add_eq_iff_eq_neg_add (a b c : A) : a + b ≈ c ↔ b ≈ -a + c :=
--theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
--iff.intro add_eq_imp_eq_neg_add eq_neg_add_imp_add_eq
--theorem add_eq_iff_eq_add_neg (a b c : A) : a + b ≈ c ↔ a ≈ c + -b :=
--theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
--iff.intro add_eq_imp_eq_add_neg eq_add_neg_imp_add_eq
definition add_group.to_left_cancel_semigroup [instance] :
add_left_cancel_semigroup A :=
add_left_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
assume H : a + b ≈ a + c,
assume H : a + b = a + c,
calc
b ≈ -a + (a + b) : neg_add_cancel_left
... ≈ -a + (a + c) : H
... ≈ c : neg_add_cancel_left)
b = -a + (a + b) : neg_add_cancel_left
... = -a + (a + c) : H
... = c : neg_add_cancel_left)
definition add_group.to_add_right_cancel_semigroup [instance] :
add_right_cancel_semigroup A :=
add_right_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
assume H : a + b ≈ c + b,
assume H : a + b = c + b,
calc
a ≈ (a + b) + -b : add_neg_cancel_right
... ≈ (c + b) + -b : H
... ≈ c : add_neg_cancel_right)
a = (a + b) + -b : add_neg_cancel_right
... = (c + b) + -b : H
... = c : add_neg_cancel_right)
/- minus -/
@ -409,52 +408,52 @@ section add_group
infix `-` := minus
theorem minus_self (a : A) : a - a ≈ 0 := !add_right_inv
theorem minus_self (a : A) : a - a = 0 := !add_right_inv
theorem minus_add_cancel (a b : A) : a - b + b ≈ a := !neg_add_cancel_right
theorem minus_add_cancel (a b : A) : a - b + b = a := !neg_add_cancel_right
theorem add_minus_cancel (a b : A) : a + b - b ≈ a := !add_neg_cancel_right
theorem add_minus_cancel (a b : A) : a + b - b = a := !add_neg_cancel_right
theorem minus_eq_zero_imp_eq {a b : A} (H : a - b ≈ 0) : a ≈ b :=
theorem minus_eq_zero_imp_eq {a b : A} (H : a - b = 0) : a = b :=
calc
a ≈ (a - b) + b : minus_add_cancel
... ≈ 0 + b : H
... ≈ b : add_left_id
a = (a - b) + b : minus_add_cancel
... = 0 + b : H
... = b : add_left_id
--theorem eq_iff_minus_eq_zero (a b : A) : a ≈ b ↔ a - b ≈ 0 :=
--theorem eq_iff_minus_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
--iff.intro (assume H, H ▹ !minus_self) (assume H, minus_eq_zero_imp_eq H)
theorem zero_minus (a : A) : 0 - a ≈ -a := !add_left_id
theorem zero_minus (a : A) : 0 - a = -a := !add_left_id
theorem minus_zero (a : A) : a - 0 ≈ a := (neg_zero⁻¹) ▹ !add_right_id
theorem minus_zero (a : A) : a - 0 = a := (neg_zero⁻¹) ▹ !add_right_id
theorem minus_neg_eq_add (a b : A) : a - (-b) ≈ a + b := !neg_neg⁻¹ ▹ idp
theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▹ idp
theorem neg_minus_eq (a b : A) : -(a - b) ≈ b - a :=
theorem neg_minus_eq (a b : A) : -(a - b) = b - a :=
neg_unique
(calc
a - b + (b - a) ≈ a - b + b - a : add_assoc
... ≈ a - a : minus_add_cancel
... ≈ 0 : minus_self)
a - b + (b - a) = a - b + b - a : add_assoc
... = a - a : minus_add_cancel
... = 0 : minus_self)
theorem add_minus_eq (a b c : A) : a + (b - c) ≈ a + b - c := !add_assoc⁻¹
theorem add_minus_eq (a b c : A) : a + (b - c) = a + b - c := !add_assoc⁻¹
theorem minus_add_eq_minus_swap (a b c : A) : a - (b + c) ≈ a - c - b :=
theorem minus_add_eq_minus_swap (a b c : A) : a - (b + c) = a - c - b :=
calc
a - (b + c) ≈ a + (-c - b) : neg_add
... ≈ a - c - b : add_assoc
a - (b + c) = a + (-c - b) : neg_add
... = a - c - b : add_assoc
--theorem minus_eq_iff_eq_add (a b c : A) : a - b ≈ c ↔ a ≈ c + b :=
--theorem minus_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
--iff.intro (assume H, add_neg_eq_imp_eq_add H) (assume H, eq_add_imp_add_neg_eq H)
--theorem eq_minus_iff_add_eq (a b c : A) : a ≈ b - c ↔ a + c ≈ b :=
--theorem eq_minus_iff_add_eq (a b c : A) : a = b - c ↔ a + c = b :=
--iff.intro (assume H, eq_add_neg_imp_add_eq H) (assume H, add_eq_imp_eq_add_neg H)
--theorem minus_eq_minus_iff {a b c d : A} (H : a - b ≈ c - d) : a ≈ b ↔ c ≈ d :=
--theorem minus_eq_minus_iff {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
--calc
-- a ≈ b ↔ a - b ≈ 0 : eq_iff_minus_eq_zero
-- ... ↔ c - d ≈ 0 : H ▹ !iff.refl
-- ... ↔ c ≈ d : iff.symm (eq_iff_minus_eq_zero c d)
-- a = b ↔ a - b = 0 : eq_iff_minus_eq_zero
-- ... ↔ c - d = 0 : H ▹ !iff.refl
-- ... ↔ c = d : iff.symm (eq_iff_minus_eq_zero c d)
end add_group
@ -465,26 +464,26 @@ section add_comm_group
variable [s : add_comm_group A]
include s
theorem minus_add_eq (a b c : A) : a - (b + c) ≈ a - b - c :=
theorem minus_add_eq (a b c : A) : a - (b + c) = a - b - c :=
!add_comm ▹ !minus_add_eq_minus_swap
theorem neg_add_eq_minus (a b : A) : -a + b ≈ b - a := !add_comm
theorem neg_add_eq_minus (a b : A) : -a + b = b - a := !add_comm
theorem neg_add_distrib (a b : A) : -(a + b) ≈ -a + -b := !add_comm ▹ !neg_add
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := !add_comm ▹ !neg_add
theorem minus_add_right_comm (a b c : A) : a - b + c ≈ a + c - b := !add_right_comm
theorem minus_add_right_comm (a b c : A) : a - b + c = a + c - b := !add_right_comm
theorem minus_minus_eq (a b c : A) : a - b - c ≈ a - (b + c) :=
theorem minus_minus_eq (a b c : A) : a - b - c = a - (b + c) :=
calc
a - b - c ≈ a + (-b + -c) : add_assoc
... ≈ a + -(b + c) : neg_add_distrib
... ≈ a - (b + c) : idp
a - b - c = a + (-b + -c) : add_assoc
... = a + -(b + c) : neg_add_distrib
... = a - (b + c) : idp
theorem add_minus_cancel_left (a b c : A) : (c + a) - (c + b) ≈ a - b :=
theorem add_minus_cancel_left (a b c : A) : (c + a) - (c + b) = a - b :=
calc
(c + a) - (c + b) ≈ c + a - c - b : minus_add_eq
... ≈ a + c - c - b : add_comm a c
... ≈ a - b : add_minus_cancel
(c + a) - (c + b) = c + a - c - b : minus_add_eq
... = a + c - c - b : add_comm a c
... = a - b : add_minus_cancel
end add_comm_group

20
hott/algebra/groupoid.hlean
View file

@ -4,7 +4,7 @@
-- Ported from Coq HoTT
import .precategory.basic .precategory.morphism .group
open path function prod sigma truncation morphism nat path_algebra unit
open eq function prod sigma truncation morphism nat path_algebra unit
structure foo (A : Type) := (bsp : A)
@ -23,14 +23,14 @@ open precategory
definition path_groupoid (A : Type.{l})
(H : is_trunc (nat.zero .+1) A) : groupoid.{l l} A :=
groupoid.mk
(λ (a b : A), a ≈ b)
(λ (a b : A), have ish : is_hset (a ≈ b), from succ_is_trunc nat.zero a b, ish)
(λ (a b c : A) (p : b ≈ c) (q : a ≈ b), q ⬝ p)
(λ (a : A), idpath a)
(λ (a b c d : A) (p : c ≈ d) (q : b ≈ c) (r : a ≈ b), concat_pp_p r q p)
(λ (a b : A) (p : a ≈ b), concat_p1 p)
(λ (a b : A) (p : a ≈ b), concat_1p p)
(λ (a b : A) (p : a ≈ b), @is_iso.mk A _ a b p (path.inverse p)
(λ (a b : A), a = b)
(λ (a b : A), have ish : is_hset (a = b), from succ_is_trunc nat.zero a b, ish)
(λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p)
(λ (a : A), refl a)
(λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), concat_pp_p r q p)
(λ (a b : A) (p : a = b), concat_p1 p)
(λ (a b : A) (p : a = b), concat_1p p)
(λ (a b : A) (p : a = b), @is_iso.mk A _ a b p (p⁻¹)
!concat_pV !concat_Vp)
-- A groupoid with a contractible carrier is a group
@ -80,7 +80,7 @@ end
-- TODO: This is probably wrong
open equiv is_equiv
definition group_equiv {A : Type.{l}} [fx : funext]
: group A ≃ Σ (G : groupoid.{l l} unit), @hom unit G ⋆ ⋆ ≈ A :=
: group A ≃ Σ (G : groupoid.{l l} unit), @hom unit G ⋆ ⋆ = A :=
sorry

26
hott/algebra/precategory/basic.hlean
View file

@ -2,9 +2,7 @@
-- 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
open eq truncation
structure precategory [class] (ob : Type) : Type :=
(hom : ob → ob → Type)
@ -12,9 +10,9 @@ structure precategory [class] (ob : Type) : Type :=
(comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
(ID : Π (a : ob), hom a a)
(assoc : Π ⦃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)
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f ≈ f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID ≈ f)
comp h (comp g f) = comp (comp h g) f)
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
namespace precategory
variables {ob : Type} [C : precategory ob]
@ -33,15 +31,15 @@ namespace precategory
--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 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 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
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
@ -60,5 +58,5 @@ end precategory
open precategory
theorem Precategory.equal (C : Precategory) : Precategory.mk C C ≈ C :=
theorem Precategory.equal (C : Precategory) : Precategory.mk C C = C :=
Precategory.rec (λ ob c, idp) C

20
hott/algebra/precategory/constructions.hlean
View file

@ -5,10 +5,10 @@
-- This file contains basic constructions on precategories, including common precategories
import .natural_transformation hott.path
import data.unit data.sigma data.prod data.empty data.bool hott.types.prod hott.types.sigma
import .natural_transformation
import types.prod types.sigma
open path prod eq eq.ops
open eq prod eq eq.ops
namespace precategory
namespace opposite
@ -28,16 +28,16 @@ namespace precategory
variables {C : Precategory} {a b c : C}
theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g ≈ g ∘ f := idp
theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp
-- TODO: Decide whether just to use funext for this theorem or
-- take the trick they use in Coq-HoTT, and introduce a further
-- axiom in the definition of precategories that provides thee
-- symmetric associativity proof.
theorem op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) ≈ C :=
theorem op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
sorry
theorem op_op : Opposite (Opposite C) ≈ C :=
theorem op_op : Opposite (Opposite C) = C :=
(ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal
end
@ -189,12 +189,12 @@ namespace precategory
mk (λa b, slice_hom a b)
sorry
(λ 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,
(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}
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_path !assoc sorry)

27
hott/algebra/precategory/functor.hlean
View file

@ -3,14 +3,13 @@
-- Authors: Floris van Doorn, Jakob von Raumer
import .basic
import hott.path
open function
open precategory path heq
open function precategory eq
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) →
(Π (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
@ -24,11 +23,11 @@ namespace functor
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 :=
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 :=
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 :=
@ -36,17 +35,17 @@ namespace functor
(λ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))
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))
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 :=
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
sorry
-/
@ -54,9 +53,9 @@ namespace functor
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 :=
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 :=
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

12
hott/algebra/precategory/iso.hlean
View file

@ -2,9 +2,9 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
import .basic .morphism hott.types.prod
import .basic .morphism types.sigma
open path precategory sigma sigma.ops equiv is_equiv function truncation
open eq precategory sigma sigma.ops equiv is_equiv function truncation
open prod
namespace morphism
@ -12,8 +12,8 @@ namespace morphism
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
-- "is_iso f" is equivalent to a certain sigma type
definition sigma_char (f : hom a b) :
(Σ (g : hom b a), (g ∘ f ≈ id) × (f ∘ g ≈ id)) ≃ is_iso f :=
protected definition sigma_char (f : hom a b) :
(Σ (g : hom b a), (g ∘ f = id) × (f ∘ g = id)) ≃ is_iso f :=
begin
fapply (equiv.mk),
intro S, apply is_iso.mk,
@ -62,7 +62,7 @@ namespace morphism
end
-- In a precategory, equal objects are isomorphic
definition iso_of_path (p : a ≈ b) : isomorphic a b :=
path.rec_on p (isomorphic.mk id)
definition iso_of_path (p : a = b) : isomorphic a b :=
eq.rec_on p (isomorphic.mk id)
end morphism

208
hott/algebra/precategory/morphism.hlean
View file

@ -2,19 +2,19 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
import .basic hott.types.sigma
import .basic
open path precategory sigma sigma.ops equiv is_equiv function truncation
open eq precategory sigma sigma.ops equiv is_equiv function truncation
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
:= mk : ∀{g}, g ∘ f = id → is_section f
inductive is_retraction [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, f ∘ g ≈ id → is_retraction f
:= 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
:= 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
@ -25,16 +25,16 @@ namespace morphism
postfix `⁻¹` := inverse
theorem inverse_compose (f : a ⟶ b) [H : is_iso f] : f⁻¹ ∘ f ≈ id :=
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 :=
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 :=
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 :=
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 :=
@ -50,74 +50,74 @@ namespace morphism
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' :=
(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
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
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
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
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
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_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' :=
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 :=
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 :=
theorem retraction_of_id : retraction_of (ID a) = id :=
retraction_eq_intro !id_compose
theorem section_of_id : section_of (ID a) ≈ id :=
theorem section_of_id : section_of (ID a) = id :=
section_eq_intro !id_compose
theorem iso_of_id : ID a⁻¹ ≈ id :=
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) :=
have aux : retraction_of g ∘ g ∘ f ≈ (retraction_of g ∘ g) ∘ f,
have aux : retraction_of g ∘ g ∘ f = (retraction_of g ∘ g) ∘ f,
from !assoc,
is_section.mk
(calc
(retraction_of f ∘ retraction_of g) ∘ g ∘ f
≈ retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc
... ≈ retraction_of f ∘ ((retraction_of g ∘ g) ∘ f) : aux
... ≈ retraction_of f ∘ id ∘ f : {retraction_compose g}
... ≈ retraction_of f ∘ f : id_left f
... ≈ id : retraction_compose f)
= retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc
... = retraction_of f ∘ ((retraction_of g ∘ g) ∘ f) : aux
... = retraction_of f ∘ id ∘ f : {retraction_compose g}
... = retraction_of f ∘ f : id_left f
... = id : retraction_compose f)
theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
: is_retraction (g ∘ f) :=
have aux : f ∘ section_of f ∘ section_of g ≈ (f ∘ section_of f) ∘ section_of g,
have aux : f ∘ section_of f ∘ section_of g = (f ∘ section_of f) ∘ section_of g,
from !assoc,
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 : aux
... ≈ g ∘ id ∘ section_of g : compose_section f
... ≈ g ∘ section_of g : id_left (section_of g)
... ≈ id : compose_section)
= g ∘ f ∘ section_of f ∘ section_of g : assoc
... = g ∘ (f ∘ section_of f) ∘ section_of g : aux
... = 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
@ -147,38 +147,38 @@ namespace morphism
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
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
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
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
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)
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)
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?
@ -188,18 +188,18 @@ namespace morphism
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 calc g ∘ (f ∘ h₁) ≈ (g ∘ f) ∘ h₁ : !assoc
... ≈ (g ∘ f) ∘ h₂ : H
... ≈ g ∘ (f ∘ h₂) : !assoc, mono_elim (mono_elim H2))
have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂),
from calc g ∘ (f ∘ h₁) = (g ∘ f) ∘ h₁ : !assoc
... = (g ∘ f) ∘ h₂ : H
... = g ∘ (f ∘ h₂) : !assoc, 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 calc (h₁ ∘ g) ∘ f ≈ h₁ ∘ g ∘ f : !assoc
... ≈ h₂ ∘ g ∘ f : H
... ≈ (h₂ ∘ g) ∘ f: !assoc, epi_elim (epi_elim H2))
have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f,
from calc (h₁ ∘ g) ∘ f = h₁ ∘ g ∘ f : !assoc
... = h₂ ∘ g ∘ f : H
... = (h₂ ∘ g) ∘ f: !assoc, epi_elim (epi_elim H2))
end morphism
namespace morphism
@ -212,33 +212,33 @@ namespace morphism
(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 :=
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 :=
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 :=
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 :=
(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
(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,
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
@ -246,9 +246,9 @@ namespace morphism
-- (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⁻¹)
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
@ -260,22 +260,22 @@ namespace morphism
{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⁻¹)⁻¹
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

32
hott/algebra/precategory/natural_transformation.hlean
View file

@ -2,12 +2,12 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn, Jakob von Raumer
import .functor hott.axioms.funext hott.types.pi hott.types.sigma
open precategory path functor truncation equiv sigma.ops sigma is_equiv function pi
import .functor types.pi
open eq precategory functor truncation equiv sigma.ops sigma is_equiv function pi
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),
(nat : Π {a b : C} (f : hom a b), G f ∘ η a = η b ∘ F f),
natural_transformation F G
infixl `⟹`:25 := natural_transformation -- \==>
@ -18,11 +18,11 @@ namespace natural_transformation
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 :=
theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f :=
rec (λ x y, y) η
protected definition sigma_char :
(Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a ≈ η b ∘ F f) ≃ (F ⟹ G) :=
(Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a = η b ∘ F f) ≃ (F ⟹ G) :=
/-equiv.mk (λ S, natural_transformation.mk S.1 S.2)
(adjointify (λ S, natural_transformation.mk S.1 S.2)
(λ H, natural_transformation.rec_on H (λ η nat, dpair η nat))
@ -47,19 +47,19 @@ namespace natural_transformation
(λ 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)
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
protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext fext2 fext3 : funext] :
η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ :=
η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
-- Proof broken, universe issues?
/-have aux [visible] : is_hprop (Π (a b : C) (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a ≈ ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
/-have aux [visible] : is_hprop (Π (a b : C) (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a = ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
begin
repeat (apply trunc_pi; intros),
apply (succ_is_trunc -1 (I a_2 ∘ (η₃ ∘n η₂) a ∘ η₁ a)),
@ -72,13 +72,13 @@ namespace natural_transformation
protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F := id
protected definition id_left (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
id ∘n η ≈ η :=
id ∘n η = η :=
--Proof broken like all trunc_pi proofs
/-begin
apply (rec_on η), intros (f, H),
fapply (path.dcongr_arg2 mk),
apply (funext.path_forall _ f (λa, !id_left)),
assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a ≈ f b ∘ F g)),
assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a = f b ∘ F g)),
--repeat (apply trunc_pi; intros),
apply (@trunc_pi _ _ _ (-2 .+1) _),
/- apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)),
@ -87,13 +87,13 @@ namespace natural_transformation
sorry
protected definition id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
η ∘n id ≈ η :=
η ∘n id = η :=
--Proof broken like all trunc_pi proofs
/-begin
apply (rec_on η), intros (f, H),
fapply (path.dcongr_arg2 mk),
apply (funext.path_forall _ f (λa, !id_right)),
assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a ≈ f b ∘ F g)),
assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a = f b ∘ F g)),
repeat (apply trunc_pi; intros),
apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)),
apply (!is_hprop.elim),

1
hott/init/default.hlean
View file

@ -9,3 +9,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
import init.bool init.num init.priority init.relation init.wf
import init.types.sigma init.types.prod
import init.trunc init.path init.equiv
import init.axioms.funext

56
hott/types/W.hlean
View file

@ -7,11 +7,13 @@ Theorems about W-types (well-founded trees)
-/
import .sigma .pi
open path sigma sigma.ops equiv is_equiv
open eq sigma sigma.ops equiv is_equiv
-- TODO fix universe levels
exit
inductive Wtype {A : Type} (B : A → Type) :=
sup : Π(a : A), (B a → Wtype B) → Wtype B
inductive Wtype.{l k} {A : Type.{l}} (B : A → Type.{k}) :=
sup : Π (a : A), (B a → Wtype.{l k} B) → Wtype.{l k} B
namespace Wtype
notation `W` binders `,` r:(scoped B, Wtype B) := r
@ -33,21 +35,21 @@ namespace Wtype
end ops
open ops
protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ ≈ w :=
protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ = w :=
cases_on w (λa f, idp)
definition path_W_sup (p : a ≈ a') (q : p ▹ f ≈ f') : ⟨a, f⟩ ≈ ⟨a', f'⟩ :=
definition path_W_sup (p : a = a') (q : p ▹ f = f') : ⟨a, f⟩ = ⟨a', f'⟩ :=
path.rec_on p (λf' q, path.rec_on q idp) f' q
definition path_W (p : w.1 ≈ w'.1) (q : p ▹ w.2 ≈ w'.2) : w ≈ w' :=
definition path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : w = w' :=
cases_on w
(λw1 w2, cases_on w' (λ w1' w2', path_W_sup))
p q
definition pr1_path (p : w ≈ w') : w.1 ≈ w'.1 :=
definition pr1_path (p : w = w') : w.1 = w'.1 :=
path.rec_on p idp
definition pr2_path (p : w ≈ w') : pr1_path p ▹ w.2 ≈ w'.2 :=
definition pr2_path (p : w = w') : pr1_path p ▹ w.2 = w'.2 :=
path.rec_on p idp
namespace ops
@ -56,8 +58,8 @@ namespace Wtype
end ops
open ops
definition sup_path_W (p : w.1 ≈ w'.1) (q : p ▹ w.2 ≈ w'.2)
: dpair (path_W p q)..1 (path_W p q)..2 ≈ dpair p q :=
definition sup_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
: dpair (path_W p q)..1 (path_W p q)..2 = dpair p q :=
begin
reverts (p, q),
apply (cases_on w), intros (w1, w2),
@ -66,22 +68,22 @@ namespace Wtype
apply (path.rec_on q), apply idp
end
definition pr1_path_W (p : w.1 ≈ w'.1) (q : p ▹ w.2 ≈ w'.2) : (path_W p q)..1 ≈ p :=
definition pr1_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2) : (path_W p q)..1 = p :=
(!sup_path_W)..1
definition pr2_path_W (p : w.1 ≈ w'.1) (q : p ▹ w.2 ≈ w'.2)
: pr1_path_W p q ▹ (path_W p q)..2 ≈ q :=
definition pr2_path_W (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
: pr1_path_W p q ▹ (path_W p q)..2 = q :=
(!sup_path_W)..2
definition eta_path_W (p : w ≈ w') : path_W (p..1) (p..2) ≈ p :=
definition eta_path_W (p : w = w') : path_W (p..1) (p..2) = p :=
begin
apply (path.rec_on p),
apply (cases_on w), intros (w1, w2),
apply idp
end
definition transport_pr1_path_W {B' : A → Type} (p : w.1 ≈ w'.1) (q : p ▹ w.2 ≈ w'.2)
: transport (λx, B' x.1) (path_W p q) ≈ transport B' p :=
definition transport_pr1_path_W {B' : A → Type} (p : w.1 = w'.1) (q : p ▹ w.2 = w'.2)
: transport (λx, B' x.1) (path_W p q) = transport B' p :=
begin
reverts (p, q),
apply (cases_on w), intros (w1, w2),
@ -90,26 +92,26 @@ namespace Wtype
apply (path.rec_on q), apply idp
end
definition path_W_uncurried (pq : Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2) : w ≈ w' :=
definition path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2) : w = w' :=
destruct pq path_W
definition sup_path_W_uncurried (pq : Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2)
: dpair (path_W_uncurried pq)..1 (path_W_uncurried pq)..2 ≈ pq :=
definition sup_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
: dpair (path_W_uncurried pq)..1 (path_W_uncurried pq)..2 = pq :=
destruct pq sup_path_W
definition pr1_path_W_uncurried (pq : Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2)
: (path_W_uncurried pq)..1 ≈ pq.1 :=
definition pr1_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
: (path_W_uncurried pq)..1 = pq.1 :=
(!sup_path_W_uncurried)..1
definition pr2_path_W_uncurried (pq : Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2)
: (pr1_path_W_uncurried pq) ▹ (path_W_uncurried pq)..2 ≈ pq.2 :=
definition pr2_path_W_uncurried (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
: (pr1_path_W_uncurried pq) ▹ (path_W_uncurried pq)..2 = pq.2 :=
(!sup_path_W_uncurried)..2
definition eta_path_W_uncurried (p : w ≈ w') : path_W_uncurried (dpair p..1 p..2) ≈ p :=
definition eta_path_W_uncurried (p : w = w') : path_W_uncurried (dpair p..1 p..2) = p :=
!eta_path_W
definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2)
: transport (λx, B' x.1) (@path_W_uncurried A B w w' pq) ≈ transport B' pq.1 :=
definition transport_pr1_path_W_uncurried {B' : A → Type} (pq : Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2)
: transport (λx, B' x.1) (@path_W_uncurried A B w w' pq) = transport B' pq.1 :=
destruct pq transport_pr1_path_W
definition isequiv_path_W /-[instance]-/ (w w' : W a, B a)
@ -119,7 +121,7 @@ namespace Wtype
eta_path_W_uncurried
sup_path_W_uncurried
definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 ≈ w'.1), p ▹ w.2 ≈ w'.2) ≃ (w ≈ w') :=
definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 = w'.1), p ▹ w.2 = w'.2) ≃ (w = w') :=
equiv.mk path_W_uncurried !isequiv_path_W
definition double_induction_on {P : (W a, B a) → (W a, B a) → Type} (w w' : W a, B a)

3
hott/types/pi.hlean
View file

@ -6,7 +6,8 @@ Ported from Coq HoTT
Theorems about pi-types (dependent function spaces)
-/
import init.equiv init.axioms.funext types.sigma
import types.sigma
open eq equiv is_equiv funext
namespace pi

4
hott/types/sigma.hlean
View file

@ -6,8 +6,8 @@ Ported from Coq HoTT
Theorems about sigma-types (dependent sums)
-/
import types.prod
import init.trunc init.axioms.funext init.types.prod
open eq sigma sigma.ops equiv is_equiv
namespace sigma
@ -400,7 +400,7 @@ namespace sigma
: is_equiv (@sigma.rec _ _ C) :=
adjointify _ (λ g a b, g ⟨a, b⟩)
(λ g, proof path_pi (λu, destruct u (λa b, idp)) qed)
(λ f, idpath f)
(λ f, refl f)
definition equiv_sigma_rec [FUN : funext] (C : (Σa, B a) → Type)
: (Π(a : A) (b: B a), C ⟨a, b⟩) ≃ (Πxy, C xy) :=