exercises
This commit is contained in:
parent
4e2c2962e6
commit
e475a6c685
2 changed files with 12 additions and 7 deletions
|
@ -139,11 +139,11 @@ module _ {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} where
|
||||||
|
|
||||||
ΣPathP : Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
|
ΣPathP : Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
|
||||||
→ x ≡ y
|
→ x ≡ y
|
||||||
ΣPathP = {!!}
|
ΣPathP (fst , snd) i = fst i , snd i
|
||||||
|
|
||||||
PathPΣ : x ≡ y
|
PathPΣ : x ≡ y
|
||||||
→ Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
|
→ Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
|
||||||
PathPΣ = {!!}
|
PathPΣ p = (λ i → Σ.fst (p i)) , (λ i → Σ.snd (p i))
|
||||||
|
|
||||||
ΣPathP-PathPΣ : ∀ p → PathPΣ (ΣPathP p) ≡ p
|
ΣPathP-PathPΣ : ∀ p → PathPΣ (ΣPathP p) ≡ p
|
||||||
ΣPathP-PathPΣ = {!!}
|
ΣPathP-PathPΣ = {!!}
|
||||||
|
@ -172,6 +172,10 @@ and `Torus'` with a path constructor `square` that involves composition.
|
||||||
|
|
||||||
Using these two ideas, define the *Klein bottle* in two different ways.
|
Using these two ideas, define the *Klein bottle* in two different ways.
|
||||||
|
|
||||||
|
```
|
||||||
|
data KleinBottle : Type where
|
||||||
|
```
|
||||||
|
|
||||||
### Exercise 10 (★★)
|
### Exercise 10 (★★)
|
||||||
|
|
||||||
Prove
|
Prove
|
||||||
|
|
|
@ -35,10 +35,10 @@ open import sums
|
||||||
Prove
|
Prove
|
||||||
```agda
|
```agda
|
||||||
uncurry : {A B X : Type} → (A → B → X) → (A × B → X)
|
uncurry : {A B X : Type} → (A → B → X) → (A × B → X)
|
||||||
uncurry = {!!}
|
uncurry f (a , b) = f a b
|
||||||
|
|
||||||
curry : {A B X : Type} → (A × B → X) → (A → B → X)
|
curry : {A B X : Type} → (A × B → X) → (A → B → X)
|
||||||
curry = {!!}
|
curry f a b = f (a , b)
|
||||||
```
|
```
|
||||||
You might know these functions from programming e.g. in Haskell.
|
You might know these functions from programming e.g. in Haskell.
|
||||||
But what do they say under the propositions-as-types interpretation?
|
But what do they say under the propositions-as-types interpretation?
|
||||||
|
@ -108,7 +108,7 @@ tne = {!!}
|
||||||
Prove
|
Prove
|
||||||
```agda
|
```agda
|
||||||
¬¬-functor : {A B : Type} → (A → B) → ¬¬ A → ¬¬ B
|
¬¬-functor : {A B : Type} → (A → B) → ¬¬ A → ¬¬ B
|
||||||
¬¬-functor = {!!}
|
¬¬-functor f ¬¬A ¬B = ¬¬A (λ A → ¬B (f A))
|
||||||
|
|
||||||
¬¬-kleisli : {A B : Type} → (A → ¬¬ B) → ¬¬ A → ¬¬ B
|
¬¬-kleisli : {A B : Type} → (A → ¬¬ B) → ¬¬ A → ¬¬ B
|
||||||
¬¬-kleisli = {!!}
|
¬¬-kleisli = {!!}
|
||||||
|
@ -131,7 +131,8 @@ to a true proposition while an uninhabited type corresponds to a false propositi
|
||||||
With this in mind construct a family
|
With this in mind construct a family
|
||||||
```agda
|
```agda
|
||||||
bool-as-type : Bool → Type
|
bool-as-type : Bool → Type
|
||||||
bool-as-type = {!!}
|
bool-as-type true = 𝟙
|
||||||
|
bool-as-type false = {! 𝟘 !}
|
||||||
```
|
```
|
||||||
such that `bool-as-type true` corresponds to "true" and
|
such that `bool-as-type true` corresponds to "true" and
|
||||||
`bool-as-type false` corresponds to "false". (Hint:
|
`bool-as-type false` corresponds to "false". (Hint:
|
||||||
|
@ -143,7 +144,7 @@ we have seen canonical types corresponding true and false in the lectures)
|
||||||
Prove
|
Prove
|
||||||
```agda
|
```agda
|
||||||
bool-≡-char₁ : ∀ (b b' : Bool) → b ≡ b' → (bool-as-type b ⇔ bool-as-type b')
|
bool-≡-char₁ : ∀ (b b' : Bool) → b ≡ b' → (bool-as-type b ⇔ bool-as-type b')
|
||||||
bool-≡-char₁ = {!!}
|
bool-≡-char₁ b b' p = (λ x → {! !}) , λ x → {! !}
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue