← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Function/Related/TypeIsomorphisms.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Function/Related/TypeIsomorphisms.agda
28
28
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
29
29
open import Relation.Binary.Sum
30
30
open import Relation.Nullary
31
 
import Relation.Nullary.Decidable as Dec
 
31
open import Relation.Nullary.Decidable as Dec using (True)
32
32
 
33
33
------------------------------------------------------------------------
34
34
-- Σ is "associative"
428
428
                          D  ∼⟨ sym C≈D ⟩
429
429
                          C  ∎)
430
430
  where open Related.EquationalReasoning
 
431
 
 
432
------------------------------------------------------------------------
 
433
-- A lemma relating True dec and P, where dec : Dec P
 
434
 
 
435
True↔ : ∀ {p} {P : Set p}
 
436
        (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P
 
437
True↔ (yes p) irr = record
 
438
  { to         = P.→-to-⟶ (λ _ → p)
 
439
  ; from       = P.→-to-⟶ (λ _ → _)
 
440
  ; inverse-of = record
 
441
    { left-inverse-of  = λ _ → P.refl
 
442
    ; right-inverse-of = irr p
 
443
    }
 
444
  }
 
445
True↔ (no ¬p) _ = record
 
446
  { to         = P.→-to-⟶ (λ ())
 
447
  ; from       = P.→-to-⟶ (λ p → ¬p p)
 
448
  ; inverse-of = record
 
449
    { left-inverse-of  = λ ()
 
450
    ; right-inverse-of = λ p → ⊥-elim (¬p p)
 
451
    }
 
452
  }
 
453
 
 
454
------------------------------------------------------------------------
 
455
-- Equality between pairs can be expressed as a pair of equalities
 
456
 
 
457
Σ-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : A → Set b} {p₁ p₂ : Σ A B} →
 
458
          (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
 
459
             P.subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔
 
460
          (p₁ ≡ p₂)
 
461
Σ-≡,≡↔≡ {A = A} {B} = record
 
462
  { to         = P.→-to-⟶ to
 
463
  ; from       = P.→-to-⟶ from
 
464
  ; inverse-of = record
 
465
    { left-inverse-of  = left-inverse-of
 
466
    ; right-inverse-of = right-inverse-of
 
467
    }
 
468
  }
 
469
  where
 
470
  to : {p₁ p₂ : Σ A B} →
 
471
       Σ (proj₁ p₁ ≡ proj₁ p₂)
 
472
         (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂) →
 
473
       p₁ ≡ p₂
 
474
  to (P.refl , P.refl) = P.refl
 
475
 
 
476
  from : {p₁ p₂ : Σ A B} →
 
477
         p₁ ≡ p₂ →
 
478
         Σ (proj₁ p₁ ≡ proj₁ p₂)
 
479
           (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂)
 
480
  from P.refl = P.refl , P.refl
 
481
 
 
482
  left-inverse-of : {p₁ p₂ : Σ A B}
 
483
                    (p : Σ (proj₁ p₁ ≡ proj₁ p₂)
 
484
                           (λ x → P.subst B x (proj₂ p₁) ≡ proj₂ p₂)) →
 
485
                    from (to p) ≡ p
 
486
  left-inverse-of (P.refl , P.refl) = P.refl
 
487
 
 
488
  right-inverse-of : {p₁ p₂ : Σ A B} (p : p₁ ≡ p₂) → to (from p) ≡ p
 
489
  right-inverse-of P.refl = P.refl
 
490
 
 
491
×-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} →
 
492
          (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ↔
 
493
          p₁ ≡ p₂
 
494
×-≡,≡↔≡ {A = A} {B} = record
 
495
  { to         = P.→-to-⟶ to
 
496
  ; from       = P.→-to-⟶ from
 
497
  ; inverse-of = record
 
498
    { left-inverse-of  = left-inverse-of
 
499
    ; right-inverse-of = right-inverse-of
 
500
    }
 
501
  }
 
502
  where
 
503
  to : {p₁ p₂ : A × B} →
 
504
       (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂) → p₁ ≡ p₂
 
505
  to (P.refl , P.refl) = P.refl
 
506
 
 
507
  from : {p₁ p₂ : A × B} → p₁ ≡ p₂ →
 
508
         (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)
 
509
  from P.refl = P.refl , P.refl
 
510
 
 
511
  left-inverse-of : {p₁ p₂ : A × B} →
 
512
                    (p : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)) →
 
513
                    from (to p) ≡ p
 
514
  left-inverse-of (P.refl , P.refl) = P.refl
 
515
 
 
516
  right-inverse-of : {p₁ p₂ : A × B} (p : p₁ ≡ p₂) → to (from p) ≡ p
 
517
  right-inverse-of P.refl = P.refl