-
Notifications
You must be signed in to change notification settings - Fork 12
/
Ext.agda
47 lines (39 loc) · 1.95 KB
/
Ext.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
{-# OPTIONS --safe #-}
module Data.Product.Properties.Ext where
open import Data.Product
open import Data.Product.Function.Dependent.Propositional using (cong)
open import Function
open import Function.Related.Propositional
open import Level
open import Relation.Binary.PropositionalEquality hiding (cong; [_])
open import Data.Product.Base as Prod
open import Data.Sum.Base
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
private variable
ℓ : Level
A B C : Set ℓ
a a₁ a₂ b₁ b₂ : Level
k : Kind
∃-cong : {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (A₁↔A₂ : A₁ ↔ A₂)
→ (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ x))
→ Σ A₁ B₁ ∼[ k ] Σ A₂ B₂
∃-cong A₁↔A₂ h = cong A₁↔A₂ h
∃-cong′ : {A : Set a} {B₁ : A → Set b₁} {B₂ : A → Set b₂}
→ (∀ {x} → B₁ x ∼[ k ] B₂ x)
→ Σ A B₁ ∼[ k ] Σ A B₂
∃-cong′ h = ∃-cong (mk↔ (id , id)) h
∃-≡ : ∀ {A : Set a₁} (P : A → Set a₂) {x} → P x ⇔ (∃[ y ] y ≡ x × P y)
∃-≡ P {x} = mk⇔ (λ Px → x , refl , Px) (λ where (y , (refl , Py)) → Py)
-- the version in Function.Related.TypeIsomorphisms isn't level-polymorphic enough
×-distribˡ-⊎' : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
×-distribˡ-⊎' = mk↔ₛ′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
[ (λ _ → P.refl) , (λ _ → P.refl) ]
(uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])
∃-distrib-⊎' : {P Q : A → Set ℓ} → (∃[ a ] (P a ⊎ Q a)) ↔ (∃[ a ] P a ⊎ ∃[ a ] Q a)
∃-distrib-⊎' = mk↔ₛ′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
[ (λ _ → P.refl) , (λ _ → P.refl) ]
(uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])