-
Notifications
You must be signed in to change notification settings - Fork 1
/
Pushout.lean
69 lines (52 loc) · 2.1 KB
/
Pushout.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
import GroundZero.HITs.Quotient
open GroundZero.Types.Id (ap)
open GroundZero.Types.Equiv
open GroundZero.Types
/-
Pushout.
* HoTT 6.8
-/
namespace GroundZero
namespace HITs
universe u v w k
section
variable {A : Type u} {B : Type v} {C : Type k} (f : C → A) (g : C → B)
inductive Pushout.rel : Sum A B → Sum A B → Type k
| mk : Π (x : C), rel (Sum.inl (f x)) (Sum.inr (g x))
hott definition Pushout := Quotient (Pushout.rel f g)
end
namespace Pushout
-- https://github.com/leanprover/lean2/blob/master/hott/hit/Pushout.hlean
variable {A : Type u} {B : Type v} {C : Type k} {f : C → A} {g : C → B}
hott definition inl (x : A) : Pushout f g :=
Quotient.elem (Sum.inl x)
hott definition inr (x : B) : Pushout f g :=
Quotient.elem (Sum.inr x)
hott definition glue (x : C) : @inl _ _ _ f g (f x) = inr (g x) :=
Quotient.line (Pushout.rel.mk x)
hott definition ind {P : Pushout f g → Type w} (inlπ : Π x, P (inl x)) (inrπ : Π x, P (inr x))
(glueπ : Π x, inlπ (f x) =[glue x] inrπ (g x)) : Π x, P x :=
begin
fapply Quotient.ind; { intro x; induction x using Sum.casesOn; apply inlπ; apply inrπ };
{ intros u v H; induction H using rel.casesOn; apply glueπ }
end
attribute [induction_eliminator] ind
hott definition rec {D : Type w} (inlπ : A → D) (inrπ : B → D)
(glueπ : Π x, inlπ (f x) = inrπ (g x)) : Pushout f g → D :=
ind inlπ inrπ (λ x, pathoverOfEq (glue x) (glueπ x))
hott definition indβrule {P : Pushout f g → Type w}
(inlπ : Π x, P (inl x)) (inrπ : Π x, P (inr x))
(glueπ : Π x, inlπ (f x) =[glue x] inrπ (g x)) (x : C) :
apd (ind inlπ inrπ glueπ) (glue x) = glueπ x :=
@Quotient.indβrule _ (rel f g) _ _ _ _ _ (rel.mk x)
hott definition recβrule {D : Type w} (inlπ : A → D) (inrπ : B → D)
(glueπ : Π x, inlπ (f x) = inrπ (g x)) (x : C) :
ap (rec inlπ inrπ glueπ) (glue x) = glueπ x :=
begin
apply pathoverOfEqInj (glue x); transitivity;
symmetry; apply apdOverConstantFamily;
transitivity; apply indβrule; reflexivity
end
end Pushout
end HITs
end GroundZero