Lifts and drops

Lax149335.LiftsAndDrops · concepts/Lax149335/LiftsAndDrops.lean · lax-149335

definition

Loading review…

Natural Language Statement

Definition

Definition 7.1 (Lifts and drops). Lift terms (respectively, drop terms) are those which can be obtained from the atomic lift (respectively, atomic drop) terms in Table 1 by applying composition, as well as the functoriality combinators for co-products, products and lists.

Table 1. The atomic lift terms are

\begin{gathered} A \xrightarrow{\mathrm{id}} A \qquad A + B \xrightarrow{\mathsf{comm}} B + A \qquad A \to A \times 1 \qquad A \to 1 \times A \\ A \times (B \times C) \xrightarrow{\mathsf{assocL}} (A \times B) \times C \qquad (A \times B) \times C \xrightarrow{\mathsf{assocR}} A \times (B \times C) \\ A + (B + C) \to (A + B) + C \qquad (A + B) + C \to A + (B + C) \\ (A + B) \times C \xrightarrow{\mathsf{distL}} A \times C + B \times C \qquad A \times (B + C) \xrightarrow{\mathsf{distR}} A \times B + A \times C \\ (A + B)^* \xrightarrow{\mathsf{split}} A^* \times (B \times A^*)^* \qquad (A \times B)^* \xrightarrow{\mathsf{shift}} 1 + A \times (B \times A)^* \times B \end{gathered}

and the atomic drop terms are

\begin{gathered} A \xrightarrow{\mathrm{id}} A \qquad A \xrightarrow{1 \,;\, v} B \qquad A \times B \xrightarrow{\mathsf{fst}} A \qquad A \times B \xrightarrow{\mathsf{snd}} B \qquad A \xrightarrow{\mathsf{Left}} A + B \qquad B \xrightarrow{\mathsf{Right}} A + B \\ \mathsf{assocL} \qquad \mathsf{assocR} \qquad A + A \xrightarrow{\mathsf{codiag}} A \qquad A \xrightarrow{\mathsf{pure}} A^* \qquad A^{**} \xrightarrow{\mathsf{concat}} A^* \qquad A^* \times A^* \xrightarrow{\mathsf{binconcat}} A^* \\ A \times (B \times A)^* \times B \xrightarrow{\mathsf{unshift}} (A \times B)^* \end{gathered}

where $1 \,;\, v$ is the unique term $A \to 1$ followed by an arbitrary value $v : 1 \to B$ .

Concept map

4 concepts; 4 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax149335.DerivedTerms
2
3	/-!
4	---
5	title: Lifts and drops
6	type: definition
7	---
8	Definition 7.1 (Lifts and drops). Lift terms (respectively, drop terms) are those
9	which can be obtained from the atomic lift (respectively, atomic drop) terms in Table 1 by
10	applying composition, as well as the functoriality combinators for co-products, products and
11	lists.
12
13	Table 1. The atomic lift terms are
14
15	$\begin{gathered} A \xrightarrow{\mathrm{id}} A \qquad A + B \xrightarrow{\mathsf{comm}} B + A \qquad A \to A \times 1 \qquad A \to 1 \times A \\ A \times (B \times C) \xrightarrow{\mathsf{assocL}} (A \times B) \times C \qquad (A \times B) \times C \xrightarrow{\mathsf{assocR}} A \times (B \times C) \\ A + (B + C) \to (A + B) + C \qquad (A + B) + C \to A + (B + C) \\ (A + B) \times C \xrightarrow{\mathsf{distL}} A \times C + B \times C \qquad A \times (B + C) \xrightarrow{\mathsf{distR}} A \times B + A \times C \\ (A + B)^* \xrightarrow{\mathsf{split}} A^* \times (B \times A^)^ \qquad (A \times B)^* \xrightarrow{\mathsf{shift}} 1 + A \times (B \times A)^* \times B \end{gathered}$
16
17
18
19
20
21
22
23
24
25
26
27	and the atomic drop terms are
28
29	$\begin{gathered} A \xrightarrow{\mathrm{id}} A \qquad A \xrightarrow{1 \,;\, v} B \qquad A \times B \xrightarrow{\mathsf{fst}} A \qquad A \times B \xrightarrow{\mathsf{snd}} B \qquad A \xrightarrow{\mathsf{Left}} A + B \qquad B \xrightarrow{\mathsf{Right}} A + B \\ \mathsf{assocL} \qquad \mathsf{assocR} \qquad A + A \xrightarrow{\mathsf{codiag}} A \qquad A \xrightarrow{\mathsf{pure}} A^* \qquad A^{*} \xrightarrow{\mathsf{concat}} A^ \qquad A^* \times A^* \xrightarrow{\mathsf{binconcat}} A^* \\ A \times (B \times A)^* \times B \xrightarrow{\mathsf{unshift}} (A \times B)^* \end{gathered}$
30
31
32
33
34
35
36
37
38
39	where $1 \,;\, v$ is the unique term $A \to 1$ followed by an arbitrary value
40	$v : 1 \to B$ .
41	-/
42
43	namespace Lax149335.LiftsAndDrops
44
45	open Lax149335.Types Lax149335.Terms Lax149335.DerivedTerms Lax149335.DerivedTerms.Term
46
47	/-- Definition 7.1 (Lifts). The terms obtained from the atomic lift terms of Table 1 by
48	composition and the functoriality combinators of products, co-products and lists. -/
49	inductive IsLift : {A B : Ty} → Term A B → Prop
50	/-- Lifts are closed under composition. -/
51	\| comp {A B C : Ty} {f : Term A B} {g : Term B C} : IsLift f → IsLift g → IsLift (f ⨟ g)
52	/-- Lifts are closed under functoriality of products. -/
53	\| prodF {A₁ A₂ B₁ B₂ : Ty} {f : Term A₁ B₁} {g : Term A₂ B₂} :
54	IsLift f → IsLift g → IsLift (Term.prodF f g)
55	/-- Lifts are closed under functoriality of co-products. -/
56	\| sumF {A₁ A₂ B₁ B₂ : Ty} {f : Term A₁ B₁} {g : Term A₂ B₂} :
57	IsLift f → IsLift g → IsLift (Term.sumF f g)
58	/-- Lifts are closed under functoriality of lists. -/
59	\| listF {A B : Ty} {f : Term A B} : IsLift f → IsLift (Term.listF f)
60	/-- The identity is a prime lift. -/
61	\| id (A : Ty) : IsLift (Term.id A)
62	/-- `(id,1)` is a prime lift. -/
63	\| unitR (A : Ty) : IsLift (Term.unitR A)
64	/-- `(1,id)` is a prime lift. -/
65	\| unitL (A : Ty) : IsLift (Term.unitL A)
66	/-- `assocL` is a prime lift. -/
67	\| assocL (A B C : Ty) : IsLift (Term.assocL A B C)
68	/-- `assocR` is a prime lift. -/
69	\| assocR (A B C : Ty) : IsLift (Term.assocR A B C)
70	/-- Associativity of the co-product, from right to left, is a prime lift. -/
71	\| sumAssocL (A B C : Ty) : IsLift (Term.sumAssocL A B C)
72	/-- Associativity of the co-product, from left to right, is a prime lift. -/
73	\| sumAssocR (A B C : Ty) : IsLift (Term.sumAssocR A B C)
74	/-- Commutativity of the co-product is a prime lift. -/
75	\| comm (A B : Ty) : IsLift (Term.comm A B)
76	/-- `distL` is a prime lift. -/
77	\| distL (A B C : Ty) : IsLift (Term.distL A B C)
78	/-- `distR` is a prime lift. -/
79	\| distR (A B C : Ty) : IsLift (Term.distR A B C)
80	/-- `split` is a prime lift. -/
81	\| split (A B : Ty) : IsLift (Term.split A B)
82	/-- `shift` is a prime lift. -/
83	\| shift (A B : Ty) : IsLift (Term.shift A B)
84
85	/-- Definition 7.1 (Drops). The terms obtained from the atomic drop terms of Table 1 by
86	composition and the functoriality combinators of products, co-products and lists. -/
87	inductive IsDrop : {A B : Ty} → Term A B → Prop
88	/-- Drops are closed under composition. -/
89	\| comp {A B C : Ty} {f : Term A B} {g : Term B C} : IsDrop f → IsDrop g → IsDrop (f ⨟ g)
90	/-- Drops are closed under functoriality of products. -/
91	\| prodF {A₁ A₂ B₁ B₂ : Ty} {f : Term A₁ B₁} {g : Term A₂ B₂} :
92	IsDrop f → IsDrop g → IsDrop (Term.prodF f g)
93	/-- Drops are closed under functoriality of co-products. -/
94	\| sumF {A₁ A₂ B₁ B₂ : Ty} {f : Term A₁ B₁} {g : Term A₂ B₂} :
95	IsDrop f → IsDrop g → IsDrop (Term.sumF f g)
96	/-- Drops are closed under functoriality of lists. -/
97	\| listF {A B : Ty} {f : Term A B} : IsDrop f → IsDrop (Term.listF f)
98	/-- The identity is a prime drop. -/
99	\| id (A : Ty) : IsDrop (Term.id A)
100	/-- A constant function `1 ; v`, for an arbitrary value `v`, is a prime drop. -/
101	\| bangV (A : Ty) {B : Ty} (v : Value B) : IsDrop (Term.toUnit A ⨟ v)
102	/-- `assocL` is a prime drop. -/
103	\| assocL (A B C : Ty) : IsDrop (Term.assocL A B C)
104	/-- `assocR` is a prime drop. -/
105	\| assocR (A B C : Ty) : IsDrop (Term.assocR A B C)
106	/-- `fst` is a prime drop. -/
107	\| fst (A B : Ty) : IsDrop (Term.fst A B)
108	/-- `snd` is a prime drop. -/
109	\| snd (A B : Ty) : IsDrop (Term.snd A B)
110	/-- `Left` is a prime drop. -/
111	\| inl (A B : Ty) : IsDrop (Term.inl A B)
112	/-- `Right` is a prime drop. -/
113	\| inr (A B : Ty) : IsDrop (Term.inr A B)
114	/-- The co-diagonal is a prime drop. -/
115	\| codiag (A : Ty) : IsDrop (Term.codiag A)
116	/-- `pure` is a prime drop. -/
117	\| pureT (A : Ty) : IsDrop (Term.pureT A)
118	/-- `binconcat` is a prime drop. -/
119	\| binconcat (A : Ty) : IsDrop (Term.binconcat A)
120	/-- `concat` is a prime drop. -/
121	\| concat (A : Ty) : IsDrop (Term.concat A)
122	/-- `unshift` is a prime drop. -/
123	\| unshift (A B : Ty) : IsDrop (Term.unshift A B)
124
125	end Lax149335.LiftsAndDrops
126

Builds on

Lax149335.DerivedTerms

Used by

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Lifts and drops

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments