add pair.map-fst and pair.map-snd
This commit is contained in:
parent
a0f0d7ce7f
commit
3bec2477d9
|
@ -28,7 +28,7 @@ def curry :
|
|||
λ A B C f x y ⇒ f (x, y);
|
||||
|
||||
def curry' :
|
||||
0.(A B C : ★) → ((A × B) → C) → A → B → C =
|
||||
0.(A B C : ★) → (A × B → C) → A → B → C =
|
||||
λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
|
||||
|
||||
def0 fst-snd :
|
||||
|
@ -54,13 +54,19 @@ def map :
|
|||
0.(A A' : ★) →
|
||||
0.(B : A → ★) → 0.(B' : A' → ★) →
|
||||
(f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
|
||||
(Σ A B) → Σ A' B' =
|
||||
Σ A B → Σ A' B' =
|
||||
λ A A' B B' f g p ⇒
|
||||
case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
|
||||
|
||||
def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
|
||||
λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
|
||||
|
||||
def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
|
||||
λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x);
|
||||
|
||||
def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
|
||||
λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f;
|
||||
|
||||
}
|
||||
|
||||
def0 Σ = pair.Σ;
|
||||
|
|
Loading…
Reference in New Issue