Skip to content

Commit 25d3274

Browse files
5HT5HT
committed
move to new /library/ structure
1 parent 61a2427 commit 25d3274

51 files changed

Lines changed: 165 additions & 178 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎library/book.anders‎

Lines changed: 44 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,45 @@
11
module book where
2-
import lib/foundations/mltt/pi
3-
import lib/foundations/mltt/sigma
4-
import lib/foundations/mltt/inductive
5-
import lib/foundations/mltt/bool
6-
import lib/foundations/mltt/either
7-
import lib/foundations/mltt/maybe
8-
import lib/foundations/mltt/nat
9-
import lib/foundations/mltt/list
10-
import lib/foundations/mltt/fin
11-
import lib/foundations/mltt/vec
12-
import lib/foundations/univalent/path
13-
import lib/foundations/univalent/prop
14-
import lib/foundations/univalent/extensionality
15-
import lib/foundations/univalent/equiv
16-
import lib/foundations/univalent/iso
17-
import lib/foundations/modal/infinitesimal
18-
import lib/mathematics/algebra/algebra
19-
import lib/mathematics/analysis/real
20-
import lib/mathematics/analysis/topology
21-
import lib/mathematics/geometry/bundle
22-
import lib/mathematics/geometry/etale
23-
import lib/mathematics/geometry/formalDisc
24-
import lib/mathematics/homotopy/coequalizer
25-
import lib/mathematics/homotopy/constcubes
26-
import lib/mathematics/homotopy/pullback
27-
import lib/mathematics/homotopy/pushout
28-
import lib/mathematics/homotopy/hubSpokes
29-
import lib/mathematics/homotopy/quotient
30-
import lib/mathematics/homotopy/truncation
31-
import lib/mathematics/homotopy/suspension
32-
import lib/mathematics/homotopy/loop
33-
import lib/mathematics/homotopy/S1
34-
import lib/mathematics/homotopy/Sn
35-
import lib/mathematics/homotopy/KGn
36-
import lib/mathematics/categories/category
37-
import lib/mathematics/categories/cartesian
38-
import lib/mathematics/categories/functor
39-
import lib/mathematics/categories/natural
40-
import lib/mathematics/categories/abelian
41-
import lib/mathematics/categories/groupoid
42-
import lib/mathematics/categories/topos
43-
import lib/mathematics/categories/meta/favonia
44-
import lib/mathematics/categories/meta/kraus
45-
import lib/mathematics/categories/meta/awodey
2+
import library/foundations/mltt/pi
3+
import library/foundations/mltt/sigma
4+
import library/foundations/mltt/inductive
5+
import library/foundations/mltt/bool
6+
import library/foundations/mltt/either
7+
import library/foundations/mltt/maybe
8+
import library/foundations/mltt/nat
9+
import library/foundations/mltt/list
10+
import library/foundations/mltt/fin
11+
import library/foundations/mltt/vec
12+
import library/foundations/univalent/path
13+
import library/foundations/univalent/prop
14+
import library/foundations/univalent/extensionality
15+
import library/foundations/univalent/equiv
16+
import library/foundations/univalent/iso
17+
import library/foundations/modal/infinitesimal
18+
import library/mathematics/algebra/algebra
19+
import library/mathematics/analysis/real
20+
import library/mathematics/analysis/topology
21+
import library/mathematics/geometry/bundle
22+
import library/mathematics/geometry/etale
23+
import library/mathematics/geometry/formalDisc
24+
import library/mathematics/homotopy/coequalizer
25+
import library/mathematics/homotopy/constcubes
26+
import library/mathematics/homotopy/pullback
27+
import library/mathematics/homotopy/pushout
28+
import library/mathematics/homotopy/hubSpokes
29+
import library/mathematics/homotopy/quotient
30+
import library/mathematics/homotopy/truncation
31+
import library/mathematics/homotopy/suspension
32+
import library/mathematics/homotopy/loop
33+
import library/mathematics/homotopy/S1
34+
import library/mathematics/homotopy/Sn
35+
import library/mathematics/homotopy/KGn
36+
import library/mathematics/categories/category
37+
import library/mathematics/categories/cartesian
38+
import library/mathematics/categories/functor
39+
import library/mathematics/categories/natural
40+
import library/mathematics/categories/abelian
41+
import library/mathematics/categories/groupoid
42+
import library/mathematics/categories/topos
43+
import library/mathematics/categories/meta/favonia
44+
import library/mathematics/categories/meta/kraus
45+
import library/mathematics/categories/meta/awodey

‎library/foundations/logic/glivenko.anders‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66
Copyright (c) Groupoid Infinity, 2014-2022. -}
77

88
module glivenko where
9-
import lib/foundations/mltt/proto
10-
import lib/foundations/mltt/either
9+
import library/foundations/mltt/proto
10+
import library/foundations/mltt/either
1111

1212
def CL (A : U) := ¬ (¬ A)
1313
def IPC→CL (A : U) : A → CL A := λ (x : A) (φ : ¬ A), φ x

‎library/foundations/logic/hilbert.anders‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66
Copyright (c) Groupoid Infinity, 2014-2022. -}
77

88
module hilbert where
9-
import lib/foundations/univalent/path
10-
import lib/foundations/mltt/proto
9+
import library/foundations/univalent/path
10+
import library/foundations/mltt/proto
1111

1212
-- [Schönfinkel] Ukraine, Dnipro
1313

‎library/foundations/mltt/bool.anders‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
module bool where
2-
import lib/foundations/univalent/path
3-
import lib/foundations/mltt/either
4-
import lib/foundations/mltt/proto
2+
import library/foundations/univalent/path
3+
import library/foundations/mltt/either
4+
import library/foundations/mltt/proto
55

66
--- data 𝟐 : U := 0₂ | 1₂
77
def rec₂ (A : U) (a b : A) : 𝟐 → A := ind₂ (λ (_ : 𝟐), A) a b

‎library/foundations/mltt/fin.anders‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66
Copyright (c) Groupoid Infinity, 2014-2023. -}
77

88
module fin where
9-
import lib/foundations/mltt/either
10-
import lib/foundations/mltt/nat
9+
import library/foundations/mltt/either
10+
import library/foundations/mltt/nat
1111

1212
def Fin : ℕ -> U := ℕ-iter U 𝟎 (+ 𝟏)
1313
def fzero (n : ℕ) : Fin (succ n) := (0₂, ★)

‎library/foundations/mltt/inductive.anders‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@
1111
Copyright (c) Groupoid Infinity, 2014-2023. -}
1212

1313
module inductive where
14-
import lib/foundations/univalent/path
15-
import lib/foundations/mltt/either
14+
import library/foundations/univalent/path
15+
import library/foundations/mltt/either
1616
option irrelevance true
1717

1818
-- Steve Awodey, Nicola Gambino, Kristina Sojakova

‎library/foundations/mltt/lambda.anders‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module lambda where
22

3-
import lib/foundations/mltt/either
3+
import library/foundations/mltt/either
44

55
def Tag : U := 𝟓
66
def VAR : Tag := 0₅

‎library/foundations/mltt/list.anders‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66
Copyright (c) Groupoid Infinity, 2014-2022. -}
77

88
module list where
9-
import lib/foundations/mltt/maybe
10-
import lib/foundations/mltt/nat
9+
import library/foundations/mltt/maybe
10+
import library/foundations/mltt/nat
1111
option girard true
1212

1313
-- def L-ctor (A : U) : U := W (x : Maybe A), maybe-rec A U 𝟎 (λ (a : A), 𝟏) x

‎library/foundations/mltt/maybe.anders‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
module maybe where
2-
import lib/foundations/mltt/either
2+
import library/foundations/mltt/either
33

44
def Maybe (A : U) : U := + 𝟏 A
55
def nothing (A : U) : Maybe A := (0₂, ★)

‎library/foundations/mltt/mltt.anders‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -14,39 +14,39 @@ option girard true
1414

1515
-- built-ins
1616

17-
def Path (A : U) (x y : A) : U := PathP (<_> A) x y
18-
def idp (A : U) (x : A) : Path A x x := <_> x
17+
def Path' (A : U) (x y : A) : U := PathP (<_> A) x y
18+
def idp (A : U) (x : A) : Path' A x x := <_> x
1919
def Pi (O : 𝟏) (A : U) (B : A → U) : U := Π (x : A), B x
2020
def Π-lambda (O : 𝟏) (A: U) (B: A → U) (b: Pi ★ A B) : Pi ★ A B := λ (x : A), b x
2121
def Π-apply (O : 𝟏) (A: U) (B: A → U) (f: Pi ★ A B) (a: A) : B a := f a
22-
def Π-β (O : 𝟏) (A : U) (B : A → U) (a : A) (f : Pi ★ A B) : Path (B a) (Π-apply ★ A B (Π-lambda ★ A B f) a) (f a) := idp (B a) (f a)
23-
def Π-η (O : 𝟏) (A : U) (B : A → U) (a : A) (f : Pi ★ A B) : Path (Pi ★ A B) f (λ (x : A), f x) := idp (Pi ★ A B) f
22+
def Π-β (O : 𝟏) (A : U) (B : A → U) (a : A) (f : Pi ★ A B) : Path' (B a) (Π-apply ★ A B (Π-lambda ★ A B f) a) (f a) := idp (B a) (f a)
23+
def Π-η (O : 𝟏) (A : U) (B : A → U) (a : A) (f : Pi ★ A B) : Path' (Pi ★ A B) f (λ (x : A), f x) := idp (Pi ★ A B) f
2424
def Sigma (O : 𝟏) (A : U) (B : A → U) : U := summa (x: A), B x
2525
def pair (O : 𝟏) (A: U) (B: A → U) (a: A) (b: B a) : Sigma ★ A B := (a, b)
2626
def pr₁ (O : 𝟏) (A: U) (B: A → U) (x: Sigma ★ A B) : A := x.1
2727
def pr₂ (O : 𝟏) (A: U) (B: A → U) (x: Sigma ★ A B) : B (pr₁ ★ A B x) := x.2
28-
def Σ-β₁ (O : 𝟏) (A : U) (B : A → U) (a : A) (b : B a) : Path A a (pr₁ ★ A B (a ,b)) := idp A a
29-
def Σ-β₂ (O : 𝟏) (A : U) (B : A → U) (a : A) (b : B a) : Path (B a) b (pr₂ ★ A B (a, b)) := idp (B a) b
30-
def Σ-η (O : 𝟏) (A : U) (B : A → U) (p : Sigma ★ A B) : Path (Sigma ★ A B) p (pr₁ ★ A B p, pr₂ ★ A B p) := idp (Sigma ★ A B) p
28+
def Σ-β₁ (O : 𝟏) (A : U) (B : A → U) (a : A) (b : B a) : Path' A a (pr₁ ★ A B (a ,b)) := idp A a
29+
def Σ-β₂ (O : 𝟏) (A : U) (B : A → U) (a : A) (b : B a) : Path' (B a) b (pr₂ ★ A B (a, b)) := idp (B a) b
30+
def Σ-η (O : 𝟏) (A : U) (B : A → U) (p : Sigma ★ A B) : Path' (Sigma ★ A B) p (pr₁ ★ A B p, pr₂ ★ A B p) := idp (Sigma ★ A B) p
3131

32-
def Path-1 (O : 𝟏) (A : U) (x y : A) : U := PathP (<_> A) x y
33-
def idp-1 (O : 𝟏) (A : U) (x : A) : Path A x x := <_> x
32+
def Path'-1 (O : 𝟏) (A : U) (x y : A) : U := PathP (<_> A) x y
33+
def idp-1 (O : 𝟏) (A : U) (x : A) : Path' A x x := <_> x
3434
def transport (A B: U) (p : PathP (<_> U) A B) (a: A): B := transp p 0 a
35-
def singl (A: U) (a: A): U := Σ (x: A), Path A a x
35+
def singl (A: U) (a: A): U := Σ (x: A), Path' A a x
3636
def eta (A: U) (a: A): singl A a := (a, idp A a)
37-
def contr (A : U) (a b : A) (p : Path A a b) : Path (singl A a) (eta A a) (b, p) := <i> (p @ i, <j> p @ i /\ j)
38-
def trans_comp (A : U) (a : A) : Path A a (transport A A (<i> A) a) := <j> transp (<_> A) -j a
39-
def subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b := transp (<i> P (p @ i)) 0 e
40-
def subst-comp (A: U) (P: A → U) (a: A) (e: P a): Path (P a) e (subst A P a a (idp A a) e) := trans_comp (P a) e
41-
def D (A : U) : U₁ := Π (x y : A), Path A x y → U
37+
def contr (A : U) (a b : A) (p : Path' A a b) : Path' (singl A a) (eta A a) (b, p) := <i> (p @ i, <j> p @ i /\ j)
38+
def trans_comp (A : U) (a : A) : Path' A a (transport A A (<i> A) a) := <j> transp (<_> A) -j a
39+
def subst (A : U) (P : A -> U) (a b : A) (p : Path' A a b) (e : P a) : P b := transp (<i> P (p @ i)) 0 e
40+
def subst-comp (A: U) (P: A → U) (a: A) (e: P a): Path' (P a) e (subst A P a a (idp A a) e) := trans_comp (P a) e
41+
def D (A : U) : U₁ := Π (x y : A), Path' A x y → U
4242

4343
-- constructive J-β
4444

45-
def J (A: U) (x: A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path A x y): C x y p
45+
def J (A: U) (x: A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path' A x y): C x y p
4646
:= subst (singl A x) (\ (z: singl A x), C x (z.1) (z.2)) (eta A x) (y, p) (contr A x y p) d
47-
def J-1 (O : 𝟏) (A : U) (x : A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path A x y): C x y p
47+
def J-1 (O : 𝟏) (A : U) (x : A) (C: D A) (d: C x x (idp A x)) (y: A) (p: Path' A x y): C x y p
4848
:= subst (singl A x) (\ (z: singl A x), C x (z.1) (z.2)) (eta A x) (y, p) (contr A x y p) d
49-
def J-β (O : 𝟏) (A : U) (a : A) (C : D A) (d: C a a (idp A a)) : Path (C a a (idp A a)) d (J A a C d a (idp A a))
49+
def J-β (O : 𝟏) (A : U) (a : A) (C : D A) (d: C a a (idp A a)) : Path' (C a a (idp A a)) d (J A a C d a (idp A a))
5050
:= subst-comp (singl A a) (\ (z: singl A a), C a (z.1) (z.2)) (eta A a) d
5151

5252

@@ -56,24 +56,24 @@ def MLTT-73 :=
5656
Σ (Π-form : Π (A : U) (B : A → U), U)
5757
(Π-ctor₁ : Π (A : U) (B : A → U), Pi ★ A B → Pi ★ A B)
5858
(Π-elim₁ : Π (A : U) (B : A → U), Pi ★ A B → Pi ★ A B)
59-
(Π-comp₁ : Π (A : U) (B : A → U) (a : A) (f : Pi ★ A B), Path (B a) (Π-elim₁ A B (Π-ctor₁ A B f) a) (f a))
60-
(Π-comp₂ : Π (A : U) (B : A → U) (a : A) (f : Pi ★ A B), Path (Pi ★ A B) f (λ (x : A), f x))
59+
(Π-comp₁ : Π (A : U) (B : A → U) (a : A) (f : Pi ★ A B), Path' (B a) (Π-elim₁ A B (Π-ctor₁ A B f) a) (f a))
60+
(Π-comp₂ : Π (A : U) (B : A → U) (a : A) (f : Pi ★ A B), Path' (Pi ★ A B) f (λ (x : A), f x))
6161
(Σ-form : Π (A : U) (B : A → U), U)
6262
(Σ-ctor₁ : Π (A : U) (B : A → U) (a : A) (b : B a) , Sigma ★ A B)
6363
(Σ-elim₁ : Π (A : U) (B : A → U) (p : Sigma ★ A B), A)
6464
(Σ-elim₂ : Π (A : U) (B : A → U) (p : Sigma ★ A B), B (pr₁ ★ A B p))
65-
(Σ-comp₁ : Π (A : U) (B : A → U) (a : A) (b: B a), Path A a (Σ-elim₁ A B (Σ-ctor₁ A B a b)))
66-
(Σ-comp₂ : Π (A : U) (B : A → U) (a : A) (b: B a), Path (B a) b (Σ-elim₂ A B (a, b)))
67-
(Σ-comp₃ : Π (A : U) (B : A → U) (p : Sigma ★ A B), Path (Sigma ★ A B) p (pr₁ ★ A B p, pr₂ ★ A B p))
65+
(Σ-comp₁ : Π (A : U) (B : A → U) (a : A) (b: B a), Path' A a (Σ-elim₁ A B (Σ-ctor₁ A B a b)))
66+
(Σ-comp₂ : Π (A : U) (B : A → U) (a : A) (b: B a), Path' (B a) b (Σ-elim₂ A B (a, b)))
67+
(Σ-comp₃ : Π (A : U) (B : A → U) (p : Sigma ★ A B), Path' (Sigma ★ A B) p (pr₁ ★ A B p, pr₂ ★ A B p))
6868
(=-form : Π (A : U) (a : A), A → U)
69-
(=-ctor₁ : Π (A : U) (a : A), Path A a a)
70-
(=-elim₁ : Π (A : U) (a : A) (C: D A) (d: C a a (=-ctor₁ A a)) (y: A) (p: Path A a y), C a y p)
71-
(=-comp₁ : Π (A : U) (a : A) (C: D A) (d: C a a (=-ctor₁ A a)), Path (C a a (=-ctor₁ A a)) d (=-elim₁ A a C d a (=-ctor₁ A a))), 𝟏
69+
(=-ctor₁ : Π (A : U) (a : A), Path' A a a)
70+
(=-elim₁ : Π (A : U) (a : A) (C: D A) (d: C a a (=-ctor₁ A a)) (y: A) (p: Path' A a y), C a y p)
71+
(=-comp₁ : Π (A : U) (a : A) (C: D A) (d: C a a (=-ctor₁ A a)), Path' (C a a (=-ctor₁ A a)) d (=-elim₁ A a C d a (=-ctor₁ A a))), 𝟏
7272

7373
--- Theorem. J-β-rule is derivable from generalized transport
7474

7575
def internalizing : MLTT-73
7676
:= ( Pi ★, Π-lambda ★, Π-apply ★, Π-β ★, Π-η ★,
7777
Sigma ★, pair ★, pr₁ ★, pr₂ ★, Σ-β₁ ★, Σ-β₂ ★, Σ-η ★,
78-
Path-1 ★, idp-1 ★, J-1 ★, J-β ★, ★
78+
Path'-1 ★, idp-1 ★, J-1 ★, J-β ★, ★
7979
)

0 commit comments

Comments
 (0)