chore(hott) delete old hott lib
This commit is contained in:
Jakob von Raumer
Leonardo de Moura
parent
402622ac91
commit
25a5e29b7c
28 changed files with 0 additions and 4492 deletions
|
|
@ -1,75 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.binary
|
||||
Authors: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
General properties of binary operations.
|
||||
-/
|
||||
|
||||
import hott.path
|
||||
open path
|
||||
|
||||
namespace path_binary
|
||||
section
|
||||
variable {A : Type}
|
||||
variables (op₁ : A → A → A) (inv : A → A) (one : A)
|
||||
|
||||
notation [local] a * b := op₁ a b
|
||||
notation [local] a ⁻¹ := inv a
|
||||
notation [local] 1 := one
|
||||
|
||||
definition commutative := ∀a b, a*b ≈ b*a
|
||||
definition associative := ∀a b c, (a*b)*c ≈ a*(b*c)
|
||||
definition left_identity := ∀a, 1 * a ≈ a
|
||||
definition right_identity := ∀a, a * 1 ≈ a
|
||||
definition left_inverse := ∀a, a⁻¹ * a ≈ 1
|
||||
definition right_inverse := ∀a, a * a⁻¹ ≈ 1
|
||||
definition left_cancelative := ∀a b c, a * b ≈ a * c → b ≈ c
|
||||
definition right_cancelative := ∀a b c, a * b ≈ c * b → a ≈ c
|
||||
|
||||
definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) ≈ b
|
||||
definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) ≈ b
|
||||
definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b ≈ a
|
||||
definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ ≈ a
|
||||
|
||||
variable (op₂ : A → A → A)
|
||||
|
||||
notation [local] a + b := op₂ a b
|
||||
|
||||
definition left_distributive := ∀a b c, a * (b + c) ≈ a * b + a * c
|
||||
definition right_distributive := ∀a b c, (a + b) * c ≈ a * c + b * c
|
||||
end
|
||||
|
||||
context
|
||||
variable {A : Type}
|
||||
variable {f : A → A → A}
|
||||
variable H_comm : commutative f
|
||||
variable H_assoc : associative f
|
||||
infixl `*` := f
|
||||
theorem left_comm : ∀a b c, a*(b*c) ≈ b*(a*c) :=
|
||||
take a b c, calc
|
||||
a*(b*c) ≈ (a*b)*c : H_assoc
|
||||
... ≈ (b*a)*c : H_comm
|
||||
... ≈ b*(a*c) : H_assoc
|
||||
|
||||
theorem right_comm : ∀a b c, (a*b)*c ≈ (a*c)*b :=
|
||||
take a b c, calc
|
||||
(a*b)*c ≈ a*(b*c) : H_assoc
|
||||
... ≈ a*(c*b) : H_comm
|
||||
... ≈ (a*c)*b : H_assoc
|
||||
end
|
||||
|
||||
context
|
||||
variable {A : Type}
|
||||
variable {f : A → A → A}
|
||||
variable H_assoc : associative f
|
||||
infixl `*` := f
|
||||
theorem assoc4helper (a b c d) : (a*b)*(c*d) ≈ a*((b*c)*d) :=
|
||||
calc
|
||||
(a*b)*(c*d) ≈ a*(b*(c*d)) : H_assoc
|
||||
... ≈ a*((b*c)*d) : H_assoc
|
||||
end
|
||||
|
||||
end path_binary
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- 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
|
||||
|
||||
-- A category is a precategory extended by a witness,
|
||||
-- that the function assigning to each isomorphism a path,
|
||||
-- is an equivalecnce.
|
||||
structure category [class] (ob : Type) extends (precategory ob) :=
|
||||
(iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
|
||||
|
||||
namespace category
|
||||
variables {ob : Type} {C : category ob} {a b : ob}
|
||||
include C
|
||||
|
||||
-- Make iso_of_path_equiv a class instance
|
||||
-- TODO: Unsafe class instance?
|
||||
instance [persistent] iso_of_path_equiv
|
||||
|
||||
definition path_of_iso {a b : ob} : a ≅ b → a ≈ b :=
|
||||
iso_of_path⁻¹
|
||||
|
||||
definition ob_1_type : is_trunc nat.zero .+1 ob :=
|
||||
begin
|
||||
apply is_trunc_succ, intros (a, b),
|
||||
fapply trunc_equiv,
|
||||
exact (@path_of_iso _ _ a b),
|
||||
apply inv_closed,
|
||||
apply is_hset_iso,
|
||||
end
|
||||
|
||||
end category
|
||||
|
||||
-- Bundled version of categories
|
||||
inductive Category : Type := mk : Π (ob : Type), category ob → Category
|
||||
|
|
@ -1,567 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.group
|
||||
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
|
||||
|
||||
open path truncation path_binary -- note: ⁻¹ will be overloaded
|
||||
|
||||
namespace path_algebra
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
/- overloaded symbols -/
|
||||
structure has_mul [class] (A : Type) :=
|
||||
(mul : A → A → A)
|
||||
|
||||
structure has_add [class] (A : Type) :=
|
||||
(add : A → A → A)
|
||||
|
||||
structure has_one [class] (A : Type) :=
|
||||
(one : A)
|
||||
|
||||
structure has_zero [class] (A : Type) :=
|
||||
(zero : A)
|
||||
|
||||
structure has_inv [class] (A : Type) :=
|
||||
(inv : A → A)
|
||||
|
||||
structure has_neg [class] (A : Type) :=
|
||||
(neg : A → A)
|
||||
|
||||
infixl `*` := has_mul.mul
|
||||
infixl `+` := has_add.add
|
||||
postfix `⁻¹` := has_inv.inv
|
||||
prefix `-` := has_neg.neg
|
||||
notation 1 := !has_one.one
|
||||
notation 0 := !has_zero.zero
|
||||
|
||||
|
||||
/- semigroup -/
|
||||
|
||||
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))
|
||||
|
||||
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)
|
||||
|
||||
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_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
|
||||
|
||||
structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
|
||||
(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 :=
|
||||
!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)
|
||||
|
||||
theorem mul_right_cancel [s : right_cancel_semigroup A] {a b c : A} :
|
||||
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))
|
||||
|
||||
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)
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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)
|
||||
|
||||
theorem add_left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
|
||||
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)
|
||||
|
||||
theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
|
||||
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)
|
||||
|
||||
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
|
||||
|
||||
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)
|
||||
|
||||
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
|
||||
|
||||
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
|
||||
|
||||
|
||||
|
||||
/- group -/
|
||||
|
||||
structure group [class] (A : Type) extends monoid A, has_inv A :=
|
||||
(mul_left_inv : ∀a, mul (inv a) a ≈ one)
|
||||
|
||||
-- Note: with more work, we could derive the axiom mul_left_id
|
||||
|
||||
section group
|
||||
|
||||
variable [s : group A]
|
||||
include s
|
||||
|
||||
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 :=
|
||||
calc
|
||||
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 :=
|
||||
calc
|
||||
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 :=
|
||||
calc
|
||||
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_inv (a : A) : (a⁻¹)⁻¹ ≈ a := inv_unique (mul_left_inv a)
|
||||
|
||||
theorem inv_inj {a b : A} (H : a⁻¹ ≈ b⁻¹) : a ≈ b :=
|
||||
calc
|
||||
a ≈ (a⁻¹)⁻¹ : inv_inv
|
||||
... ≈ b : inv_unique (H⁻¹ ▹ (mul_left_inv _))
|
||||
|
||||
--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 :=
|
||||
--inv_one ▹ !inv_eq_inv_iff_eq
|
||||
|
||||
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⁻¹ :=
|
||||
--iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv
|
||||
|
||||
theorem mul_right_inv (a : A) : a * a⁻¹ ≈ 1 :=
|
||||
calc
|
||||
a * a⁻¹ ≈ (a⁻¹)⁻¹ * a⁻¹ : inv_inv
|
||||
... ≈ 1 : mul_left_inv
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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)
|
||||
|
||||
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
|
||||
|
||||
-- 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⁻¹ :=
|
||||
H ▹ !mul_inv_cancel_right⁻¹
|
||||
|
||||
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 :=
|
||||
H⁻¹ ▹ !inv_mul_cancel_left
|
||||
|
||||
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 :=
|
||||
!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 :=
|
||||
!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 :=
|
||||
!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 :=
|
||||
!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 :=
|
||||
--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⁻¹ :=
|
||||
--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,
|
||||
calc
|
||||
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,
|
||||
calc
|
||||
a ≈ (a * b) * b⁻¹ : mul_inv_cancel_right
|
||||
... ≈ (c * b) * b⁻¹ : H
|
||||
... ≈ c : mul_inv_cancel_right)
|
||||
|
||||
end group
|
||||
|
||||
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)
|
||||
|
||||
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 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
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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_inj {a b : A} (H : -a ≈ -b) : a ≈ b :=
|
||||
calc
|
||||
a ≈ -(-a) : neg_neg
|
||||
... ≈ b : neg_unique (H⁻¹ ▹ (add_left_inv _))
|
||||
|
||||
--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 :=
|
||||
--neg_zero ▹ !neg_eq_neg_iff_eq
|
||||
|
||||
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 :=
|
||||
--iff.intro !eq_neg_imp_eq_neg !eq_neg_imp_eq_neg
|
||||
|
||||
theorem add_right_inv (a : A) : a + -a ≈ 0 :=
|
||||
calc
|
||||
a + -a ≈ -(-a) + -a : neg_neg
|
||||
... ≈ 0 : add_left_inv
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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)
|
||||
|
||||
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 :=
|
||||
H ▹ !neg_add_cancel_left⁻¹
|
||||
|
||||
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 :=
|
||||
H⁻¹ ▹ !add_neg_cancel_right
|
||||
|
||||
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 :=
|
||||
!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 :=
|
||||
!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 :=
|
||||
!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 :=
|
||||
--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 :=
|
||||
--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,
|
||||
calc
|
||||
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,
|
||||
calc
|
||||
a ≈ (a + b) + -b : add_neg_cancel_right
|
||||
... ≈ (c + b) + -b : H
|
||||
... ≈ c : add_neg_cancel_right)
|
||||
|
||||
/- minus -/
|
||||
|
||||
-- TODO: derive corresponding facts for div in a field
|
||||
definition minus (a b : A) : A := a + -b
|
||||
|
||||
infix `-` := minus
|
||||
|
||||
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 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 :=
|
||||
calc
|
||||
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 :=
|
||||
--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 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 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)
|
||||
|
||||
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 :=
|
||||
calc
|
||||
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 :=
|
||||
--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 :=
|
||||
--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 :=
|
||||
--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)
|
||||
|
||||
end add_group
|
||||
|
||||
structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
|
||||
|
||||
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 :=
|
||||
!add_comm ▹ !minus_add_eq_minus_swap
|
||||
|
||||
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 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) :=
|
||||
calc
|
||||
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 :=
|
||||
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
|
||||
|
||||
|
||||
end add_comm_group
|
||||
|
||||
|
||||
/- bundled structures -/
|
||||
|
||||
structure Semigroup :=
|
||||
(carrier : Type) (struct : semigroup carrier)
|
||||
|
||||
coercion Semigroup.carrier
|
||||
instance Semigroup.struct
|
||||
|
||||
structure CommSemigroup :=
|
||||
(carrier : Type) (struct : comm_semigroup carrier)
|
||||
|
||||
coercion CommSemigroup.carrier
|
||||
instance CommSemigroup.struct
|
||||
|
||||
structure Monoid :=
|
||||
(carrier : Type) (struct : monoid carrier)
|
||||
|
||||
coercion Monoid.carrier
|
||||
instance Monoid.struct
|
||||
|
||||
structure CommMonoid :=
|
||||
(carrier : Type) (struct : comm_monoid carrier)
|
||||
|
||||
coercion CommMonoid.carrier
|
||||
instance CommMonoid.struct
|
||||
|
||||
structure Group :=
|
||||
(carrier : Type) (struct : group carrier)
|
||||
|
||||
coercion Group.carrier
|
||||
instance Group.struct
|
||||
|
||||
structure CommGroup :=
|
||||
(carrier : Type) (struct : comm_group carrier)
|
||||
|
||||
coercion CommGroup.carrier
|
||||
instance CommGroup.struct
|
||||
|
||||
structure AddSemigroup :=
|
||||
(carrier : Type) (struct : add_semigroup carrier)
|
||||
|
||||
coercion AddSemigroup.carrier
|
||||
instance AddSemigroup.struct
|
||||
|
||||
structure AddCommSemigroup :=
|
||||
(carrier : Type) (struct : add_comm_semigroup carrier)
|
||||
|
||||
coercion AddCommSemigroup.carrier
|
||||
instance AddCommSemigroup.struct
|
||||
|
||||
structure AddMonoid :=
|
||||
(carrier : Type) (struct : add_monoid carrier)
|
||||
|
||||
coercion AddMonoid.carrier
|
||||
instance AddMonoid.struct
|
||||
|
||||
structure AddCommMonoid :=
|
||||
(carrier : Type) (struct : add_comm_monoid carrier)
|
||||
|
||||
coercion AddCommMonoid.carrier
|
||||
instance AddCommMonoid.struct
|
||||
|
||||
structure AddGroup :=
|
||||
(carrier : Type) (struct : add_group carrier)
|
||||
|
||||
coercion AddGroup.carrier
|
||||
instance AddGroup.struct
|
||||
|
||||
structure AddCommGroup :=
|
||||
(carrier : Type) (struct : add_comm_group carrier)
|
||||
|
||||
coercion AddCommGroup.carrier
|
||||
instance AddCommGroup.struct
|
||||
|
||||
end path_algebra
|
||||
|
|
@ -1,87 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import .precategory.basic .precategory.morphism .group
|
||||
|
||||
open path function prod sigma truncation morphism nat path_algebra unit
|
||||
|
||||
structure foo (A : Type) := (bsp : A)
|
||||
|
||||
structure groupoid [class] (ob : Type) extends precategory ob :=
|
||||
(all_iso : Π ⦃a b : ob⦄ (f : hom a b),
|
||||
@is_iso ob (precategory.mk hom _ _ _ assoc id_left id_right) a b f)
|
||||
|
||||
namespace groupoid
|
||||
|
||||
instance [persistent] all_iso
|
||||
|
||||
--set_option pp.universes true
|
||||
--set_option pp.implicit true
|
||||
universe variable l
|
||||
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)
|
||||
!concat_pV !concat_Vp)
|
||||
|
||||
-- A groupoid with a contractible carrier is a group
|
||||
definition group_of_contr {ob : Type} (H : is_contr ob)
|
||||
(G : groupoid ob) : group (hom (center ob) (center ob)) :=
|
||||
begin
|
||||
fapply group.mk,
|
||||
intros (f, g), apply (comp f g),
|
||||
apply homH,
|
||||
intros (f, g, h), apply ((assoc f g h)⁻¹),
|
||||
apply (ID (center ob)),
|
||||
intro f, apply id_left,
|
||||
intro f, apply id_right,
|
||||
intro f, exact (morphism.inverse f),
|
||||
intro f, exact (morphism.inverse_compose f),
|
||||
end
|
||||
|
||||
definition group_of_unit (G : groupoid unit) : group (hom ⋆ ⋆) :=
|
||||
begin
|
||||
fapply group.mk,
|
||||
intros (f, g), apply (comp f g),
|
||||
apply homH,
|
||||
intros (f, g, h), apply ((assoc f g h)⁻¹),
|
||||
apply (ID ⋆),
|
||||
intro f, apply id_left,
|
||||
intro f, apply id_right,
|
||||
intro f, exact (morphism.inverse f),
|
||||
intro f, exact (morphism.inverse_compose f),
|
||||
end
|
||||
|
||||
-- Conversely we can turn each group into a groupoid on the unit type
|
||||
definition of_group (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
|
||||
begin
|
||||
fapply groupoid.mk,
|
||||
intros, exact A,
|
||||
intros, apply (@group.carrier_hset A G),
|
||||
intros (a, b, c, g, h), exact (@group.mul A G g h),
|
||||
intro a, exact (@group.one A G),
|
||||
intros, exact ((@group.mul_assoc A G h g f)⁻¹),
|
||||
intros, exact (@group.mul_left_id A G f),
|
||||
intros, exact (@group.mul_right_id A G f),
|
||||
intros, apply is_iso.mk,
|
||||
apply mul_left_inv,
|
||||
apply mul_right_inv,
|
||||
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 :=
|
||||
sorry
|
||||
|
||||
|
||||
end groupoid
|
||||
|
|
@ -1,64 +0,0 @@
|
|||
-- 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
|
||||
|
||||
structure precategory [class] (ob : Type) : Type :=
|
||||
(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)
|
||||
(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)
|
||||
|
||||
namespace precategory
|
||||
variables {ob : Type} [C : precategory ob]
|
||||
variables {a b c d : ob}
|
||||
include C
|
||||
instance [persistent] homH
|
||||
|
||||
definition compose := comp
|
||||
|
||||
definition id [reducible] {a : ob} : hom a a := ID a
|
||||
|
||||
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}
|
||||
|
||||
|
||||
--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 Precategory.equal (C : Precategory) : Precategory.mk C C ≈ C :=
|
||||
Precategory.rec (λ ob c, idp) C
|
||||
|
|
@ -1,368 +0,0 @@
|
|||
-- 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
|
||||
|
||||
-- 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
|
||||
|
||||
open path prod eq eq.ops
|
||||
|
||||
namespace precategory
|
||||
namespace opposite
|
||||
section
|
||||
definition opposite {ob : Type} (C : precategory ob) : precategory ob :=
|
||||
mk (λ a b, hom b a)
|
||||
(λ b a, !homH)
|
||||
(λ a b c f g, g ∘ f)
|
||||
(λ a, id)
|
||||
(λ a b c d f g h, !assoc⁻¹)
|
||||
(λ a b f, !id_right)
|
||||
(λ a b f, !id_left)
|
||||
|
||||
definition Opposite (C : Precategory) : Precategory := Mk (opposite C)
|
||||
|
||||
infixr `∘op`:60 := @compose _ (opposite _) _ _ _
|
||||
|
||||
variables {C : Precategory} {a b c : C}
|
||||
|
||||
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 :=
|
||||
sorry
|
||||
|
||||
theorem op_op : Opposite (Opposite C) ≈ C :=
|
||||
(ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal
|
||||
|
||||
end
|
||||
end opposite
|
||||
|
||||
/-definition type_category : precategory 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-/
|
||||
|
||||
-- Note: Discrete precategory doesn't really make sense in HoTT,
|
||||
-- We'll define a discrete _category_ later.
|
||||
/-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_precategory (A : Type) [H : decidable_eq A] : precategory 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 truncation
|
||||
|
||||
definition prod_precategory {obC obD : Type} (C : precategory obC) (D : precategory obD)
|
||||
: precategory (obC × obD) :=
|
||||
mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
|
||||
(λ a b, !trunc_prod)
|
||||
(λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
|
||||
(λ a, (id, id))
|
||||
(λ a b c d h g f, pair_path !assoc !assoc )
|
||||
(λ a b f, prod.path !id_left !id_left )
|
||||
(λ a b f, prod.path !id_right !id_right)
|
||||
|
||||
definition Prod_precategory (C D : Precategory) : Precategory := Mk (prod_precategory 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_precategory
|
||||
--instance [persistent] type_category category_one
|
||||
-- category_two product.prod_category
|
||||
instance [persistent] product.prod_precategory
|
||||
|
||||
end ops
|
||||
|
||||
open ops
|
||||
namespace opposite
|
||||
section
|
||||
open ops functor
|
||||
set_option pp.universes true
|
||||
|
||||
definition opposite_functor {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
|
||||
/-begin
|
||||
apply (@functor.mk (Cᵒᵖ) (Dᵒᵖ)),
|
||||
intro a, apply (respect_id F),
|
||||
intros, apply (@respect_comp C D)
|
||||
end-/ sorry
|
||||
|
||||
end
|
||||
end opposite
|
||||
|
||||
namespace product
|
||||
section
|
||||
open ops functor
|
||||
definition prod_functor {C C' D D' : Precategory} (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_path !respect_id !respect_id)
|
||||
(λ a b c g f, pair_path !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 : Precategory)
|
||||
definition functor_category [fx : funext] : precategory (functor C D) :=
|
||||
mk (λa b, natural_transformation a b)
|
||||
sorry --TODO: Prove that the nat trafos between two functors are an hset
|
||||
(λ 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 : precategory ob} {c : ob}
|
||||
protected definition slice_obs (C : precategory 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
|
||||
|
||||
/- TODO wait for some helping lemmas
|
||||
definition slice_category (C : precategory ob) (c : ob) : precategory (slice_obs C c) :=
|
||||
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,
|
||||
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_path !assoc sorry)
|
||||
(λ a b f, sigma.path !id_left sorry)
|
||||
(λ a b f, sigma.path !id_right sorry)
|
||||
-/
|
||||
|
||||
|
||||
-- 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
|
||||
|
||||
exit
|
||||
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)
|
||||
|
|
@ -1,149 +0,0 @@
|
|||
-- 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 categories.
|
||||
-- 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
|
||||
|
|
@ -1,68 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- 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
|
||||
|
||||
open path precategory sigma sigma.ops equiv is_equiv function truncation
|
||||
open prod
|
||||
|
||||
namespace morphism
|
||||
variables {ob : Type} [C : precategory ob] include C
|
||||
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 :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
intro S, apply is_iso.mk,
|
||||
exact (pr₁ S.2),
|
||||
exact (pr₂ S.2),
|
||||
fapply adjointify,
|
||||
intro H, apply (is_iso.rec_on H), intros (g, η, ε),
|
||||
exact (dpair g (pair η ε)),
|
||||
intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp,
|
||||
intro S, apply (sigma.rec_on S), intros (g, ηε),
|
||||
apply (prod.rec_on ηε), intros (η, ε), apply idp,
|
||||
end
|
||||
|
||||
-- The structure for isomorphism can be characterized up to equivalence
|
||||
-- by a sigma type.
|
||||
definition sigma_is_iso_equiv ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
intro S, apply isomorphic.mk, apply (S.2),
|
||||
fapply adjointify,
|
||||
intro p, apply (isomorphic.rec_on p), intros (f, H),
|
||||
exact (dpair f H),
|
||||
intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp,
|
||||
intro S, apply (sigma.rec_on S), intros (f, H), apply idp,
|
||||
end
|
||||
|
||||
-- The statement "f is an isomorphism" is a mere proposition
|
||||
definition is_hprop_of_is_iso : is_hset (is_iso f) :=
|
||||
begin
|
||||
apply trunc_equiv,
|
||||
apply (equiv.to_is_equiv (!sigma_char)),
|
||||
apply trunc_sigma,
|
||||
apply (!homH),
|
||||
intro g, apply trunc_prod,
|
||||
repeat (apply succ_is_trunc; apply trunc_succ; apply (!homH)),
|
||||
end
|
||||
|
||||
-- The type of isomorphisms between two objects is a set
|
||||
definition is_hset_iso : is_hset (a ≅ b) :=
|
||||
begin
|
||||
apply trunc_equiv,
|
||||
apply (equiv.to_is_equiv (!sigma_is_iso_equiv)),
|
||||
apply trunc_sigma,
|
||||
apply homH,
|
||||
intro f, apply is_hprop_of_is_iso,
|
||||
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)
|
||||
|
||||
end morphism
|
||||
|
|
@ -1,282 +0,0 @@
|
|||
-- 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 hott.types.sigma
|
||||
|
||||
open path 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
|
||||
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) :=
|
||||
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)
|
||||
|
||||
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,
|
||||
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)
|
||||
|
||||
theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
|
||||
!section_retraction_imp_iso
|
||||
|
||||
structure isomorphic (a b : ob) :=
|
||||
(iso : hom a b)
|
||||
[is_iso : is_iso iso]
|
||||
|
||||
infix `≅`:50 := morphism.isomorphic
|
||||
|
||||
namespace isomorphic
|
||||
|
||||
-- openrelation
|
||||
instance [persistent] is_iso
|
||||
|
||||
definition refl (a : ob) : a ≅ a :=
|
||||
mk id
|
||||
|
||||
definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
|
||||
mk (inverse (iso H))
|
||||
|
||||
definition 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 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))
|
||||
|
||||
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
|
||||
|
|
@ -1,115 +0,0 @@
|
|||
-- 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 hott.types.pi hott.types.sigma
|
||||
open precategory path 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),
|
||||
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 sigma_char :
|
||||
(Σ (η : Π (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))
|
||||
(λ H, natural_transformation.rec_on H (λ η nat, idpath (natural_transformation.mk η nat)))
|
||||
(λ S, sigma.rec_on S (λ η nat, idpath (dpair η nat))))-/
|
||||
|
||||
/- THE FOLLLOWING CAUSES LEAN TO SEGFAULT?
|
||||
begin
|
||||
fapply equiv.mk,
|
||||
intro S, apply natural_transformation.mk, exact (S.2),
|
||||
fapply adjointify,
|
||||
intro H, apply (natural_transformation.rec_on H), intros (η, natu),
|
||||
exact (dpair η @natu),
|
||||
intro H, apply (natural_transformation.rec_on _ _ _),
|
||||
intros,
|
||||
end
|
||||
check sigma_char-/
|
||||
sorry
|
||||
|
||||
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
|
||||
|
||||
protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext fext2 fext3 : funext] :
|
||||
η₃ ∘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),
|
||||
begin
|
||||
repeat (apply trunc_pi; intros),
|
||||
apply (succ_is_trunc -1 (I a_2 ∘ (η₃ ∘n η₂) a ∘ η₁ a)),
|
||||
end,
|
||||
dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) !is_hprop.elim-/
|
||||
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 definition id_left (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
|
||||
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)),
|
||||
--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)),
|
||||
apply (!is_hprop.elim),-/
|
||||
end-/
|
||||
sorry
|
||||
|
||||
protected definition id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
|
||||
η ∘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)),
|
||||
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),
|
||||
end-/
|
||||
sorry
|
||||
|
||||
protected definition to_hset [fx : funext] : is_hset (F ⟹ G) :=
|
||||
--Proof broken like all trunc_pi proofs
|
||||
/-begin
|
||||
apply trunc_equiv, apply (equiv.to_is_equiv sigma_char),
|
||||
apply trunc_sigma,
|
||||
apply trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)),
|
||||
intro η, apply trunc_pi, intro a,
|
||||
apply trunc_pi, intro b, apply trunc_pi, intro f,
|
||||
apply succ_is_trunc, apply trunc_succ, exact (@homH (objects D) _ (F a) (G b)),
|
||||
end-/
|
||||
sorry
|
||||
|
||||
end natural_transformation
|
||||
|
|
@ -1,122 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.relation
|
||||
Author: Jeremy Avigad
|
||||
|
||||
General properties of relations, and classes for equivalence relations and congruences.
|
||||
-/
|
||||
|
||||
namespace relation
|
||||
|
||||
/- properties of binary relations -/
|
||||
|
||||
section
|
||||
variables {T : Type} (R : T → T → Type)
|
||||
|
||||
definition reflexive : Type := Πx, R x x
|
||||
definition symmetric : Type := Π⦃x y⦄, R x y → R y x
|
||||
definition transitive : Type := Π⦃x y z⦄, R x y → R y z → R x z
|
||||
end
|
||||
|
||||
|
||||
/- classes for equivalence relations -/
|
||||
|
||||
structure is_reflexive [class] {T : Type} (R : T → T → Type) := (refl : reflexive R)
|
||||
structure is_symmetric [class] {T : Type} (R : T → T → Type) := (symm : symmetric R)
|
||||
structure is_transitive [class] {T : Type} (R : T → T → Type) := (trans : transitive R)
|
||||
|
||||
structure is_equivalence [class] {T : Type} (R : T → T → Type)
|
||||
extends is_reflexive R, is_symmetric R, is_transitive R
|
||||
|
||||
-- partial equivalence relation
|
||||
structure is_PER {T : Type} (R : T → T → Type) extends is_symmetric R, is_transitive R
|
||||
|
||||
-- Generic notation. For example, is_refl R is the reflexivity of R, if that can be
|
||||
-- inferred by type class inference
|
||||
section
|
||||
variables {T : Type} (R : T → T → Type)
|
||||
definition rel_refl [C : is_reflexive R] := is_reflexive.refl R
|
||||
definition rel_symm [C : is_symmetric R] := is_symmetric.symm R
|
||||
definition rel_trans [C : is_transitive R] := is_transitive.trans R
|
||||
end
|
||||
|
||||
|
||||
/- classes for unary and binary congruences with respect to arbitrary relations -/
|
||||
|
||||
structure is_congruence [class]
|
||||
{T1 : Type} (R1 : T1 → T1 → Type)
|
||||
{T2 : Type} (R2 : T2 → T2 → Type)
|
||||
(f : T1 → T2) :=
|
||||
(congr : Π{x y}, R1 x y → R2 (f x) (f y))
|
||||
|
||||
structure is_congruence2 [class]
|
||||
{T1 : Type} (R1 : T1 → T1 → Type)
|
||||
{T2 : Type} (R2 : T2 → T2 → Type)
|
||||
{T3 : Type} (R3 : T3 → T3 → Type)
|
||||
(f : T1 → T2 → T3) :=
|
||||
(congr2 : Π{x1 y1 : T1} {x2 y2 : T2}, R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2))
|
||||
|
||||
namespace is_congruence
|
||||
|
||||
-- makes the type class explicit
|
||||
definition app {T1 : Type} {R1 : T1 → T1 → Type} {T2 : Type} {R2 : T2 → T2 → Type}
|
||||
{f : T1 → T2} (C : is_congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
|
||||
is_congruence.rec (λu, u) C x y
|
||||
|
||||
definition app2 {T1 : Type} {R1 : T1 → T1 → Type} {T2 : Type} {R2 : T2 → T2 → Type}
|
||||
{T3 : Type} {R3 : T3 → T3 → Type}
|
||||
{f : T1 → T2 → T3} (C : is_congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
|
||||
R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
|
||||
is_congruence2.rec (λu, u) C x1 y1 x2 y2
|
||||
|
||||
/- tools to build instances -/
|
||||
|
||||
theorem compose
|
||||
{T2 : Type} {R2 : T2 → T2 → Type}
|
||||
{T3 : Type} {R3 : T3 → T3 → Type}
|
||||
{g : T2 → T3} (C2 : is_congruence R2 R3 g)
|
||||
⦃T1 : Type⦄ {R1 : T1 → T1 → Type}
|
||||
{f : T1 → T2} (C1 : is_congruence R1 R2 f) :
|
||||
is_congruence R1 R3 (λx, g (f x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app C2 (app C1 H))
|
||||
|
||||
theorem compose21
|
||||
{T2 : Type} {R2 : T2 → T2 → Type}
|
||||
{T3 : Type} {R3 : T3 → T3 → Type}
|
||||
{T4 : Type} {R4 : T4 → T4 → Type}
|
||||
{g : T2 → T3 → T4} (C3 : is_congruence2 R2 R3 R4 g)
|
||||
⦃T1 : Type⦄ {R1 : T1 → T1 → Type}
|
||||
{f1 : T1 → T2} (C1 : is_congruence R1 R2 f1)
|
||||
{f2 : T1 → T3} (C2 : is_congruence R1 R3 f2) :
|
||||
is_congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
|
||||
is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
|
||||
|
||||
theorem const {T2 : Type} (R2 : T2 → T2 → Type) (H : relation.reflexive R2)
|
||||
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.mk (λx y H1, H c)
|
||||
|
||||
end is_congruence
|
||||
|
||||
theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Type)
|
||||
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
|
||||
is_congruence R1 R2 (λu : T1, c) :=
|
||||
is_congruence.const R2 (is_reflexive.refl R2) R1 c
|
||||
|
||||
theorem congruence_trivial [instance] {T : Type} (R : T → T → Type) :
|
||||
is_congruence R R (λu, u) :=
|
||||
is_congruence.mk (λx y H, H)
|
||||
|
||||
|
||||
/- relations that can be coerced to functions / implications-/
|
||||
|
||||
structure mp_like [class] (R : Type → Type → Type) :=
|
||||
(app : Π{a b : Type}, R a b → (a → b))
|
||||
|
||||
definition rel_mp (R : Type → Type → Type) [C : mp_like R] {a b : Type} (H : R a b) :=
|
||||
mp_like.app H
|
||||
|
||||
|
||||
end relation
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad, Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
import hott.path hott.equiv
|
||||
open path
|
||||
|
||||
-- Funext
|
||||
-- ------
|
||||
|
||||
-- Define function extensionality as a type class
|
||||
inductive funext [class] : Type :=
|
||||
mk : (Π (A : Type) (P : A → Type ) (f g : Π x, P x), is_equiv (@apD10 A P f g))
|
||||
→ funext
|
||||
|
||||
namespace funext
|
||||
|
||||
universe variables l k
|
||||
variables [F : funext.{l k}] {A : Type.{l}} {P : A → Type.{k}}
|
||||
|
||||
include F
|
||||
protected definition ap [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) :=
|
||||
rec_on F (λ(H : Π A P f g, _), !H)
|
||||
|
||||
definition path_pi {f g : Π x, P x} : f ∼ g → f ≈ g :=
|
||||
is_equiv.inv (@apD10 A P f g)
|
||||
|
||||
omit F
|
||||
definition path_pi2 [F : funext] {A B : Type} {P : A → B → Type}
|
||||
(f g : Πx y, P x y) : (Πx y, f x y ≈ g x y) → f ≈ g :=
|
||||
λ E, path_pi (λx, path_pi (E x))
|
||||
|
||||
end funext
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import hott.path hott.equiv
|
||||
open path equiv
|
||||
|
||||
--Ensure that the types compared are in the same universe
|
||||
section
|
||||
universe variable l
|
||||
variables {A B : Type.{l}}
|
||||
|
||||
definition isequiv_path (H : A ≈ B) :=
|
||||
(@is_equiv.transport Type (λX, X) A B H)
|
||||
|
||||
definition equiv_path (H : A ≈ B) : A ≃ B :=
|
||||
equiv.mk _ (isequiv_path H)
|
||||
|
||||
end
|
||||
|
||||
inductive ua_type [class] : Type :=
|
||||
mk : (Π (A B : Type), is_equiv (@equiv_path A B)) → ua_type
|
||||
|
||||
namespace ua_type
|
||||
|
||||
context
|
||||
universe k
|
||||
parameters [F : ua_type.{k}] {A B: Type.{k}}
|
||||
|
||||
-- Make the Equivalence given by the axiom an instance
|
||||
protected definition inst [instance] : is_equiv (@equiv_path.{k} A B) :=
|
||||
rec_on F (λ H, H A B)
|
||||
|
||||
-- This is the version of univalence axiom we will probably use most often
|
||||
definition ua : A ≃ B → A ≈ B :=
|
||||
@is_equiv.inv _ _ (@equiv_path A B) inst
|
||||
|
||||
end
|
||||
|
||||
end ua_type
|
||||
|
||||
-- One consequence of UA is that we can transport along equivalencies of types
|
||||
namespace Equiv
|
||||
universe variable l
|
||||
|
||||
protected definition subst [UA : ua_type] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
|
||||
: P A → P B :=
|
||||
path.transport P (ua_type.ua H)
|
||||
|
||||
-- We can use this for calculation evironments
|
||||
calc_subst subst
|
||||
|
||||
end Equiv
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
-- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
|
||||
-- hott.default
|
||||
-- ============
|
||||
|
||||
-- A library for homotopy type theory
|
||||
|
||||
import ..standard .path .equiv .trunc .fibrant
|
||||
|
|
@ -1,266 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad, Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import .path
|
||||
open path function
|
||||
|
||||
-- Equivalences
|
||||
-- ------------
|
||||
|
||||
-- This is our definition of equivalence. In the HoTT-book it's called
|
||||
-- ihae (half-adjoint equivalence).
|
||||
structure is_equiv [class] {A B : Type} (f : A → B) :=
|
||||
(inv : B → A)
|
||||
(retr : (f ∘ inv) ∼ id)
|
||||
(sect : (inv ∘ f) ∼ id)
|
||||
(adj : Πx, retr (f x) ≈ ap f (sect x))
|
||||
|
||||
|
||||
-- A more bundled version of equivalence to calculate with
|
||||
structure equiv (A B : Type) :=
|
||||
(to_fun : A → B)
|
||||
(to_is_equiv : is_equiv to_fun)
|
||||
|
||||
-- Some instances and closure properties of equivalences
|
||||
namespace is_equiv
|
||||
|
||||
postfix `⁻¹` := inv
|
||||
|
||||
variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
|
||||
|
||||
-- The identity function is an equivalence.
|
||||
definition id_is_equiv : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
|
||||
|
||||
-- The composition of two equivalences is, again, an equivalence.
|
||||
protected definition compose [Hf : is_equiv f] [Hg : is_equiv g] : (is_equiv (g ∘ f)) :=
|
||||
is_equiv.mk ((inv f) ∘ (inv g))
|
||||
(λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
|
||||
(λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
|
||||
(λa, (whiskerL _ (adj g (f a))) ⬝
|
||||
(ap_pp g _ _)⁻¹ ⬝
|
||||
ap02 g (concat_A1p (retr f) (sect g (f a))⁻¹ ⬝
|
||||
(ap_compose (inv f) f _ ◾ adj f a) ⬝
|
||||
(ap_pp f _ _)⁻¹
|
||||
) ⬝
|
||||
(ap_compose f g _)⁻¹
|
||||
)
|
||||
|
||||
-- Any function equal to an equivalence is an equivlance as well.
|
||||
definition path_closed [Hf : is_equiv f] (Heq : f ≈ f') : (is_equiv f') :=
|
||||
path.rec_on Heq Hf
|
||||
|
||||
-- Any function pointwise equal to an equivalence is an equivalence as well.
|
||||
definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
|
||||
let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ retr f b) in
|
||||
let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ sect f a) in
|
||||
let adj' := (λ (a : A),
|
||||
let ff'a := Hty a in
|
||||
let invf := inv f in
|
||||
let secta := sect f a in
|
||||
let retrfa := retr f (f a) in
|
||||
let retrf'a := retr f (f' a) in
|
||||
have eq1 : _ ≈ _,
|
||||
from calc ap f secta ⬝ ff'a
|
||||
≈ retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _)
|
||||
... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p
|
||||
... ≈ ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f,
|
||||
have eq2 : _ ≈ _,
|
||||
from calc retrf'a
|
||||
≈ (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹)
|
||||
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a
|
||||
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap
|
||||
... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p
|
||||
... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V
|
||||
... ≈ (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap
|
||||
... ≈ (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V
|
||||
... ≈ Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p,
|
||||
have eq3 : _ ≈ _,
|
||||
from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
|
||||
≈ (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2
|
||||
... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V
|
||||
... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp,
|
||||
eq3) in
|
||||
is_equiv.mk (inv f) sect' retr' adj'
|
||||
end is_equiv
|
||||
|
||||
namespace is_equiv
|
||||
context
|
||||
parameters {A B : Type} (f : A → B) (g : B → A)
|
||||
(ret : f ∘ g ∼ id) (sec : g ∘ f ∼ id)
|
||||
|
||||
definition adjointify_sect' : g ∘ f ∼ id :=
|
||||
(λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
|
||||
|
||||
definition adjointify_adj' : Π (x : A), ret (f x) ≈ ap f (adjointify_sect' x) :=
|
||||
(λ (a : A),
|
||||
let fgretrfa := ap f (ap g (ret (f a))) in
|
||||
let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in
|
||||
let fgfa := f (g (f a)) in
|
||||
let retrfa := ret (f a) in
|
||||
have eq1 : ap f (sec a) ≈ _,
|
||||
from calc ap f (sec a)
|
||||
≈ idp ⬝ ap f (sec a) : !concat_1p⁻¹
|
||||
... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV
|
||||
... ≈ ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
|
||||
... ≈ ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
|
||||
... ≈ (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,
|
||||
have eq2 : ap f (sec a) ⬝ idp ≈ (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
|
||||
from !concat_p1 ⬝ eq1,
|
||||
have eq3 : idp ≈ _,
|
||||
from calc idp
|
||||
≈ (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2
|
||||
... ≈ (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp
|
||||
... ≈ (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹}
|
||||
... ≈ ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp
|
||||
... ≈ ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
|
||||
... ≈ ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
|
||||
... ≈ (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹}
|
||||
... ≈ retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹}
|
||||
... ≈ retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹
|
||||
... ≈ retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹},
|
||||
have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
|
||||
from moveR_M1 _ _ eq3,
|
||||
eq4)
|
||||
|
||||
definition adjointify : is_equiv f :=
|
||||
is_equiv.mk g ret adjointify_sect' adjointify_adj'
|
||||
|
||||
end
|
||||
end is_equiv
|
||||
|
||||
namespace is_equiv
|
||||
variables {A B: Type} (f : A → B)
|
||||
|
||||
--The inverse of an equivalence is, again, an equivalence.
|
||||
definition inv_closed [instance] [Hf : is_equiv f] : (is_equiv (inv f)) :=
|
||||
adjointify (inv f) f (sect f) (retr f)
|
||||
|
||||
end is_equiv
|
||||
|
||||
namespace is_equiv
|
||||
variables {A : Type}
|
||||
section
|
||||
variables {B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f]
|
||||
include Hf
|
||||
|
||||
definition cancel_R (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
|
||||
have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f,
|
||||
@homotopy_closed _ _ _ _ (compose (f⁻¹) (g ∘ f)) (λb, ap g (@retr _ _ f _ b))
|
||||
|
||||
definition cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
|
||||
have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f,
|
||||
@homotopy_closed _ _ _ _ (compose (f ∘ g) (f⁻¹)) (λa, sect f (g a))
|
||||
|
||||
--Rewrite rules
|
||||
definition moveR_M {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) :=
|
||||
(ap f p) ⬝ (@retr _ _ f _ y)
|
||||
|
||||
definition moveL_M {x : A} {y : B} (p : (inv f) y ≈ x) : (y ≈ f x) :=
|
||||
(moveR_M f (p⁻¹))⁻¹
|
||||
|
||||
definition moveR_V {x : B} {y : A} (p : x ≈ f y) : (inv f) x ≈ y :=
|
||||
ap (f⁻¹) p ⬝ sect f y
|
||||
|
||||
definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x :=
|
||||
(moveR_V f (p⁻¹))⁻¹
|
||||
|
||||
definition ap_closed [instance] (x y : A) : is_equiv (ap f) :=
|
||||
adjointify (ap f)
|
||||
(λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
|
||||
(λq, !ap_pp
|
||||
⬝ whiskerR !ap_pp _
|
||||
⬝ ((!ap_V ⬝ inverse2 ((adj f _)⁻¹))
|
||||
◾ (inverse (ap_compose (f⁻¹) f _))
|
||||
◾ (adj f _)⁻¹)
|
||||
⬝ concat_pA1_p (retr f) _ _
|
||||
⬝ whiskerR !concat_Vp _
|
||||
⬝ !concat_1p)
|
||||
(λp, whiskerR (whiskerL _ ((ap_compose f (f⁻¹) _)⁻¹)) _
|
||||
⬝ concat_pA1_p (sect f) _ _
|
||||
⬝ whiskerR !concat_Vp _
|
||||
⬝ !concat_1p)
|
||||
|
||||
-- The function equiv_rect says that given an equivalence f : A → B,
|
||||
-- and a hypothesis from B, one may always assume that the hypothesis
|
||||
-- is in the image of e.
|
||||
|
||||
-- In fibrational terms, if we have a fibration over B which has a section
|
||||
-- once pulled back along an equivalence f : A → B, then it has a section
|
||||
-- over all of B.
|
||||
|
||||
definition equiv_rect (P : B -> Type) :
|
||||
(Πx, P (f x)) → (Πy, P y) :=
|
||||
(λg y, path.transport _ (retr f y) (g (f⁻¹ y)))
|
||||
|
||||
definition equiv_rect_comp (P : B → Type)
|
||||
(df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) ≈ df x :=
|
||||
calc equiv_rect f P df (f x)
|
||||
≈ transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
|
||||
... ≈ transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
|
||||
... ≈ transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
|
||||
... ≈ df x : apD df (sect f x)
|
||||
|
||||
end
|
||||
|
||||
--Transporting is an equivalence
|
||||
protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (is_equiv (transport P p)) :=
|
||||
is_equiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
|
||||
|
||||
end is_equiv
|
||||
|
||||
namespace equiv
|
||||
|
||||
instance [persistent] to_is_equiv
|
||||
|
||||
infix `≃`:25 := equiv
|
||||
|
||||
context
|
||||
parameters {A B C : Type} (eqf : A ≃ B)
|
||||
|
||||
private definition f : A → B := to_fun eqf
|
||||
private definition Hf [instance] : is_equiv f := to_is_equiv eqf
|
||||
|
||||
protected definition refl : A ≃ A := equiv.mk id is_equiv.id_is_equiv
|
||||
|
||||
theorem trans (eqg: B ≃ C) : A ≃ C :=
|
||||
equiv.mk ((to_fun eqg) ∘ f)
|
||||
(is_equiv.compose f (to_fun eqg))
|
||||
|
||||
theorem path_closed (f' : A → B) (Heq : to_fun eqf ≈ f') : A ≃ B :=
|
||||
equiv.mk f' (is_equiv.path_closed f Heq)
|
||||
|
||||
theorem symm : B ≃ A :=
|
||||
equiv.mk (is_equiv.inv f) !is_equiv.inv_closed
|
||||
|
||||
theorem cancel_R (g : B → C) [Hgf : is_equiv (g ∘ f)] : B ≃ C :=
|
||||
equiv.mk g (is_equiv.cancel_R f _)
|
||||
|
||||
theorem cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : C ≃ A :=
|
||||
equiv.mk g (is_equiv.cancel_L f _)
|
||||
|
||||
protected theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
|
||||
equiv.mk (transport P p) (is_equiv.transport P p)
|
||||
|
||||
end
|
||||
|
||||
context
|
||||
parameters {A B : Type} (eqf eqg : A ≃ B)
|
||||
|
||||
private definition Hf [instance] : is_equiv (to_fun eqf) := to_is_equiv eqf
|
||||
private definition Hg [instance] : is_equiv (to_fun eqg) := to_is_equiv eqg
|
||||
|
||||
--We need this theorem for the funext_from_ua proof
|
||||
theorem inv_eq (p : eqf ≈ eqg)
|
||||
: is_equiv.inv (to_fun eqf) ≈ is_equiv.inv (to_fun eqg) :=
|
||||
path.rec_on p idp
|
||||
|
||||
end
|
||||
|
||||
-- calc enviroment
|
||||
-- Note: Calculating with substitutions needs univalence
|
||||
calc_trans trans
|
||||
calc_refl refl
|
||||
calc_symm symm
|
||||
|
||||
end equiv
|
||||
|
|
@ -1,81 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import hott.equiv hott.axioms.funext
|
||||
open path function funext
|
||||
|
||||
namespace is_equiv
|
||||
context
|
||||
|
||||
--Precomposition of arbitrary functions with f
|
||||
definition precomp {A B : Type} (f : A → B) (C : Type) (h : B → C) : A → C := h ∘ f
|
||||
|
||||
--Postcomposition of arbitrary functions with f
|
||||
definition postcomp {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l
|
||||
|
||||
--Precomposing with an equivalence is an equivalence
|
||||
definition precomp_closed [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
|
||||
: is_equiv (precomp f C) :=
|
||||
adjointify (precomp f C) (λh, h ∘ f⁻¹)
|
||||
(λh, path_pi (λx, ap h (sect f x)))
|
||||
(λg, path_pi (λy, ap g (retr f y)))
|
||||
|
||||
--Postcomposing with an equivalence is an equivalence
|
||||
definition postcomp_closed [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
|
||||
: is_equiv (postcomp f C) :=
|
||||
adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
|
||||
(λh, path_pi (λx, retr f (h x)))
|
||||
(λg, path_pi (λy, sect f (g y)))
|
||||
|
||||
--Conversely, if pre- or post-composing with a function is always an equivalence,
|
||||
--then that function is also an equivalence. It's convenient to know
|
||||
--that we only need to assume the equivalence when the other type is
|
||||
--the domain or the codomain.
|
||||
protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type)
|
||||
(Ceq : is_equiv (precomp f C)) (Deq : is_equiv (precomp f D)) (k : C → D) (h : A → C) :
|
||||
k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) :=
|
||||
let invD := inv (precomp f D) in
|
||||
let invC := inv (precomp f C) in
|
||||
have eq1 : invD (k ∘ h) ≈ k ∘ (invC h),
|
||||
from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
|
||||
... ≈ k ∘ (invC h) : !sect,
|
||||
eq1⁻¹
|
||||
|
||||
definition from_isequiv_precomp {A B : Type} (f : A → B) (Aeq : is_equiv (precomp f A))
|
||||
(Beq : is_equiv (precomp f B)) : (is_equiv f) :=
|
||||
let invA := inv (precomp f A) in
|
||||
let invB := inv (precomp f B) in
|
||||
let sect' : f ∘ (invA id) ∼ id := (λx,
|
||||
calc f (invA id x) ≈ (f ∘ invA id) x : idp
|
||||
... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
|
||||
... ≈ invB (precomp f B id) x : idp
|
||||
... ≈ x : apD10 (sect (precomp f B) id))
|
||||
in
|
||||
let retr' : (invA id) ∘ f ∼ id := (λx,
|
||||
calc invA id (f x) ≈ precomp f A (invA id) x : idp
|
||||
... ≈ x : apD10 (retr (precomp f A) id)) in
|
||||
adjointify f (invA id) sect' retr'
|
||||
|
||||
end
|
||||
|
||||
end is_equiv
|
||||
|
||||
--Bundled versions of the previous theorems
|
||||
namespace equiv
|
||||
|
||||
definition precomp_closed [F : funext] {A B C : Type} {eqf : A ≃ B}
|
||||
: (B → C) ≃ (A → C) :=
|
||||
let f := to_fun eqf in
|
||||
let Hf := to_is_equiv eqf in
|
||||
equiv.mk (is_equiv.precomp f C)
|
||||
(@is_equiv.precomp_closed A B f F Hf C)
|
||||
|
||||
definition postcomp_closed [F : funext] {A B C : Type} {eqf : A ≃ B}
|
||||
: (C → A) ≃ (C → B) :=
|
||||
let f := to_fun eqf in
|
||||
let Hf := to_is_equiv eqf in
|
||||
equiv.mk (is_equiv.postcomp f C)
|
||||
(@is_equiv.postcomp_closed A B f F Hf C)
|
||||
|
||||
end equiv
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
|
||||
import data.unit data.bool data.nat
|
||||
import data.prod data.sum data.sigma
|
||||
|
||||
open unit bool nat prod sum sigma
|
||||
|
||||
inductive fibrant [class] (T : Type) : Type :=
|
||||
fibrant_mk : fibrant T
|
||||
|
||||
namespace fibrant
|
||||
|
||||
axiom unit_fibrant : fibrant unit
|
||||
axiom nat_fibrant : fibrant nat
|
||||
axiom bool_fibrant : fibrant bool
|
||||
axiom sum_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A ⊎ B)
|
||||
axiom prod_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A × B)
|
||||
axiom sigma_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
|
||||
fibrant (Σx : A, B x)
|
||||
axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
|
||||
fibrant (Πx : A, B x)
|
||||
|
||||
instance [persistent] unit_fibrant
|
||||
instance [persistent] nat_fibrant
|
||||
instance [persistent] bool_fibrant
|
||||
instance [persistent] sum_fibrant
|
||||
instance [persistent] prod_fibrant
|
||||
instance [persistent] sigma_fibrant
|
||||
instance [persistent] pi_fibrant
|
||||
|
||||
end fibrant
|
||||
|
|
@ -1,130 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import hott.equiv hott.funext_varieties hott.axioms.ua hott.axioms.funext
|
||||
import data.prod data.sigma data.unit
|
||||
|
||||
open path function prod sigma truncation equiv is_equiv unit ua_type
|
||||
|
||||
context
|
||||
universe variables l
|
||||
parameter [UA : ua_type.{l+1}]
|
||||
|
||||
protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
|
||||
{w : A → B} {H0 : is_equiv w} : is_equiv (@compose C A B w) :=
|
||||
let w' := equiv.mk w H0 in
|
||||
let eqinv : A ≈ B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
|
||||
let eq' := equiv_path eqinv in
|
||||
is_equiv.adjointify (@compose C A B w)
|
||||
(@compose C B A (is_equiv.inv w))
|
||||
(λ (x : C → B),
|
||||
have eqretr : eq' ≈ w',
|
||||
from (@retr _ _ (@equiv_path A B) (@ua_type.inst UA A B) w'),
|
||||
have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
|
||||
from inv_eq eq' w' eqretr,
|
||||
have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
|
||||
from (λ p,
|
||||
(@path.rec_on Type.{l+1} A
|
||||
(λ B' p', Π (x' : C → B'), (to_fun (equiv_path p'))
|
||||
∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') ≈ x')
|
||||
B p (λ x', idp))
|
||||
) eqinv x,
|
||||
have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
|
||||
from eqretr ▹ eqfin,
|
||||
have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) ≈ x,
|
||||
from invs_eq ▹ eqfin',
|
||||
eqfin''
|
||||
)
|
||||
(λ (x : C → A),
|
||||
have eqretr : eq' ≈ w',
|
||||
from (@retr _ _ (@equiv_path A B) ua_type.inst w'),
|
||||
have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
|
||||
from inv_eq eq' w' eqretr,
|
||||
have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) ≈ x,
|
||||
from (λ p, path.rec_on p idp) eqinv,
|
||||
have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
|
||||
from eqretr ▹ eqfin,
|
||||
have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
|
||||
from invs_eq ▹ eqfin',
|
||||
eqfin''
|
||||
)
|
||||
|
||||
-- We are ready to prove functional extensionality,
|
||||
-- starting with the naive non-dependent version.
|
||||
protected definition diagonal [reducible] (B : Type) : Type
|
||||
:= Σ xy : B × B, pr₁ xy ≈ pr₂ xy
|
||||
|
||||
protected definition isequiv_src_compose {A B : Type}
|
||||
: @is_equiv (A → diagonal B)
|
||||
(A → B)
|
||||
(compose (pr₁ ∘ dpr1)) :=
|
||||
@ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1)
|
||||
(is_equiv.adjointify (pr₁ ∘ dpr1)
|
||||
(λ x, dpair (x , x) idp) (λx, idp)
|
||||
(λ x, sigma.rec_on x
|
||||
(λ xy, prod.rec_on xy
|
||||
(λ b c p, path.rec_on p idp))))
|
||||
|
||||
protected definition isequiv_tgt_compose {A B : Type}
|
||||
: @is_equiv (A → diagonal B)
|
||||
(A → B)
|
||||
(compose (pr₂ ∘ dpr1)) :=
|
||||
@ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1)
|
||||
(is_equiv.adjointify (pr2 ∘ dpr1)
|
||||
(λ x, dpair (x , x) idp) (λx, idp)
|
||||
(λ x, sigma.rec_on x
|
||||
(λ xy, prod.rec_on xy
|
||||
(λ b c p, path.rec_on p idp))))
|
||||
|
||||
theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}}
|
||||
: Π {f g : A → B}, f ∼ g → f ≈ g :=
|
||||
(λ (f g : A → B) (p : f ∼ g),
|
||||
let d := λ (x : A), dpair (f x , f x) idp in
|
||||
let e := λ (x : A), dpair (f x , g x) (p x) in
|
||||
let precomp1 := compose (pr₁ ∘ dpr1) in
|
||||
have equiv1 [visible] : is_equiv precomp1,
|
||||
from @isequiv_src_compose A B,
|
||||
have equiv2 [visible] : Π x y, is_equiv (ap precomp1),
|
||||
from is_equiv.ap_closed precomp1,
|
||||
have H' : Π (x y : A → diagonal B),
|
||||
pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y,
|
||||
from (λ x y, is_equiv.inv (ap precomp1)),
|
||||
have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e,
|
||||
from idp,
|
||||
have eq0 : d ≈ e,
|
||||
from H' d e eq2,
|
||||
have eq1 : (pr₂ ∘ dpr1) ∘ d ≈ (pr₂ ∘ dpr1) ∘ e,
|
||||
from ap _ eq0,
|
||||
eq1
|
||||
)
|
||||
|
||||
end
|
||||
|
||||
-- Now we use this to prove weak funext, which as we know
|
||||
-- implies (with dependent eta) also the strong dependent funext.
|
||||
universe variables l k
|
||||
theorem weak_funext_from_ua [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_funext.{l+1 k+1} :=
|
||||
(λ (A : Type) (P : A → Type) allcontr,
|
||||
let U := (λ (x : A), unit) in
|
||||
have pequiv : Π (x : A), P x ≃ U x,
|
||||
from (λ x, @equiv_contr_unit(P x) (allcontr x)),
|
||||
have psim : Π (x : A), P x ≈ U x,
|
||||
from (λ x, @is_equiv.inv _ _
|
||||
equiv_path ua_type.inst (pequiv x)),
|
||||
have p : P ≈ U,
|
||||
from @nondep_funext_from_ua _ A Type P U psim,
|
||||
have tU' : is_contr (A → unit),
|
||||
from is_contr.mk (λ x, ⋆)
|
||||
(λ f, @nondep_funext_from_ua _ A unit (λ x, ⋆) f
|
||||
(λ x, unit.rec_on (f x) idp)),
|
||||
have tU : is_contr (Π x, U x),
|
||||
from tU',
|
||||
have tlast : is_contr (Πx, P x),
|
||||
from path.transport _ (p⁻¹) tU,
|
||||
tlast
|
||||
)
|
||||
|
||||
-- In the following we will proof function extensionality using the univalence axiom
|
||||
definition funext_from_ua [instance] [ua ua2 : ua_type] : funext :=
|
||||
funext_from_weak_funext (@weak_funext_from_ua ua ua2)
|
||||
|
|
@ -1,110 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import hott.path hott.trunc hott.equiv hott.axioms.funext
|
||||
|
||||
open path truncation sigma function
|
||||
|
||||
/- In hott.axioms.funext, we defined function extensionality to be the assertion
|
||||
that the map apD10 is an equivalence. We now prove that this follows
|
||||
from a couple of weaker-looking forms of function extensionality. We do
|
||||
require eta conversion, which Coq 8.4+ has judgmentally.
|
||||
|
||||
This proof is originally due to Voevodsky; it has since been simplified
|
||||
by Peter Lumsdaine and Michael Shulman. -/
|
||||
|
||||
-- Naive funext is the simple assertion that pointwise equal functions are equal.
|
||||
-- TODO think about universe levels
|
||||
definition naive_funext :=
|
||||
Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g
|
||||
|
||||
-- Weak funext says that a product of contractible types is contractible.
|
||||
definition weak_funext.{l k} :=
|
||||
Π {A : Type.{l}} (P : A → Type.{k}) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
|
||||
|
||||
-- The obvious implications are Funext -> NaiveFunext -> WeakFunext
|
||||
-- TODO: Get class inference to work locally
|
||||
definition naive_funext_from_funext [F : funext] : naive_funext :=
|
||||
(λ A P f g h,
|
||||
have Fefg: is_equiv (@apD10 A P f g),
|
||||
from (@funext.ap F A P f g),
|
||||
have eq1 : _, from (@is_equiv.inv _ _ (@apD10 A P f g) Fefg h),
|
||||
eq1
|
||||
)
|
||||
|
||||
definition weak_funext_from_naive_funext : naive_funext → weak_funext :=
|
||||
(λ nf A P (Pc : Πx, is_contr (P x)),
|
||||
let c := λx, center (P x) in
|
||||
is_contr.mk c (λ f,
|
||||
have eq' : (λx, center (P x)) ∼ f,
|
||||
from (λx, contr (f x)),
|
||||
have eq : (λx, center (P x)) ≈ f,
|
||||
from nf A P (λx, center (P x)) f eq',
|
||||
eq
|
||||
)
|
||||
)
|
||||
|
||||
/- The less obvious direction is that WeakFunext implies Funext
|
||||
(and hence all three are logically equivalent). The point is that under weak
|
||||
funext, the space of "pointwise homotopies" has the same universal property as
|
||||
the space of paths. -/
|
||||
|
||||
context
|
||||
universes l k
|
||||
parameters (wf : weak_funext.{l+1 k+1}) {A : Type.{l+1}} {B : A → Type.{k+1}} (f : Π x, B x)
|
||||
|
||||
protected definition idhtpy : f ∼ f := (λ x, idp)
|
||||
|
||||
definition contr_basedhtpy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
|
||||
is_contr.mk (dpair f idhtpy)
|
||||
(λ dp, sigma.rec_on dp
|
||||
(λ (g : Π x, B x) (h : f ∼ g),
|
||||
let r := λ (k : Π x, Σ y, f x ≈ y),
|
||||
@dpair _ (λg, f ∼ g)
|
||||
(λx, dpr1 (k x)) (λx, dpr2 (k x)) in
|
||||
let s := λ g h x, @dpair _ (λy, f x ≈ y) (g x) (h x) in
|
||||
have t1 : Πx, is_contr (Σ y, f x ≈ y),
|
||||
from (λx, !contr_basedpaths),
|
||||
have t2 : is_contr (Πx, Σ y, f x ≈ y),
|
||||
from !wf,
|
||||
have t3 : (λ x, @dpair _ (λ y, f x ≈ y) (f x) idp) ≈ s g h,
|
||||
from @path_contr (Π x, Σ y, f x ≈ y) t2 _ _,
|
||||
have t4 : r (λ x, dpair (f x) idp) ≈ r (s g h),
|
||||
from ap r t3,
|
||||
have endt : dpair f idhtpy ≈ dpair g h,
|
||||
from t4,
|
||||
endt
|
||||
)
|
||||
)
|
||||
|
||||
parameters (Q : Π g (h : f ∼ g), Type) (d : Q f idhtpy)
|
||||
|
||||
definition htpy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
|
||||
@transport _ (λ gh, Q (dpr1 gh) (dpr2 gh)) (dpair f idhtpy) (dpair g h)
|
||||
(@path_contr _ contr_basedhtpy _ _) d
|
||||
|
||||
definition htpy_ind_beta : htpy_ind f idhtpy ≈ d :=
|
||||
(@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp
|
||||
|
||||
end
|
||||
|
||||
-- Now the proof is fairly easy; we can just use the same induction principle on both sides.
|
||||
universe variables l k
|
||||
|
||||
theorem funext_from_weak_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+1} :=
|
||||
funext.mk (λ A B f g,
|
||||
let eq_to_f := (λ g' x, f ≈ g') in
|
||||
let sim2path := htpy_ind _ f eq_to_f idp in
|
||||
have t1 : sim2path f (idhtpy f) ≈ idp,
|
||||
proof htpy_ind_beta _ f eq_to_f idp qed,
|
||||
have t2 : apD10 (sim2path f (idhtpy f)) ≈ (idhtpy f),
|
||||
proof ap apD10 t1 qed,
|
||||
have sect : apD10 ∘ (sim2path g) ∼ id,
|
||||
proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed,
|
||||
have retr : (sim2path g) ∘ apD10 ∼ id,
|
||||
from (λ h, path.rec_on h (htpy_ind_beta _ f _ idp)),
|
||||
is_equiv.adjointify apD10 (sim2path g) sect retr)
|
||||
|
||||
definition funext_from_naive_funext : naive_funext -> funext :=
|
||||
compose funext_from_weak_funext weak_funext_from_naive_funext
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
standard.hott
|
||||
=============
|
||||
|
||||
A library for homotopy type theory. HoTT is consistent with the
|
||||
existence of an imprediative, proof irrelevant `Prop`, but favors
|
||||
"proof relevant," predicative versions of the usual logical
|
||||
constructions. For example, we use the path type, products, sums,
|
||||
sigmas, and the empty type, rather than equality, and, or, exists, and
|
||||
false. These operations take values in `Type` rather than `Prop`.
|
||||
|
||||
Note that the univalence axiom is inconsistent with classical axioms
|
||||
such as propositional extensionality or Hilbert choice, and we have to
|
||||
ensure that the library does not import these.
|
||||
|
||||
The modules imported by the command `import hott` are found in the
|
||||
file [default](default.lean).
|
||||
|
||||
* [path](path.lean) : the path type and operations on paths
|
||||
* [equiv](equiv.lean) : equivalence of types
|
||||
* [trunc](trunc.lean) : truncatedness of types
|
||||
* [funext](funext.lean) : the functional extensionality axiom
|
||||
* [fibrant](fibrant.lean) : a class for fibrant types
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
import data.empty .path
|
||||
|
||||
open path
|
||||
inductive tdecidable [class] (A : Type) : Type :=
|
||||
inl : A → tdecidable A,
|
||||
inr : ~A → tdecidable A
|
||||
|
||||
structure decidable_paths [class] (A : Type) :=
|
||||
(elim : ∀(x y : A), tdecidable (x ≈ y))
|
||||
|
|
@ -1,720 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
-- Ported from Coq HoTT
|
||||
--
|
||||
-- TODO: things to test:
|
||||
-- o To what extent can we use opaque definitions outside the file?
|
||||
-- o Try doing these proofs with tactics.
|
||||
-- o Try using the simplifier on some of these proofs.
|
||||
|
||||
import algebra.function
|
||||
|
||||
open function
|
||||
|
||||
-- Path
|
||||
-- ----
|
||||
|
||||
inductive path.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
|
||||
idpath : path a a
|
||||
|
||||
namespace path
|
||||
variables {A B C : Type} {P : A → Type} {x y z t : A}
|
||||
|
||||
notation a ≈ b := path a b
|
||||
notation x ≈ y `:>`:50 A:49 := @path A x y
|
||||
definition idp {a : A} := idpath a
|
||||
|
||||
-- unbased path induction
|
||||
definition rec' [reducible] {P : Π (a b : A), (a ≈ b) -> Type}
|
||||
(H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p :=
|
||||
path.rec (H a) p
|
||||
|
||||
definition rec_on' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b)
|
||||
(H : Π (a : A), P a a idp) : P a b p :=
|
||||
path.rec (H a) p
|
||||
|
||||
-- Concatenation and inverse
|
||||
-- -------------------------
|
||||
|
||||
definition concat (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
|
||||
path.rec (λu, u) q p
|
||||
|
||||
definition inverse (p : x ≈ y) : y ≈ x :=
|
||||
path.rec (idpath x) p
|
||||
|
||||
notation p₁ ⬝ p₂ := concat p₁ p₂
|
||||
notation p ⁻¹ := inverse p
|
||||
|
||||
-- The 1-dimensional groupoid structure
|
||||
-- ------------------------------------
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_p1 (p : x ≈ y) : p ⬝ idp ≈ p :=
|
||||
rec_on p idp
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_1p (p : x ≈ y) : idp ⬝ p ≈ p :=
|
||||
rec_on p idp
|
||||
|
||||
-- Concatenation is associative.
|
||||
definition concat_p_pp (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r :=
|
||||
rec_on r (rec_on q idp)
|
||||
|
||||
definition concat_pp_p (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
(p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) :=
|
||||
rec_on r (rec_on q idp)
|
||||
|
||||
-- The left inverse law.
|
||||
definition concat_pV (p : x ≈ y) : p ⬝ p⁻¹ ≈ idp :=
|
||||
rec_on p idp
|
||||
|
||||
-- The right inverse law.
|
||||
definition concat_Vp (p : x ≈ y) : p⁻¹ ⬝ p ≈ idp :=
|
||||
rec_on p idp
|
||||
|
||||
-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
|
||||
-- redundant, following from earlier theorems.
|
||||
|
||||
definition concat_V_pp (p : x ≈ y) (q : y ≈ z) : p⁻¹ ⬝ (p ⬝ q) ≈ q :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition concat_p_Vp (p : x ≈ y) (q : x ≈ z) : p ⬝ (p⁻¹ ⬝ q) ≈ q :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition concat_pp_V (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q⁻¹ ≈ p :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition concat_pV_p (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p :=
|
||||
rec_on q (take p, rec_on p idp) p
|
||||
|
||||
-- Inverse distributes over concatenation
|
||||
definition inv_pp (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p⁻¹ :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition inv_Vp (p : y ≈ x) (q : y ≈ z) : (p⁻¹ ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
-- universe metavariables
|
||||
definition inv_pV (p : x ≈ y) (q : z ≈ y) : (p ⬝ q⁻¹)⁻¹ ≈ q ⬝ p⁻¹ :=
|
||||
rec_on p (take q, rec_on q idp) q
|
||||
|
||||
definition inv_VV (p : y ≈ x) (q : z ≈ y) : (p⁻¹ ⬝ q⁻¹)⁻¹ ≈ q ⬝ p :=
|
||||
rec_on p (rec_on q idp)
|
||||
|
||||
-- Inverse is an involution.
|
||||
definition inv_V (p : x ≈ y) : p⁻¹⁻¹ ≈ p :=
|
||||
rec_on p idp
|
||||
|
||||
-- Theorems for moving things around in equations
|
||||
-- ----------------------------------------------
|
||||
|
||||
definition moveR_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
p ≈ (r⁻¹ ⬝ q) → (r ⬝ p) ≈ q :=
|
||||
rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p
|
||||
|
||||
definition moveR_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p⁻¹ → r ⬝ p ≈ q :=
|
||||
rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q
|
||||
|
||||
definition moveR_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
p ≈ r ⬝ q → r⁻¹ ⬝ p ≈ q :=
|
||||
rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q
|
||||
|
||||
definition moveR_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p → r ⬝ p⁻¹ ≈ q :=
|
||||
rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r
|
||||
|
||||
definition moveL_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r⁻¹ ⬝ q ≈ p → q ≈ r ⬝ p :=
|
||||
rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p
|
||||
|
||||
definition moveL_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p⁻¹ ≈ r → q ≈ r ⬝ p :=
|
||||
rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q
|
||||
|
||||
definition moveL_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
r ⬝ q ≈ p → q ≈ r⁻¹ ⬝ p :=
|
||||
rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q
|
||||
|
||||
definition moveL_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p ≈ r → q ≈ r ⬝ p⁻¹ :=
|
||||
rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r
|
||||
|
||||
definition moveL_1M (p q : x ≈ y) :
|
||||
p ⬝ q⁻¹ ≈ idp → p ≈ q :=
|
||||
rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p
|
||||
|
||||
definition moveL_M1 (p q : x ≈ y) :
|
||||
q⁻¹ ⬝ p ≈ idp → p ≈ q :=
|
||||
rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p
|
||||
|
||||
definition moveL_1V (p : x ≈ y) (q : y ≈ x) :
|
||||
p ⬝ q ≈ idp → p ≈ q⁻¹ :=
|
||||
rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p
|
||||
|
||||
definition moveL_V1 (p : x ≈ y) (q : y ≈ x) :
|
||||
q ⬝ p ≈ idp → p ≈ q⁻¹ :=
|
||||
rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p
|
||||
|
||||
definition moveR_M1 (p q : x ≈ y) :
|
||||
idp ≈ p⁻¹ ⬝ q → p ≈ q :=
|
||||
rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
definition moveR_1M (p q : x ≈ y) :
|
||||
idp ≈ q ⬝ p⁻¹ → p ≈ q :=
|
||||
rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_1V (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ q ⬝ p → p⁻¹ ≈ q :=
|
||||
rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_V1 (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ p ⬝ q → p⁻¹ ≈ q :=
|
||||
rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
|
||||
-- Transport
|
||||
-- ---------
|
||||
|
||||
definition transport [reducible] (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y :=
|
||||
path.rec_on p u
|
||||
|
||||
-- This idiom makes the operation right associative.
|
||||
notation p `▹`:65 x:64 := transport _ p x
|
||||
|
||||
definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition ap01 := ap
|
||||
|
||||
definition homotopy [reducible] (f g : Πx, P x) : Type :=
|
||||
Πx : A, f x ≈ g x
|
||||
|
||||
notation f ∼ g := homotopy f g
|
||||
|
||||
definition apD10 {f g : Πx, P x} (H : f ≈ g) : f ∼ g :=
|
||||
λx, path.rec_on H idp
|
||||
|
||||
definition ap10 {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H
|
||||
|
||||
definition ap11 {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y :=
|
||||
rec_on H (rec_on p idp)
|
||||
|
||||
definition apD (f : Πa:A, P a) {x y : A} (p : x ≈ y) : p ▹ (f x) ≈ f y :=
|
||||
rec_on p idp
|
||||
|
||||
|
||||
-- calc enviroment
|
||||
-- ---------------
|
||||
|
||||
calc_subst transport
|
||||
calc_trans concat
|
||||
calc_refl idpath
|
||||
calc_symm inverse
|
||||
|
||||
-- More theorems for moving things around in equations
|
||||
-- ---------------------------------------------------
|
||||
|
||||
definition moveR_transport_p (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
u ≈ p⁻¹ ▹ v → p ▹ u ≈ v :=
|
||||
rec_on p (take v, id) v
|
||||
|
||||
definition moveR_transport_V (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
u ≈ p ▹ v → p⁻¹ ▹ u ≈ v :=
|
||||
rec_on p (take u, id) u
|
||||
|
||||
definition moveL_transport_V (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
p ▹ u ≈ v → u ≈ p⁻¹ ▹ v :=
|
||||
rec_on p (take v, id) v
|
||||
|
||||
definition moveL_transport_p (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
p⁻¹ ▹ u ≈ v → u ≈ p ▹ v :=
|
||||
rec_on p (take u, id) u
|
||||
|
||||
-- Functoriality of functions
|
||||
-- --------------------------
|
||||
|
||||
-- Here we prove that functions behave like functors between groupoids, and that [ap] itself is
|
||||
-- functorial.
|
||||
|
||||
-- Functions take identity paths to identity paths
|
||||
definition ap_1 (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp
|
||||
|
||||
definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
|
||||
|
||||
-- Functions commute with concatenation.
|
||||
definition ap_pp (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition ap_p_pp (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) :
|
||||
r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) :=
|
||||
rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p
|
||||
|
||||
definition ap_pp_p (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) :
|
||||
(ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) :=
|
||||
rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r
|
||||
|
||||
-- Functions commute with path inverses.
|
||||
definition inverse_ap (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)⁻¹ ≈ ap f (p⁻¹) :=
|
||||
rec_on p idp
|
||||
|
||||
definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p⁻¹) ≈ (ap f p)⁻¹ :=
|
||||
rec_on p idp
|
||||
|
||||
-- [ap] itself is functorial in the first argument.
|
||||
|
||||
definition ap_idmap (p : x ≈ y) : ap id p ≈ p :=
|
||||
rec_on p idp
|
||||
|
||||
definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
|
||||
ap (g ∘ f) p ≈ ap g (ap f p) :=
|
||||
rec_on p idp
|
||||
|
||||
-- Sometimes we don't have the actual function [compose].
|
||||
definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
|
||||
ap (λa, g (f a)) p ≈ ap g (ap f p) :=
|
||||
rec_on p idp
|
||||
|
||||
-- The action of constant maps.
|
||||
definition ap_const (p : x ≈ y) (z : B) :
|
||||
ap (λu, z) p ≈ idp :=
|
||||
rec_on p idp
|
||||
|
||||
-- Naturality of [ap].
|
||||
definition concat_Ap {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
|
||||
rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹)
|
||||
|
||||
-- Naturality of [ap] at identity.
|
||||
definition concat_A1p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
|
||||
rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹)
|
||||
|
||||
definition concat_pA1 {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) :
|
||||
(p x) ⬝ (ap f q) ≈ q ⬝ (p y) :=
|
||||
rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹)
|
||||
|
||||
-- Naturality with other paths hanging around.
|
||||
|
||||
definition concat_pA_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{w z : B} (r : w ≈ f x) (s : g y ≈ z) :
|
||||
(r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) :=
|
||||
rec_on s (rec_on q idp)
|
||||
|
||||
definition concat_pA_p {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{w : B} (r : w ≈ f x) :
|
||||
(r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ ap g q :=
|
||||
rec_on q idp
|
||||
|
||||
-- TODO: try this using the simplifier, and compare proofs
|
||||
definition concat_A_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{z : B} (s : g y ≈ z) :
|
||||
(ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (ap g q ⬝ s) :=
|
||||
rec_on s (rec_on q
|
||||
(calc
|
||||
(ap f idp) ⬝ (p x ⬝ idp) ≈ idp ⬝ p x : idp
|
||||
... ≈ p x : concat_1p _
|
||||
... ≈ (p x) ⬝ (ap g idp ⬝ idp) : idp))
|
||||
-- This also works:
|
||||
-- rec_on s (rec_on q (concat_1p _ ▹ idp))
|
||||
|
||||
definition concat_pA1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
|
||||
{w z : A} (r : w ≈ f x) (s : y ≈ z) :
|
||||
(r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (q ⬝ s) :=
|
||||
rec_on s (rec_on q idp)
|
||||
|
||||
definition concat_pp_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{w z : A} (r : w ≈ x) (s : g y ≈ z) :
|
||||
(r ⬝ p x) ⬝ (ap g q ⬝ s) ≈ (r ⬝ q) ⬝ (p y ⬝ s) :=
|
||||
rec_on s (rec_on q idp)
|
||||
|
||||
definition concat_pA1_p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
|
||||
{w : A} (r : w ≈ f x) :
|
||||
(r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ q :=
|
||||
rec_on q idp
|
||||
|
||||
definition concat_A1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
|
||||
{z : A} (s : y ≈ z) :
|
||||
(ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (q ⬝ s) :=
|
||||
rec_on s (rec_on q (concat_1p _ ▹ idp))
|
||||
|
||||
definition concat_pp_A1 {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{w : A} (r : w ≈ x) :
|
||||
(r ⬝ p x) ⬝ ap g q ≈ (r ⬝ q) ⬝ p y :=
|
||||
rec_on q idp
|
||||
|
||||
definition concat_p_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
|
||||
{z : A} (s : g y ≈ z) :
|
||||
p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) :=
|
||||
begin
|
||||
apply (rec_on s),
|
||||
apply (rec_on q),
|
||||
apply (concat_1p (p x) ▹ idp)
|
||||
end
|
||||
|
||||
-- Action of [apD10] and [ap10] on paths
|
||||
-- -------------------------------------
|
||||
|
||||
-- Application of paths between functions preserves the groupoid structure
|
||||
|
||||
definition apD10_1 (f : Πx, P x) (x : A) : apD10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition apD10_pp {f f' f'' : Πx, P x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x :=
|
||||
rec_on h (take h', rec_on h' idp) h'
|
||||
|
||||
definition apD10_V {f g : Πx : A, P x} (h : f ≈ g) (x : A) :
|
||||
apD10 (h⁻¹) x ≈ (apD10 h x)⁻¹ :=
|
||||
rec_on h idp
|
||||
|
||||
definition ap10_1 {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition ap10_pp {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x
|
||||
|
||||
definition ap10_V {f g : A → B} (h : f ≈ g) (x : A) : ap10 (h⁻¹) x ≈ (ap10 h x)⁻¹ :=
|
||||
apD10_V h x
|
||||
|
||||
-- [ap10] also behaves nicely on paths produced by [ap]
|
||||
definition ap_ap10 (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
|
||||
ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:=
|
||||
rec_on p idp
|
||||
|
||||
|
||||
-- Transport and the groupoid structure of paths
|
||||
-- ---------------------------------------------
|
||||
|
||||
definition transport_1 (P : A → Type) {x : A} (u : P x) :
|
||||
idp ▹ u ≈ u := idp
|
||||
|
||||
definition transport_pp (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
|
||||
p ⬝ q ▹ u ≈ q ▹ p ▹ u :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition transport_pV (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
|
||||
p ▹ p⁻¹ ▹ z ≈ z :=
|
||||
(transport_pp P (p⁻¹) p z)⁻¹ ⬝ ap (λr, transport P r z) (concat_Vp p)
|
||||
|
||||
definition transport_Vp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
|
||||
p⁻¹ ▹ p ▹ z ≈ z :=
|
||||
(transport_pp P p (p⁻¹) z)⁻¹ ⬝ ap (λr, transport P r z) (concat_pV p)
|
||||
|
||||
definition transport_p_pp (P : A → Type)
|
||||
{x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) :
|
||||
ap (λe, e ▹ u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝
|
||||
ap (transport P r) (transport_pp P p q u)
|
||||
≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u))
|
||||
:> ((p ⬝ (q ⬝ r)) ▹ u ≈ r ▹ q ▹ p ▹ u) :=
|
||||
rec_on r (rec_on q (rec_on p idp))
|
||||
|
||||
-- Here is another coherence lemma for transport.
|
||||
definition transport_pVp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
|
||||
transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) :=
|
||||
rec_on p idp
|
||||
|
||||
-- Dependent transport in a doubly dependent type.
|
||||
-- should P, Q and y all be explicit here?
|
||||
definition transportD (P : A → Type) (Q : Π a : A, P a → Type)
|
||||
{a a' : A} (p : a ≈ a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=
|
||||
rec_on p z
|
||||
-- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation
|
||||
notation p `▹D`:65 x:64 := transportD _ _ p _ x
|
||||
|
||||
-- Transporting along higher-dimensional paths
|
||||
definition transport2 (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) :
|
||||
p ▹ z ≈ q ▹ z :=
|
||||
ap (λp', p' ▹ z) r
|
||||
|
||||
notation p `▹2`:65 x:64 := transport2 _ p _ x
|
||||
|
||||
-- An alternative definition.
|
||||
definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q)
|
||||
(z : Q x) :
|
||||
transport2 Q r z ≈ ap10 (ap (transport Q) r) z :=
|
||||
rec_on r idp
|
||||
|
||||
definition transport2_p2p (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y}
|
||||
(r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) :
|
||||
transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z :=
|
||||
rec_on r1 (rec_on r2 idp)
|
||||
|
||||
definition transport2_V (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
|
||||
transport2 Q (r⁻¹) z ≈ ((transport2 Q r z)⁻¹) :=
|
||||
rec_on r idp
|
||||
|
||||
definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type)
|
||||
{x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) :=
|
||||
rec_on p w
|
||||
|
||||
notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x
|
||||
|
||||
definition concat_AT (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
|
||||
(s : z ≈ w) :
|
||||
ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s :=
|
||||
rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹)
|
||||
|
||||
-- TODO (from Coq library): What should this be called?
|
||||
definition ap_transport {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
|
||||
f y (p ▹ z) ≈ (p ▹ (f x z)) :=
|
||||
rec_on p idp
|
||||
|
||||
|
||||
-- Transporting in particular fibrations
|
||||
-- -------------------------------------
|
||||
|
||||
/-
|
||||
From the Coq HoTT library:
|
||||
|
||||
One frequently needs lemmas showing that transport in a certain dependent type is equal to some
|
||||
more explicitly defined operation, defined according to the structure of that dependent type.
|
||||
For most dependent types, we prove these lemmas in the appropriate file in the types/
|
||||
subdirectory. Here we consider only the most basic cases.
|
||||
-/
|
||||
|
||||
-- Transporting in a constant fibration.
|
||||
definition transport_const (p : x ≈ y) (z : B) : transport (λx, B) p z ≈ z :=
|
||||
rec_on p idp
|
||||
|
||||
definition transport2_const {p q : x ≈ y} (r : p ≈ q) (z : B) :
|
||||
transport_const p z ≈ transport2 (λu, B) r z ⬝ transport_const q z :=
|
||||
rec_on r (concat_1p _)⁻¹
|
||||
|
||||
-- Transporting in a pulled back fibration.
|
||||
-- TODO: P can probably be implicit
|
||||
definition transport_compose (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
|
||||
transport (P ∘ f) p z ≈ transport P (ap f p) z :=
|
||||
rec_on p idp
|
||||
|
||||
definition transport_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') :
|
||||
transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p :=
|
||||
rec_on p idp
|
||||
|
||||
definition apD10_ap_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) :
|
||||
apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) :=
|
||||
rec_on p idp
|
||||
|
||||
definition apD10_ap_postcompose (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) :
|
||||
apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) :=
|
||||
rec_on p idp
|
||||
|
||||
-- A special case of [transport_compose] which seems to come up a lot.
|
||||
definition transport_idmap_ap (P : A → Type) x y (p : x ≈ y) (u : P x) :
|
||||
transport P p u ≈ transport (λz, z) (ap P p) u :=
|
||||
rec_on p idp
|
||||
|
||||
|
||||
-- The behavior of [ap] and [apD]
|
||||
-- ------------------------------
|
||||
|
||||
-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const].
|
||||
definition apD_const (f : A → B) (p: x ≈ y) :
|
||||
apD f p ≈ transport_const p (f x) ⬝ ap f p :=
|
||||
rec_on p idp
|
||||
|
||||
|
||||
-- The 2-dimensional groupoid structure
|
||||
-- ------------------------------------
|
||||
|
||||
-- Horizontal composition of 2-dimensional paths.
|
||||
definition concat2 {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
|
||||
p ⬝ q ≈ p' ⬝ q' :=
|
||||
rec_on h (rec_on h' idp)
|
||||
|
||||
infixl `◾`:75 := concat2
|
||||
|
||||
-- 2-dimensional path inversion
|
||||
definition inverse2 {p q : x ≈ y} (h : p ≈ q) : p⁻¹ ≈ q⁻¹ :=
|
||||
rec_on h idp
|
||||
|
||||
|
||||
-- Whiskering
|
||||
-- ----------
|
||||
|
||||
definition whiskerL (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r :=
|
||||
idp ◾ h
|
||||
|
||||
definition whiskerR {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r :=
|
||||
h ◾ idp
|
||||
|
||||
-- Unwhiskering, a.k.a. cancelling
|
||||
|
||||
definition cancelL {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
|
||||
rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q
|
||||
|
||||
definition cancelR {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
|
||||
rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q
|
||||
|
||||
-- Whiskering and identity paths.
|
||||
|
||||
definition whiskerR_p1 {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
|
||||
rec_on h (rec_on p idp)
|
||||
|
||||
definition whiskerR_1p (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
rec_on q idp
|
||||
|
||||
definition whiskerL_p1 (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
rec_on q idp
|
||||
|
||||
definition whiskerL_1p {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
|
||||
rec_on h (rec_on p idp)
|
||||
|
||||
definition concat2_p1 {p q : x ≈ y} (h : p ≈ q) :
|
||||
h ◾ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) :=
|
||||
rec_on h idp
|
||||
|
||||
definition concat2_1p {p q : x ≈ y} (h : p ≈ q) :
|
||||
idp ◾ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) :=
|
||||
rec_on h idp
|
||||
|
||||
-- TODO: note, 4 inductions
|
||||
-- The interchange law for concatenation.
|
||||
definition concat_concat2 {p p' p'' : x ≈ y} {q q' q'' : y ≈ z}
|
||||
(a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') :
|
||||
(a ◾ c) ⬝ (b ◾ d) ≈ (a ⬝ b) ◾ (c ⬝ d) :=
|
||||
rec_on d (rec_on c (rec_on b (rec_on a idp)))
|
||||
|
||||
definition concat_whisker {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
|
||||
(whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
|
||||
rec_on b (rec_on a (concat_1p _)⁻¹)
|
||||
|
||||
-- Structure corresponding to the coherence equations of a bicategory.
|
||||
|
||||
-- The "pentagonator": the 3-cell witnessing the associativity pentagon.
|
||||
definition pentagon {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
|
||||
whiskerL p (concat_p_pp q r s)
|
||||
⬝ concat_p_pp p (q ⬝ r) s
|
||||
⬝ whiskerR (concat_p_pp p q r) s
|
||||
≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s :=
|
||||
rec_on s (rec_on r (rec_on q (rec_on p idp)))
|
||||
|
||||
-- The 3-cell witnessing the left unit triangle.
|
||||
definition triangulator (p : x ≈ y) (q : y ≈ z) :
|
||||
concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
|
||||
rec_on q (rec_on p idp)
|
||||
|
||||
definition eckmann_hilton {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
|
||||
(!whiskerR_p1 ◾ !whiskerL_1p)⁻¹
|
||||
⬝ (!concat_p1 ◾ !concat_p1)
|
||||
⬝ (!concat_1p ◾ !concat_1p)
|
||||
⬝ !concat_whisker
|
||||
⬝ (!concat_1p ◾ !concat_1p)⁻¹
|
||||
⬝ (!concat_p1 ◾ !concat_p1)⁻¹
|
||||
⬝ (!whiskerL_1p ◾ !whiskerR_p1)
|
||||
|
||||
-- The action of functions on 2-dimensional paths
|
||||
definition ap02 (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q :=
|
||||
rec_on r idp
|
||||
|
||||
definition ap02_pp (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') :
|
||||
ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' :=
|
||||
rec_on r (rec_on r' idp)
|
||||
|
||||
definition ap02_p2p (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p')
|
||||
(s : q ≈ q') :
|
||||
ap02 f (r ◾ s) ≈ ap_pp f p q
|
||||
⬝ (ap02 f r ◾ ap02 f s)
|
||||
⬝ (ap_pp f p' q')⁻¹ :=
|
||||
rec_on r (rec_on s (rec_on q (rec_on p idp)))
|
||||
-- rec_on r (rec_on s (rec_on p (rec_on q idp)))
|
||||
|
||||
definition apD02 {p q : x ≈ y} (f : Π x, P x) (r : p ≈ q) :
|
||||
apD f p ≈ transport2 P r (f x) ⬝ apD f q :=
|
||||
rec_on r (concat_1p _)⁻¹
|
||||
|
||||
-- And now for a lemma whose statement is much longer than its proof.
|
||||
definition apD02_pp (P : A → Type) (f : Π x:A, P x) {x y : A}
|
||||
{p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) :
|
||||
apD02 f (r1 ⬝ r2) ≈ apD02 f r1
|
||||
⬝ whiskerL (transport2 P r1 (f x)) (apD02 f r2)
|
||||
⬝ concat_p_pp _ _ _
|
||||
⬝ (whiskerR ((transport2_p2p P r1 r2 (f x))⁻¹) (apD f p3)) :=
|
||||
rec_on r2 (rec_on r1 (rec_on p1 idp))
|
||||
end path
|
||||
namespace path
|
||||
variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D}
|
||||
|
||||
theorem congr_arg2 (f : A → B → C) (Ha : a ≈ a') (Hb : b ≈ b') : f a b ≈ f a' b' :=
|
||||
rec_on Ha (rec_on Hb idp)
|
||||
|
||||
theorem congr_arg3 (f : A → B → C → D) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c')
|
||||
: f a b c ≈ f a' b' c' :=
|
||||
rec_on Ha (congr_arg2 (f a) Hb Hc)
|
||||
|
||||
theorem congr_arg4 (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' :=
|
||||
rec_on Ha (congr_arg3 (f a) Hb Hc Hd)
|
||||
|
||||
end path
|
||||
|
||||
namespace path
|
||||
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
|
||||
{E : Πa b c, D a b c → Type} {F : Type}
|
||||
variables {a a' : A}
|
||||
{b : B a} {b' : B a'}
|
||||
{c : C a b} {c' : C a' b'}
|
||||
{d : D a b c} {d' : D a' b' c'}
|
||||
|
||||
theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a ≈ a') (Hb : Ha ▹ b ≈ b')
|
||||
: f a b ≈ f a' b' :=
|
||||
rec_on Hb (rec_on Ha idp)
|
||||
|
||||
/- From the Coq version:
|
||||
|
||||
-- ** Tactics, hints, and aliases
|
||||
|
||||
-- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))].
|
||||
-- Given as a notation not a definition so that the resultant terms are literally instances of
|
||||
-- [concat], with no unfolding required.
|
||||
Notation concatR := (λp q, concat q p).
|
||||
|
||||
Hint Resolve
|
||||
concat_1p concat_p1 concat_p_pp
|
||||
inv_pp inv_V
|
||||
: path_hints.
|
||||
|
||||
(* First try at a paths db
|
||||
We want the RHS of the equation to become strictly simpler
|
||||
Hint Rewrite
|
||||
⬝concat_p1
|
||||
⬝concat_1p
|
||||
⬝concat_p_pp (* there is a choice here !*)
|
||||
⬝concat_pV
|
||||
⬝concat_Vp
|
||||
⬝concat_V_pp
|
||||
⬝concat_p_Vp
|
||||
⬝concat_pp_V
|
||||
⬝concat_pV_p
|
||||
(*⬝inv_pp*) (* I am not sure about this one
|
||||
⬝inv_V
|
||||
⬝moveR_Mp
|
||||
⬝moveR_pM
|
||||
⬝moveL_Mp
|
||||
⬝moveL_pM
|
||||
⬝moveL_1M
|
||||
⬝moveL_M1
|
||||
⬝moveR_M1
|
||||
⬝moveR_1M
|
||||
⬝ap_1
|
||||
(* ⬝ap_pp
|
||||
⬝ap_p_pp ?*)
|
||||
⬝inverse_ap
|
||||
⬝ap_idmap
|
||||
(* ⬝ap_compose
|
||||
⬝ap_compose'*)
|
||||
⬝ap_const
|
||||
(* Unsure about naturality of [ap], was absent in the old implementation*)
|
||||
⬝apD10_1
|
||||
:paths.
|
||||
|
||||
Ltac hott_simpl :=
|
||||
autorewrite with paths in * |- * ; auto with path_hints.
|
||||
|
||||
-/
|
||||
end path
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jakob von Raumer
|
||||
-- Ported from Coq HoTT
|
||||
import hott.path hott.trunc data.sigma data.prod
|
||||
|
||||
open path prod truncation
|
||||
|
||||
structure is_pointed [class] (A : Type) :=
|
||||
(point : A)
|
||||
|
||||
namespace is_pointed
|
||||
variables {A B : Type} (f : A → B)
|
||||
|
||||
-- Any contractible type is pointed
|
||||
protected definition contr [instance] [H : is_contr A] : is_pointed A :=
|
||||
is_pointed.mk (center A)
|
||||
|
||||
-- A pi type with a pointed target is pointed
|
||||
protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]
|
||||
: is_pointed (Πx, P x) :=
|
||||
is_pointed.mk (λx, point (P x))
|
||||
|
||||
-- A sigma type of pointed components is pointed
|
||||
protected definition sigma [instance] {P : A → Type} [G : is_pointed A]
|
||||
[H : is_pointed (P (point A))] : is_pointed (Σx, P x) :=
|
||||
is_pointed.mk (sigma.dpair (point A) (point (P (point A))))
|
||||
|
||||
protected definition prod [H1 : is_pointed A] [H2 : is_pointed B]
|
||||
: is_pointed (A × B) :=
|
||||
is_pointed.mk (prod.mk (point A) (point B))
|
||||
|
||||
protected definition loop_space (a : A) : is_pointed (a ≈ a) :=
|
||||
is_pointed.mk idp
|
||||
|
||||
end is_pointed
|
||||
|
|
@ -1,255 +0,0 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Jeremy Avigad, Floris van Doorn
|
||||
-- Ported from Coq HoTT
|
||||
|
||||
import .path .logic data.nat.basic data.empty data.unit data.sigma .equiv
|
||||
open path nat sigma unit
|
||||
set_option pp.universes true
|
||||
|
||||
-- Truncation levels
|
||||
-- -----------------
|
||||
|
||||
-- TODO: make everything universe polymorphic
|
||||
|
||||
-- TODO: everything definition with a hprop as codomain can be a theorem?
|
||||
|
||||
/- truncation indices -/
|
||||
|
||||
namespace truncation
|
||||
|
||||
inductive trunc_index : Type₁ :=
|
||||
minus_two : trunc_index,
|
||||
trunc_S : trunc_index → trunc_index
|
||||
|
||||
postfix `.+1`:(max+1) := trunc_index.trunc_S
|
||||
postfix `.+2`:(max+1) := λn, (n .+1 .+1)
|
||||
notation `-2` := trunc_index.minus_two
|
||||
notation `-1` := (-2.+1)
|
||||
|
||||
namespace trunc_index
|
||||
definition add (n m : trunc_index) : trunc_index :=
|
||||
trunc_index.rec_on m n (λ k l, l .+1)
|
||||
|
||||
definition leq (n m : trunc_index) : Type₁ :=
|
||||
trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
|
||||
end trunc_index
|
||||
|
||||
-- Coq calls this `-2+`, but `+2+` looks more natural, since trunc_index_add 0 0 = 2
|
||||
infix `+2+`:65 := trunc_index.add
|
||||
|
||||
notation x <= y := trunc_index.leq x y
|
||||
notation x ≤ y := trunc_index.leq x y
|
||||
|
||||
namespace trunc_index
|
||||
definition succ_le {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H
|
||||
definition succ_le_cancel {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := H
|
||||
definition minus_two_le (n : trunc_index) : -2 ≤ n := star
|
||||
definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := H
|
||||
end trunc_index
|
||||
|
||||
definition nat_to_trunc_index [coercion] (n : nat) : trunc_index :=
|
||||
nat.rec_on n (-1.+1) (λ n k, k.+1)
|
||||
|
||||
/- truncated types -/
|
||||
|
||||
/-
|
||||
Just as in Coq HoTT we define an internal version of contractibility and is_trunc, but we only
|
||||
use `is_trunc` and `is_contr`
|
||||
-/
|
||||
|
||||
structure contr_internal (A : Type) :=
|
||||
(center : A) (contr : Π(a : A), center ≈ a)
|
||||
|
||||
definition is_trunc_internal (n : trunc_index) : Type → Type :=
|
||||
trunc_index.rec_on n (λA, contr_internal A)
|
||||
(λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
|
||||
|
||||
structure is_trunc [class] (n : trunc_index) (A : Type) :=
|
||||
(to_internal : is_trunc_internal n A)
|
||||
|
||||
-- should this be notation or definitions?
|
||||
notation `is_contr` := is_trunc -2
|
||||
notation `is_hprop` := is_trunc -1
|
||||
notation `is_hset` := is_trunc (nat_to_trunc_index nat.zero)
|
||||
-- definition is_contr := is_trunc -2
|
||||
-- definition is_hprop := is_trunc -1
|
||||
-- definition is_hset := is_trunc 0
|
||||
|
||||
variables {A B : Type}
|
||||
|
||||
-- TODO: rename to is_trunc_succ
|
||||
definition is_trunc_succ (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x ≈ y)]
|
||||
: is_trunc n.+1 A :=
|
||||
is_trunc.mk (λ x y, !is_trunc.to_internal)
|
||||
|
||||
-- TODO: rename to is_trunc_path
|
||||
definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
|
||||
is_trunc.mk (!is_trunc.to_internal x y)
|
||||
|
||||
/- contractibility -/
|
||||
|
||||
definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A :=
|
||||
is_trunc.mk (contr_internal.mk center contr)
|
||||
|
||||
definition center (A : Type) [H : is_contr A] : A :=
|
||||
@contr_internal.center A !is_trunc.to_internal
|
||||
|
||||
definition contr [H : is_contr A] (a : A) : !center ≈ a :=
|
||||
@contr_internal.contr A !is_trunc.to_internal a
|
||||
|
||||
definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
|
||||
contr x⁻¹ ⬝ (contr y)
|
||||
|
||||
definition path2_contr {A : Type} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
|
||||
have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
|
||||
K p⁻¹ ⬝ K q
|
||||
|
||||
definition contr_paths_contr [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
|
||||
is_contr.mk !path_contr (λ p, !path2_contr)
|
||||
|
||||
/- truncation is upward close -/
|
||||
|
||||
-- n-types are also (n+1)-types
|
||||
definition trunc_succ [instance] (A : Type) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
|
||||
trunc_index.rec_on n
|
||||
(λ A (H : is_contr A), !is_trunc_succ)
|
||||
(λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ _ _ (λ x y, IH _ !succ_is_trunc))
|
||||
A H
|
||||
--in the proof the type of H is given explicitly to make it available for class inference
|
||||
|
||||
|
||||
definition trunc_leq (A : Type) (n m : trunc_index) (Hnm : n ≤ m)
|
||||
[Hn : is_trunc n A] : is_trunc m A :=
|
||||
have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
|
||||
λ k A, trunc_index.cases_on k
|
||||
(λh1 h2, h2)
|
||||
(λk h1 h2, empty.elim (is_trunc -2 A) (trunc_index.not_succ_le_minus_two h1)),
|
||||
have step : Π (m : trunc_index)
|
||||
(IHm : Π (n : trunc_index) (A : Type), n ≤ m → is_trunc n A → is_trunc m A)
|
||||
(n : trunc_index) (A : Type)
|
||||
(Hnm : n ≤ m .+1) (Hn : is_trunc n A), is_trunc m .+1 A, from
|
||||
λm IHm n, trunc_index.rec_on n
|
||||
(λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn))
|
||||
(λn IHn A Hnm (Hn : is_trunc n.+1 A),
|
||||
@is_trunc_succ A m (λx y, IHm n (x≈y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)),
|
||||
trunc_index.rec_on m base step n A Hnm Hn
|
||||
|
||||
-- the following cannot be instances in their current form, because it is looping
|
||||
definition trunc_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
|
||||
trunc_index.rec_on n H _
|
||||
|
||||
definition trunc_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
|
||||
: is_trunc (n.+1) A :=
|
||||
trunc_leq A -1 (n.+1) star
|
||||
|
||||
definition trunc_hset (A : Type) (n : trunc_index) [H : is_hset A]
|
||||
: is_trunc (n.+2) A :=
|
||||
trunc_leq A 0 (n.+2) star
|
||||
|
||||
/- hprops -/
|
||||
|
||||
definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y :=
|
||||
@center _ !succ_is_trunc
|
||||
|
||||
definition contr_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A :=
|
||||
is_contr.mk x (λy, !is_hprop.elim)
|
||||
|
||||
--Coq has the following as instance, but doesn't look too useful
|
||||
definition hprop_inhabited_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
|
||||
@is_trunc_succ A -2
|
||||
(λx y,
|
||||
have H2 [visible] : is_contr A, from H x,
|
||||
!contr_paths_contr)
|
||||
|
||||
definition is_hprop.mk {A : Type} (H : ∀x y : A, x ≈ y) : is_hprop A :=
|
||||
hprop_inhabited_contr (λ x, is_contr.mk x (H x))
|
||||
|
||||
/- hsets -/
|
||||
|
||||
definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
|
||||
@is_trunc_succ _ _ (λ x y, is_hprop.mk (H x y))
|
||||
|
||||
definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q :=
|
||||
@is_hprop.elim _ !succ_is_trunc p q
|
||||
|
||||
/- instances -/
|
||||
|
||||
definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
|
||||
is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp))
|
||||
|
||||
-- definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry
|
||||
|
||||
definition unit_contr [instance] : is_contr unit :=
|
||||
is_contr.mk star (λp, unit.rec_on p idp)
|
||||
|
||||
definition empty_hprop [instance] : is_hprop empty :=
|
||||
is_hprop.mk (λx, !empty.elim x)
|
||||
|
||||
/- truncated universe -/
|
||||
|
||||
structure trunctype (n : trunc_index) :=
|
||||
(trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type)
|
||||
coercion trunctype.trunctype_type
|
||||
|
||||
notation n `-Type` := trunctype n
|
||||
notation `hprop` := -1-Type
|
||||
notation `hset` := 0-Type
|
||||
|
||||
definition hprop.mk := @trunctype.mk -1
|
||||
definition hset.mk := @trunctype.mk 0
|
||||
|
||||
--what does the following line in Coq do?
|
||||
--Canonical Structure default_TruncType := fun n T P => (@BuildTruncType n T P).
|
||||
|
||||
/- interaction with equivalences -/
|
||||
|
||||
section
|
||||
open is_equiv equiv
|
||||
|
||||
--should we remove the following two theorems as they are special cases of "trunc_equiv"
|
||||
definition equiv_preserves_contr (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) :=
|
||||
is_contr.mk (f (center A)) (λp, moveR_M f !contr)
|
||||
|
||||
theorem contr_equiv (H : A ≃ B) [HA: is_contr A] : is_contr B :=
|
||||
@equiv_preserves_contr _ _ (to_fun H) (to_is_equiv H) _
|
||||
|
||||
definition contr_equiv_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
|
||||
equiv.mk
|
||||
(λa, center B)
|
||||
(is_equiv.adjointify (λa, center B) (λb, center A) contr contr)
|
||||
|
||||
definition trunc_equiv (n : trunc_index) (f : A → B) [H : is_equiv f] [HA : is_trunc n A]
|
||||
: is_trunc n B :=
|
||||
trunc_index.rec_on n
|
||||
(λA (HA : is_contr A) B f (H : is_equiv f), !equiv_preserves_contr)
|
||||
(λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ _ _ (λ x y : B,
|
||||
IH (f⁻¹ x ≈ f⁻¹ y) !succ_is_trunc (x ≈ y) ((ap (f⁻¹))⁻¹) !inv_closed))
|
||||
A HA B f H
|
||||
|
||||
definition trunc_equiv' (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B :=
|
||||
trunc_equiv n (to_fun f)
|
||||
|
||||
definition isequiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
|
||||
: is_equiv f :=
|
||||
is_equiv.adjointify f g (λb, !is_hprop.elim) (λa, !is_hprop.elim)
|
||||
|
||||
-- definition equiv_iff_hprop_uncurried [HA : is_hprop A] [HB : is_hprop B] : (A ↔ B) → (A ≃ B) := sorry
|
||||
|
||||
definition equiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : A ≃ B :=
|
||||
equiv.mk f (isequiv_iff_hprop f g)
|
||||
end
|
||||
|
||||
/- interaction with the Unit type -/
|
||||
|
||||
-- A contractible type is equivalent to [Unit]. *)
|
||||
definition equiv_contr_unit [H : is_contr A] : A ≃ unit :=
|
||||
equiv.mk (λ (x : A), ⋆)
|
||||
(is_equiv.mk (λ (u : unit), center A)
|
||||
(λ (u : unit), unit.rec_on u idp)
|
||||
(λ (x : A), contr x)
|
||||
(λ (x : A), (!ap_const)⁻¹))
|
||||
|
||||
-- TODO: port "Truncated morphisms"
|
||||
|
||||
end truncation
|
||||
|
|
@ -1,153 +0,0 @@
|
|||
/-
|
||||
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
|
||||
|
||||
Theorems about W-types (well-founded trees)
|
||||
-/
|
||||
|
||||
import .sigma .pi
|
||||
open path sigma sigma.ops equiv is_equiv
|
||||
|
||||
|
||||
inductive Wtype {A : Type} (B : A → Type) :=
|
||||
sup : Π(a : A), (B a → Wtype B) → Wtype B
|
||||
|
||||
namespace Wtype
|
||||
notation `W` binders `,` r:(scoped B, Wtype B) := r
|
||||
|
||||
universe variables u v
|
||||
variables {A A' : Type.{u}} {B B' : A → Type.{v}} {C : Π(a : A), B a → Type}
|
||||
{a a' : A} {f : B a → W a, B a} {f' : B a' → W a, B a} {w w' : W(a : A), B a}
|
||||
|
||||
definition pr1 (w : W(a : A), B a) : A :=
|
||||
Wtype.rec_on w (λa f IH, a)
|
||||
|
||||
definition pr2 (w : W(a : A), B a) : B (pr1 w) → W(a : A), B a :=
|
||||
Wtype.rec_on w (λa f IH, f)
|
||||
|
||||
namespace ops
|
||||
postfix `.1`:(max+1) := Wtype.pr1
|
||||
postfix `.2`:(max+1) := Wtype.pr2
|
||||
notation `⟨` a `,` f `⟩`:0 := Wtype.sup a f --input ⟨ ⟩ as \< \>
|
||||
end ops
|
||||
open ops
|
||||
|
||||
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'⟩ :=
|
||||
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' :=
|
||||
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 :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition pr2_path (p : w ≈ w') : pr1_path p ▹ w.2 ≈ w'.2 :=
|
||||
path.rec_on p idp
|
||||
|
||||
namespace ops
|
||||
postfix `..1`:(max+1) := pr1_path
|
||||
postfix `..2`:(max+1) := pr2_path
|
||||
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 :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
apply (cases_on w), intros (w1, w2),
|
||||
apply (cases_on w'), intros (w1', w2', p), generalize w2', --change to revert
|
||||
apply (path.rec_on p), intros (w2', q),
|
||||
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 :=
|
||||
(!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 :=
|
||||
(!sup_path_W)..2
|
||||
|
||||
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 :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
apply (cases_on w), intros (w1, w2),
|
||||
apply (cases_on w'), intros (w1', w2', p), generalize w2',
|
||||
apply (path.rec_on p), intros (w2', q),
|
||||
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' :=
|
||||
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 :=
|
||||
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 :=
|
||||
(!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 :=
|
||||
(!sup_path_W_uncurried)..2
|
||||
|
||||
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 :=
|
||||
destruct pq transport_pr1_path_W
|
||||
|
||||
definition isequiv_path_W /-[instance]-/ (w w' : W a, B a)
|
||||
: is_equiv (@path_W_uncurried A B w w') :=
|
||||
adjointify path_W_uncurried
|
||||
(λp, dpair (p..1) (p..2))
|
||||
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') :=
|
||||
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)
|
||||
(H : ∀ (a a' : A) (f : B a → W a, B a) (f' : B a' → W a, B a),
|
||||
(∀ (b : B a) (b' : B a'), P (f b) (f' b')) → P (sup a f) (sup a' f')) : P w w' :=
|
||||
begin
|
||||
revert w',
|
||||
apply (rec_on w), intros (a, f, IH, w'),
|
||||
apply (cases_on w'), intros (a', f'),
|
||||
apply H, intros (b, b'),
|
||||
apply IH
|
||||
end
|
||||
|
||||
/- truncatedness -/
|
||||
open truncation
|
||||
definition trunc_W [FUN : funext.{v (max 1 u v)}] (n : trunc_index) [HA : is_trunc (n.+1) A]
|
||||
: is_trunc (n.+1) (W a, B a) :=
|
||||
begin
|
||||
fapply is_trunc_succ, intros (w, w'),
|
||||
apply (double_induction_on w w'), intros (a, a', f, f', IH),
|
||||
fapply trunc_equiv',
|
||||
apply equiv_path_W,
|
||||
apply trunc_sigma,
|
||||
fapply (succ_is_trunc n),
|
||||
intro p, revert IH, generalize f', --change to revert after simpl
|
||||
apply (path.rec_on p), intros (f', IH),
|
||||
apply pi.trunc_path_pi, intro b,
|
||||
apply IH
|
||||
end
|
||||
|
||||
end Wtype
|
||||
|
|
@ -1,123 +0,0 @@
|
|||
/-
|
||||
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
|
||||
Ported from Coq HoTT
|
||||
|
||||
Theorems about pi-types (dependent function spaces)
|
||||
-/
|
||||
|
||||
import ..trunc ..axioms.funext .sigma
|
||||
open path equiv is_equiv funext
|
||||
|
||||
namespace pi
|
||||
universe variables l k
|
||||
variables {A A' : Type.{l}} {B : A → Type.{k}} {C : Πa, B a → Type}
|
||||
{D : Πa b, C a b → Type}
|
||||
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a}
|
||||
|
||||
/- Paths -/
|
||||
|
||||
/- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g].
|
||||
|
||||
This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path: -/
|
||||
|
||||
/- Now we show how these things compute. -/
|
||||
|
||||
definition apD10_path_pi [H : funext] (h : f ∼ g) : apD10 (path_pi h) ∼ h :=
|
||||
apD10 (retr apD10 h)
|
||||
|
||||
definition path_pi_eta [H : funext] (p : f ≈ g) : path_pi (apD10 p) ≈ p :=
|
||||
sect apD10 p
|
||||
|
||||
definition path_pi_idp [H : funext] : path_pi (λx : A, idpath (f x)) ≈ idpath f :=
|
||||
!path_pi_eta
|
||||
|
||||
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
|
||||
|
||||
definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f ≈ g) ≃ (f ∼ g) :=
|
||||
equiv.mk _ !funext.ap
|
||||
|
||||
definition is_equiv_path_pi [instance] [H : funext] (f g : Πx, B x)
|
||||
: is_equiv (@path_pi _ _ _ f g) :=
|
||||
inv_closed apD10
|
||||
|
||||
definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f ≈ g) :=
|
||||
equiv.mk _ !is_equiv_path_pi
|
||||
|
||||
|
||||
/- Transport -/
|
||||
|
||||
protected definition transport (p : a ≈ a') (f : Π(b : B a), C a b)
|
||||
: (transport (λa, Π(b : B a), C a b) p f)
|
||||
∼ (λb, transport (C a') !transport_pV (transportD _ _ p _ (f (p⁻¹ ▹ b)))) :=
|
||||
path.rec_on p (λx, idp)
|
||||
|
||||
/- A special case of [transport_pi] where the type [B] does not depend on [A],
|
||||
and so it is just a fixed type [B]. -/
|
||||
definition transport_constant {C : A → A' → Type} (p : a ≈ a') (f : Π(b : A'), C a b)
|
||||
: (path.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, path.transport (λa, C a b) p (f b)) :=
|
||||
path.rec_on p (λx, idp)
|
||||
|
||||
/- Maps on paths -/
|
||||
|
||||
/- The action of maps given by lambda. -/
|
||||
definition ap_lambdaD [H : funext] {C : A' → Type} (p : a ≈ a') (f : Πa b, C b) :
|
||||
ap (λa b, f a b) p ≈ path_pi (λb, ap (λa, f a b) p) :=
|
||||
begin
|
||||
apply (path.rec_on p),
|
||||
apply inverse,
|
||||
apply path_pi_idp
|
||||
end
|
||||
|
||||
/- Dependent paths -/
|
||||
|
||||
/- with more implicit arguments the conclusion of the following theorem is
|
||||
(Π(b : B a), transportD B C p b (f b) ≈ g (path.transport B p b)) ≃
|
||||
(path.transport (λa, Π(b : B a), C a b) p f ≈ g) -/
|
||||
definition dpath_pi [H : funext] (p : a ≈ a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
|
||||
: (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) ≃ (p ▹ f ≈ g) :=
|
||||
path.rec_on p (λg, !homotopy_equiv_path) g
|
||||
|
||||
section open sigma.ops
|
||||
/- more implicit arguments:
|
||||
(Π(b : B a), path.transport C (sigma.path p idp) (f b) ≈ g (p ▹ b)) ≃
|
||||
(Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) ≈ g (path.transport B p b)) -/
|
||||
definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a ≈ a')
|
||||
(f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
|
||||
(Π(b : B a), (sigma.path p idp) ▹ (f b) ≈ g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) :=
|
||||
path.rec_on p (λg, !equiv.refl) g
|
||||
end
|
||||
|
||||
/- truncation -/
|
||||
|
||||
open truncation
|
||||
definition trunc_pi [instance] [H : funext.{l k}] (B : A → Type.{k}) (n : trunc_index)
|
||||
[H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
|
||||
begin
|
||||
reverts (B, H),
|
||||
apply (trunc_index.rec_on n),
|
||||
intros (B, H),
|
||||
fapply is_contr.mk,
|
||||
intro a, apply center, apply H, --remove "apply H" when term synthesis works correctly
|
||||
intro f, apply path_pi,
|
||||
intro x, apply (contr (f x)),
|
||||
intros (n, IH, B, H),
|
||||
fapply is_trunc_succ, intros (f, g),
|
||||
fapply trunc_equiv',
|
||||
apply equiv.symm, apply path_equiv_homotopy,
|
||||
apply IH,
|
||||
intro a,
|
||||
show is_trunc n (f a ≈ g a), from
|
||||
succ_is_trunc n (f a) (g a)
|
||||
end
|
||||
|
||||
definition trunc_path_pi [instance] [H : funext.{l k}] (n : trunc_index) (f g : Πa, B a)
|
||||
[H : ∀a, is_trunc n (f a ≈ g a)] : is_trunc n (f ≈ g) :=
|
||||
begin
|
||||
apply trunc_equiv', apply equiv.symm,
|
||||
apply path_equiv_homotopy,
|
||||
apply trunc_pi, exact H,
|
||||
end
|
||||
|
||||
end pi
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
/-
|
||||
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
|
||||
Ported from Coq HoTT
|
||||
|
||||
Theorems about products
|
||||
-/
|
||||
|
||||
import ..trunc data.prod
|
||||
open path equiv is_equiv truncation prod
|
||||
|
||||
variables {A A' B B' C D : Type}
|
||||
{a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}
|
||||
|
||||
namespace prod
|
||||
|
||||
-- prod.eta is already used for the eta rule for strict equality
|
||||
protected definition peta (u : A × B) : (pr₁ u , pr₂ u) ≈ u :=
|
||||
destruct u (λu1 u2, idp)
|
||||
|
||||
definition pair_path (pa : a ≈ a') (pb : b ≈ b') : (a , b) ≈ (a' , b') :=
|
||||
path.rec_on pa (path.rec_on pb idp)
|
||||
|
||||
protected definition path : (pr₁ u ≈ pr₁ v) → (pr₂ u ≈ pr₂ v) → u ≈ v :=
|
||||
begin
|
||||
apply (prod.rec_on u), intros (a₁, b₁),
|
||||
apply (prod.rec_on v), intros (a₂, b₂, H₁, H₂),
|
||||
apply (transport _ (peta (a₁, b₁))),
|
||||
apply (transport _ (peta (a₂, b₂))),
|
||||
apply (pair_path H₁ H₂),
|
||||
end
|
||||
|
||||
/- Symmetry -/
|
||||
|
||||
definition isequiv_flip [instance] (A B : Type) : is_equiv (@flip A B) :=
|
||||
adjointify flip
|
||||
flip
|
||||
(λu, destruct u (λb a, idp))
|
||||
(λu, destruct u (λa b, idp))
|
||||
|
||||
definition symm_equiv (A B : Type) : A × B ≃ B × A :=
|
||||
equiv.mk flip _
|
||||
|
||||
-- trunc_prod is defined in sigma
|
||||
|
||||
end prod
|
||||
|
|
@ -1,474 +0,0 @@
|
|||
/-
|
||||
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
|
||||
Ported from Coq HoTT
|
||||
|
||||
Theorems about sigma-types (dependent sums)
|
||||
-/
|
||||
|
||||
import ..trunc .prod ..axioms.funext
|
||||
open path sigma sigma.ops equiv is_equiv
|
||||
|
||||
namespace sigma
|
||||
infixr [local] ∘ := function.compose --remove
|
||||
variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
|
||||
{D : Πa b, C a b → Type}
|
||||
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
|
||||
|
||||
-- sigma.eta is already used for the eta rule for strict equality
|
||||
protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ ≈ u :=
|
||||
destruct u (λu1 u2, idp)
|
||||
|
||||
definition eta2 (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ ≈ u :=
|
||||
destruct u (λu1 u2, destruct u2 (λu21 u22, idp))
|
||||
|
||||
definition eta3 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ ≈ u :=
|
||||
destruct u (λu1 u2, destruct u2 (λu21 u22, destruct u22 (λu221 u222, idp)))
|
||||
|
||||
definition dpair_eq_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
|
||||
path.rec_on p (λb b' q, path.rec_on q idp) b b' q
|
||||
|
||||
/- In Coq they often have to give u and v explicitly -/
|
||||
protected definition path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
|
||||
destruct u
|
||||
(λu1 u2, destruct v (λ v1 v2, dpair_eq_dpair))
|
||||
p q
|
||||
|
||||
/- Projections of paths from a total space -/
|
||||
|
||||
definition path_pr1 (p : u ≈ v) : u.1 ≈ v.1 :=
|
||||
ap dpr1 p
|
||||
|
||||
postfix `..1`:(max+1) := path_pr1
|
||||
|
||||
definition path_pr2 (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 :=
|
||||
path.rec_on p idp
|
||||
--Coq uses the following proof, which only computes if u,v are dpairs AND p is idp
|
||||
--(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p
|
||||
|
||||
postfix `..2`:(max+1) := path_pr2
|
||||
|
||||
definition dpair_sigma_path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: dpair (sigma.path p q)..1 (sigma.path p q)..2 ≈ ⟨p, q⟩ :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert
|
||||
apply (path.rec_on p), intros (v2, q),
|
||||
apply (path.rec_on q), apply idp
|
||||
end
|
||||
|
||||
definition sigma_path_pr1 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (sigma.path p q)..1 ≈ p :=
|
||||
(!dpair_sigma_path)..1
|
||||
|
||||
definition sigma_path_pr2 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: sigma_path_pr1 p q ▹ (sigma.path p q)..2 ≈ q :=
|
||||
(!dpair_sigma_path)..2
|
||||
|
||||
definition sigma_path_eta (p : u ≈ v) : sigma.path (p..1) (p..2) ≈ p :=
|
||||
begin
|
||||
apply (path.rec_on p),
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply idp
|
||||
end
|
||||
|
||||
definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: transport (λx, B' x.1) (sigma.path p q) ≈ transport B' p :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2, p), generalize v2,
|
||||
apply (path.rec_on p), intros (v2, q),
|
||||
apply (path.rec_on q), apply idp
|
||||
end
|
||||
|
||||
/- the uncurried version of sigma_path. We will prove that this is an equivalence -/
|
||||
|
||||
definition sigma_path_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
|
||||
destruct pq sigma.path
|
||||
|
||||
definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
|
||||
: dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 ≈ pq :=
|
||||
destruct pq dpair_sigma_path
|
||||
|
||||
definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
|
||||
: (sigma_path_uncurried pq)..1 ≈ pq.1 :=
|
||||
(!dpair_sigma_path_uncurried)..1
|
||||
|
||||
definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
|
||||
: (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 ≈ pq.2 :=
|
||||
(!dpair_sigma_path_uncurried)..2
|
||||
|
||||
definition sigma_path_eta_uncurried (p : u ≈ v) : sigma_path_uncurried (dpair p..1 p..2) ≈ p :=
|
||||
!sigma_path_eta
|
||||
|
||||
definition transport_sigma_path_dpr1_uncurried {B' : A → Type}
|
||||
(pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
|
||||
: transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) ≈ transport B' pq.1 :=
|
||||
destruct pq transport_dpr1_sigma_path
|
||||
|
||||
definition is_equiv_sigma_path [instance] (u v : Σa, B a)
|
||||
: is_equiv (@sigma_path_uncurried A B u v) :=
|
||||
adjointify sigma_path_uncurried
|
||||
(λp, ⟨p..1, p..2⟩)
|
||||
sigma_path_eta_uncurried
|
||||
dpair_sigma_path_uncurried
|
||||
|
||||
definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
|
||||
equiv.mk sigma_path_uncurried !is_equiv_sigma_path
|
||||
|
||||
definition dpair_eq_dpair_pp_pp (p1 : a ≈ a' ) (q1 : p1 ▹ b ≈ b' )
|
||||
(p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
|
||||
dpair_eq_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
|
||||
≈ dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 :=
|
||||
begin
|
||||
reverts (b', p2, b'', q1, q2),
|
||||
apply (path.rec_on p1), intros (b', p2),
|
||||
apply (path.rec_on p2), intros (b'', q1),
|
||||
apply (path.rec_on q1), intro q2,
|
||||
apply (path.rec_on q2), apply idp
|
||||
end
|
||||
|
||||
definition sigma_path_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2)
|
||||
(p2 : v.1 ≈ w.1) (q2 : p2 ▹ v.2 ≈ w.2) :
|
||||
sigma.path (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
|
||||
≈ sigma.path p1 q1 ⬝ sigma.path p2 q2 :=
|
||||
begin
|
||||
reverts (p1, q1, p2, q2),
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2),
|
||||
apply (destruct w), intros,
|
||||
apply dpair_eq_dpair_pp_pp
|
||||
end
|
||||
|
||||
definition dpair_eq_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
|
||||
dpair_eq_dpair p q ≈ dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
|
||||
begin
|
||||
reverts (b', q),
|
||||
apply (path.rec_on p), intros (b', q),
|
||||
apply (path.rec_on q), apply idp
|
||||
end
|
||||
|
||||
/- path_pr1 commutes with the groupoid structure. -/
|
||||
|
||||
definition path_pr1_idp (u : Σa, B a) : (idpath u)..1 ≈ idpath (u.1) := idp
|
||||
definition path_pr1_pp (p : u ≈ v) (q : v ≈ w) : (p ⬝ q) ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp
|
||||
definition path_pr1_V (p : u ≈ v) : p⁻¹ ..1 ≈ (p..1)⁻¹ := !ap_V
|
||||
|
||||
/- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/
|
||||
|
||||
definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ dpair_eq_dpair idp q :=
|
||||
path.rec_on q idp
|
||||
|
||||
/- Dependent transport is the same as transport along a sigma_path. -/
|
||||
|
||||
definition transportD_eq_transport (p : a ≈ a') (c : C a b) :
|
||||
p ▹D c ≈ transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
|
||||
path.rec_on p idp
|
||||
|
||||
definition sigma_path_eq_sigma_path {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'}
|
||||
(r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : sigma.path p1 p2 ≈ sigma.path q1 q2 :=
|
||||
path.rec_on r
|
||||
proof (λq2 s, path.rec_on s idp) qed
|
||||
q2
|
||||
s
|
||||
-- begin
|
||||
-- reverts (q2, s),
|
||||
-- apply (path.rec_on r), intros (q2, s),
|
||||
-- apply (path.rec_on s), apply idp
|
||||
-- end
|
||||
|
||||
|
||||
/- A path between paths in a total space is commonly shown component wise. -/
|
||||
definition path_sigma_path {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
|
||||
begin
|
||||
reverts (q, r, s),
|
||||
apply (path.rec_on p),
|
||||
apply (destruct u), intros (u1, u2, q, r, s),
|
||||
apply concat, rotate 1,
|
||||
apply sigma_path_eta,
|
||||
apply (sigma_path_eq_sigma_path r s)
|
||||
end
|
||||
|
||||
/- In Coq they often have to give u and v explicitly when using the following definition -/
|
||||
definition path_sigma_path_uncurried {p q : u ≈ v}
|
||||
(rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
|
||||
destruct rs path_sigma_path
|
||||
|
||||
/- Transport -/
|
||||
|
||||
/- The concrete description of transport in sigmas (and also pis) is rather trickier than in the other types. In particular, these cannot be described just in terms of transport in simpler types; they require also the dependent transport [transportD].
|
||||
|
||||
In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory). A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/
|
||||
|
||||
definition transport_eq (p : a ≈ a') (bc : Σ(b : B a), C a b)
|
||||
: p ▹ bc ≈ ⟨p ▹ bc.1, p ▹D bc.2⟩ :=
|
||||
begin
|
||||
apply (path.rec_on p),
|
||||
apply (destruct bc), intros (b, c),
|
||||
apply idp
|
||||
end
|
||||
|
||||
/- The special case when the second variable doesn't depend on the first is simpler. -/
|
||||
definition transport_eq_deg {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b)
|
||||
: p ▹ bc ≈ ⟨bc.1, p ▹ bc.2⟩ :=
|
||||
begin
|
||||
apply (path.rec_on p),
|
||||
apply (destruct bc), intros (b, c),
|
||||
apply idp
|
||||
end
|
||||
|
||||
/- Or if the second variable contains a first component that doesn't depend on the first. -/
|
||||
|
||||
definition transport_eq_4deg {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
|
||||
(bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd ≈ ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ :=
|
||||
begin
|
||||
revert bcd,
|
||||
apply (path.rec_on p), intro bcd,
|
||||
apply (destruct bcd), intros (b, cd),
|
||||
apply (destruct cd), intros (c, d),
|
||||
apply idp
|
||||
end
|
||||
|
||||
/- Functorial action -/
|
||||
variables (f : A → A') (g : Πa, B a → B' (f a))
|
||||
|
||||
protected definition functor (u : Σa, B a) : Σa', B' a' :=
|
||||
⟨f u.1, g u.1 u.2⟩
|
||||
|
||||
/- Equivalences -/
|
||||
|
||||
--TODO: remove explicit arguments of is_equiv
|
||||
definition is_equiv_functor [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
|
||||
: is_equiv (functor f g) :=
|
||||
adjointify (functor f g)
|
||||
(functor (f⁻¹) (λ(a' : A') (b' : B' a'),
|
||||
((g (f⁻¹ a'))⁻¹ (transport B' (retr f a'⁻¹) b'))))
|
||||
begin
|
||||
intro u',
|
||||
apply (destruct u'), intros (a', b'),
|
||||
apply (sigma.path (retr f a')),
|
||||
-- "rewrite retr (g (f⁻¹ a'))"
|
||||
apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))),
|
||||
show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') ≈ b',
|
||||
from transport_pV B' (retr f a') b'
|
||||
end
|
||||
begin
|
||||
intro u,
|
||||
apply (destruct u), intros (a, b),
|
||||
apply (sigma.path (sect f a)),
|
||||
show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) ≈ b,
|
||||
from calc
|
||||
transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b)))
|
||||
≈ g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b)))
|
||||
: ap_transport (sect f a) (λ a, g a⁻¹)
|
||||
... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b)))
|
||||
: ap (g a⁻¹) !transport_compose
|
||||
... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b)))
|
||||
: ap (λ x, g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (x⁻¹) (g a b)))) (adj f a)
|
||||
... ≈ g a⁻¹ (g a b) : transport_pV
|
||||
... ≈ b : sect (g a) b
|
||||
end
|
||||
-- -- "rewrite ap_transport"
|
||||
-- apply concat, apply inverse, apply (ap_transport (sect f a) (λ a, g a⁻¹)),
|
||||
-- apply concat, apply (ap (g a⁻¹)),
|
||||
-- -- "rewrite transport_compose"
|
||||
-- apply concat, apply transport_compose,
|
||||
-- -- "rewrite adj"
|
||||
-- -- "rewrite transport_pV"
|
||||
-- apply sect,
|
||||
|
||||
definition equiv_functor_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
|
||||
: (Σa, B a) ≃ (Σa', B' a') :=
|
||||
equiv.mk (functor f g) !is_equiv_functor
|
||||
|
||||
context --remove
|
||||
irreducible inv function.compose --remove
|
||||
definition equiv_functor (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
|
||||
(Σa, B a) ≃ (Σa', B' a') :=
|
||||
equiv_functor_of_is_equiv (to_fun Hf) (λ a, to_fun (Hg a))
|
||||
end --remove
|
||||
|
||||
definition equiv_functor_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a :=
|
||||
equiv_functor equiv.refl Hg
|
||||
|
||||
definition ap_functor_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b')
|
||||
: ap (sigma.functor f g) (sigma.path p q)
|
||||
≈ sigma.path (ap f p)
|
||||
(transport_compose _ f p (g a b)⁻¹ ⬝ ap_transport p g b⁻¹ ⬝ ap (g a') q) :=
|
||||
begin
|
||||
reverts (b', q),
|
||||
apply (path.rec_on p),
|
||||
intros (b', q), apply (path.rec_on q),
|
||||
apply idp
|
||||
end
|
||||
|
||||
definition ap_functor_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: ap (sigma.functor f g) (sigma.path p q)
|
||||
≈ sigma.path (ap f p)
|
||||
(transport_compose B' f p (g u.1 u.2)⁻¹ ⬝ ap_transport p g u.2⁻¹ ⬝ ap (g v.1) q) :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
apply (destruct u), intros (a, b),
|
||||
apply (destruct v), intros (a', b', p, q),
|
||||
apply ap_functor_sigma_dpair
|
||||
end
|
||||
|
||||
/- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
|
||||
open truncation
|
||||
definition is_equiv_dpr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)]
|
||||
: is_equiv (@dpr1 A B) :=
|
||||
adjointify dpr1
|
||||
(λa, ⟨a, !center⟩)
|
||||
(λa, idp)
|
||||
(λu, sigma.path idp !contr)
|
||||
|
||||
definition equiv_of_all_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
|
||||
equiv.mk dpr1 _
|
||||
|
||||
/- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/
|
||||
|
||||
definition equiv_center_of_contr (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A)
|
||||
:=
|
||||
equiv.mk _ (adjointify
|
||||
(λu, contr u.1⁻¹ ▹ u.2)
|
||||
(λb, ⟨!center, b⟩)
|
||||
(λb, ap (λx, x ▹ b) !path2_contr)
|
||||
(λu, sigma.path !contr !transport_pV))
|
||||
|
||||
/- Associativity -/
|
||||
|
||||
--this proof is harder than in Coq because we don't have eta definitionally for sigma
|
||||
protected definition assoc_equiv (C : (Σa, B a) → Type) : (Σa b, C ⟨a, b⟩) ≃ (Σu, C u) :=
|
||||
-- begin
|
||||
-- apply equiv.mk,
|
||||
-- apply (adjointify (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
|
||||
-- (λuc, ⟨uc.1.1, uc.1.2, !peta⁻¹ ▹ uc.2⟩)),
|
||||
-- intro uc, apply (destruct uc), intro u,
|
||||
-- apply (destruct u), intros (a, b, c),
|
||||
-- apply idp,
|
||||
-- intro av, apply (destruct av), intros (a, v),
|
||||
-- apply (destruct v), intros (b, c),
|
||||
-- apply idp,
|
||||
-- end
|
||||
equiv.mk _ (adjointify
|
||||
(λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
|
||||
(λuc, ⟨uc.1.1, uc.1.2, !peta⁻¹ ▹ uc.2⟩)
|
||||
proof (λuc, destruct uc (λu, destruct u (λa b c, idp))) qed
|
||||
proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
|
||||
|
||||
open prod
|
||||
definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
|
||||
equiv.mk _ (adjointify
|
||||
(λav, ⟨(av.1, av.2.1), av.2.2⟩)
|
||||
(λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !prod.peta⁻¹ ▹ uc.2⟩)
|
||||
proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed
|
||||
proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
|
||||
|
||||
/- Symmetry -/
|
||||
definition symm_equiv_uncurried (C : A × A' → Type) : (Σa a', C (a, a')) ≃ (Σa' a, C (a, a')) :=
|
||||
calc
|
||||
(Σa a', C (a, a')) ≃ Σu, C u : assoc_equiv_prod
|
||||
... ≃ Σv, C (flip v) : equiv_functor !prod.symm_equiv
|
||||
(λu, prod.destruct u (λa a', equiv.refl))
|
||||
... ≃ (Σa' a, C (a, a')) : assoc_equiv_prod
|
||||
|
||||
definition symm_equiv (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
|
||||
symm_equiv_uncurried (λu, C (pr1 u) (pr2 u))
|
||||
|
||||
definition equiv_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
|
||||
equiv.mk _ (adjointify
|
||||
(λs, (s.1, s.2))
|
||||
(λp, ⟨pr₁ p, pr₂ p⟩)
|
||||
proof (λp, prod.destruct p (λa b, idp)) qed
|
||||
proof (λs, destruct s (λa b, idp)) qed)
|
||||
|
||||
definition symm_equiv_deg (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
|
||||
calc
|
||||
(Σ(a : A), B) ≃ A × B : equiv_prod
|
||||
... ≃ B × A : prod.symm_equiv
|
||||
... ≃ Σ(b : B), A : equiv_prod
|
||||
|
||||
/- ** Universal mapping properties -/
|
||||
/- *** The positive universal property. -/
|
||||
|
||||
section
|
||||
open funext
|
||||
--in Coq this can be done without function extensionality
|
||||
definition is_equiv_sigma_rec [instance] [FUN : funext] (C : (Σa, B a) → Type)
|
||||
: 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)
|
||||
|
||||
definition equiv_sigma_rec [FUN : funext] (C : (Σa, B a) → Type)
|
||||
: (Π(a : A) (b: B a), C ⟨a, b⟩) ≃ (Πxy, C xy) :=
|
||||
equiv.mk sigma.rec _
|
||||
|
||||
/- *** The negative universal property. -/
|
||||
|
||||
definition coind_uncurried (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A) : Σ(b : B a), C a b
|
||||
:= ⟨fg.1 a, fg.2 a⟩
|
||||
|
||||
definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
|
||||
coind_uncurried ⟨f, g⟩ a
|
||||
|
||||
--is the instance below dangerous?
|
||||
--in Coq this can be done without function extensionality
|
||||
definition is_equiv_coind [instance] [FUN : funext] (C : Πa, B a → Type)
|
||||
: is_equiv (@coind_uncurried _ _ C) :=
|
||||
adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩)
|
||||
(λ h, proof path_pi (λu, !peta) qed)
|
||||
(λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed))
|
||||
|
||||
definition equiv_coind [FUN : funext] : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
|
||||
equiv.mk coind_uncurried _
|
||||
end
|
||||
|
||||
/- ** Subtypes (sigma types whose second components are hprops) -/
|
||||
|
||||
/- To prove equality in a subtype, we only need equality of the first component. -/
|
||||
definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 ≈ v.1 → u ≈ v :=
|
||||
(sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc))))
|
||||
|
||||
definition is_equiv_path_hprop [instance] [H : Πa, is_hprop (B a)] (u v : Σa, B a)
|
||||
: is_equiv (path_hprop u v) :=
|
||||
!is_equiv.compose
|
||||
|
||||
definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 ≈ v.1) ≃ (u ≈ v)
|
||||
:=
|
||||
equiv.mk !path_hprop _
|
||||
|
||||
/- truncatedness -/
|
||||
definition trunc_sigma [instance] (B : A → Type) (n : trunc_index)
|
||||
[HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) :=
|
||||
begin
|
||||
reverts (A, B, HA, HB),
|
||||
apply (trunc_index.rec_on n),
|
||||
intros (A, B, HA, HB),
|
||||
fapply trunc_equiv',
|
||||
apply equiv.symm,
|
||||
apply equiv_center_of_contr, apply HA, --should be solved by term synthesis
|
||||
apply HB,
|
||||
intros (n, IH, A, B, HA, HB),
|
||||
fapply is_trunc_succ, intros (u, v),
|
||||
fapply trunc_equiv',
|
||||
apply equiv_sigma_path,
|
||||
apply IH,
|
||||
apply succ_is_trunc, assumption,
|
||||
intro p,
|
||||
show is_trunc n (p ▹ u .2 ≈ v .2), from
|
||||
succ_is_trunc n (p ▹ u.2) (v.2),
|
||||
end
|
||||
|
||||
end sigma
|
||||
|
||||
open truncation sigma
|
||||
|
||||
namespace prod
|
||||
/- truncatedness -/
|
||||
definition trunc_prod [instance] (A B : Type) (n : trunc_index)
|
||||
[HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) :=
|
||||
trunc_equiv' n !equiv_prod
|
||||
end prod
|
||||
Loading…
Reference in a new issue