nLab
partial function type
Redirected from "Laughlin wavefunctions".
Contents
Idea
In the same way that one could define equivalence types as types of one-to-one correspondences and function types as types of anafunctions , one could define partial function types as types of partial anafunctions .
Partial anafunctions are type families x : A , y : B ⊢ R ( x , y ) type x\colon A, y \colon B \vdash R(x, y) \; \mathrm{type} which comes with a family of witnesses
x : A ⊢ p ( x ) : isProp ( ∑ y : B R ( x , y ) ) x \colon A \vdash p(x) \colon \mathrm{isProp}\left(\sum_{y:B} R(x, y) \right)
that for each element x : A x\colon A , the dependent sum type ∑ y : B R ( x , y ) \sum_{y \colon B} R(x, y) is a mere proposition . From every partial anafunction, one could derive the partial function
x : A , p : ∑ y : B R ( x , y ) ⊢ f ( x , p ) : B x:A, p:\sum_{y:B} R(x, y) \vdash f(x, p):B
and for every mere proposition -valued type family x : A ⊢ P ( x ) x:A \vdash P(x) and every partial function x : A , p : P ( x ) , ⊢ f ( x , p ) : B x:A, p:P(x), \vdash f(x, p):B , one could define the partial anafunction x : A , y : B ⊢ R ( x , y ) x:A, y:B \vdash R(x, y) as
R ( x , y ) ≔ ∑ p : P ( x ) f ( x , p ) = B y R(x, y) \coloneqq \sum_{p:P(x)} f(x, p) =_B y
Defining partial function types requires both identity types and heterogeneous identity types being defined first, which we shall write as a = A b a =_A b and x = B p y x =_{B}^{p} y respectively for a : A a:A , b : A b:A , p : a = A b p:a =_A b , x : B ( a ) x:B(a) , and y : B ( b ) y:B(b) . We use the notation A ⇀ B A \rightharpoonup B to represent the type of partial functions between A A and B B .
Rules for partial function types
The rules for partial function types are as follows:
Γ ⊢ A type Γ ⊢ B type Γ ⊢ A ⇀ B type Γ ⊢ A type Γ ⊢ B type Γ , f : A ⇀ B , x : A , y : B ⊢ 𝒫 A , B ( f , x , y ) type \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \rightharpoonup B \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \rightharpoonup B, x:A, y:B \vdash \mathcal{P}_{A, B}(f, x, y) \; \mathrm{type}} Γ ⊢ A type Γ ⊢ B type Γ , x : A ⊢ P ( x ) type Γ , x : A , p : P ( x ) , q : P ( x ) ⊢ τ − 1 ( x , p , q ) : p = P ( x ) q Γ , x : A , p : P ( x ) ⊢ f ( x , p ) : B Γ ⊢ ( x , p ) ↦ f ( x , p ) : A ⇀ B \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{type} \quad \Gamma, x:A, p:P(x), q:P(x) \vdash \tau_{-1}(x, p, q):p =_{P(x)} q \quad \Gamma, x:A, p:P(x) \vdash f(x, p):B}{\Gamma \vdash (x, p) \mapsto f(x, p):A \rightharpoonup B} Γ ⊢ A type Γ ⊢ B type Γ , x : A ⊢ P ( x ) type Γ , x : A , p : P ( x ) , q : P ( x ) ⊢ τ − 1 ( x , p , q ) : p = P ( x ) q Γ , x : A , p : P ( x ) ⊢ f ( x , p ) : B Γ , x : A , p : P ( x ) ⊢ α ( x , p ) : 𝒫 A , B ( ( x , p ) ↦ f ( x , p ) , x , f ( x , p ) ) \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{type} \quad \Gamma, x:A, p:P(x), q:P(x) \vdash \tau_{-1}(x, p, q):p =_{P(x)} q \quad \Gamma, x:A, p:P(x) \vdash f(x, p):B}{\Gamma, x:A, p:P(x) \vdash \alpha(x, p):\mathcal{P}_{A, B}((x, p) \mapsto f(x, p), x, f(x, p))} Γ ⊢ A type Γ ⊢ B type Γ , x : A ⊢ P ( x ) type Γ , x : A , p : P ( x ) , q : P ( x ) ⊢ τ − 1 ( x , p , q ) : p = P ( x ) q Γ , f : A ⇀ B , x : A , p : P ( x ) ⊢ ev ( f , x , p ) : B \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{type} \quad \Gamma, x:A, p:P(x), q:P(x) \vdash \tau_{-1}(x, p, q):p =_{P(x)} q}{\Gamma, f:A \rightharpoonup B, x:A, p:P(x) \vdash \mathrm{ev}(f, x, p):B} Γ ⊢ A type Γ ⊢ B type Γ , x : A ⊢ P ( x ) type Γ , x : A , p : P ( x ) , q : P ( x ) ⊢ τ − 1 ( x , p , q ) : p = P ( x ) q Γ , f : A ⇀ B , x : A , p : P ( x ) ⊢ β ( f , x , p ) : ℱ A , B ( f , x , ev ( f , x , p ) ) \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{type} \quad \Gamma, x:A, p:P(x), q:P(x) \vdash \tau_{-1}(x, p, q):p =_{P(x)} q}{\Gamma, f:A \rightharpoonup B, x:A, p:P(x) \vdash \beta(f, x, p):\mathcal{F}_{A, B}(f, x, \mathrm{ev}(f, x, p))} Γ ⊢ A type Γ ⊢ B type Γ , f : A ⇀ B , x : A , y : B , u : 𝒫 A , B ( f , x , y ) , z : B , v : 𝒫 A , B ( f , x , z ) ⊢ κ ( f , x , y , u , z , v ) : y = B z \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \rightharpoonup B, x:A, y:B, u:\mathcal{P}_{A, B}(f, x, y), z:B, v:\mathcal{P}_{A, B}(f, x, z) \vdash \kappa(f, x, y, u, z, v):y =_B z} Γ ⊢ A type Γ ⊢ B type Γ , f : A ⇀ B , x : A , y : B , u : 𝒫 A , B ( f , x , y ) , z : B , v : 𝒫 A , B ( f , x , z ) ⊢ η ( f , x , y , u , z , v ) : u = 𝒫 A , B ( f , x ) κ ( f , x , y , u , z , v ) v \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \rightharpoonup B, x:A, y:B, u:\mathcal{P}_{A, B}(f, x, y), z:B, v:\mathcal{P}_{A, B}(f, x, z) \vdash \eta(f, x, y, u, z, v):u =_{\mathcal{P}_{A, B}(f, x)}^{\kappa(f, x, y, u, z, v)} v}
By the rules for dependent sum types and dependent product types , one could derive that
Γ ⊢ A type Γ ⊢ B type Γ , f : A ⇀ B ⊢ η ( f ) : ∏ x : A isProp ( ∑ y : B 𝒫 A , B ( f , x , y ) ) \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \rightharpoonup B \vdash \eta(f):\prod_{x:A} \mathrm{isProp}\left(\sum_{y:B} \mathcal{P}_{A, B}(f, x, y) \right)}
which is precisely the statement that 𝒫 A , B ( f ) \mathcal{P}_{A, B}(f) is a partial anafunction for all partial functions f : A ⇀ B f:A \rightharpoonup B .
See also
Last revised on January 6, 2023 at 01:33:07.
See the history of this page for a list of all contributions to it.