← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Sum.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Sum.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Sums of binary relations
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Relation.Binary.Sum where
8
8
 
9
9
open import Data.Sum as Sum
11
11
open import Data.Unit using (⊤)
12
12
open import Data.Empty
13
13
open import Function
14
 
open import Function.Equality as F using (_⟨$⟩_)
 
14
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
15
15
open import Function.Equivalence as Eq
16
 
  using (Equivalent; _⇔_; module Equivalent)
17
 
  renaming (_∘_ to _⟨∘⟩_)
 
16
  using (Equivalence; _⇔_; module Equivalence)
 
17
open import Function.Injection as Inj
 
18
  using (Injection; _↣_; module Injection)
18
19
open import Function.Inverse as Inv
19
 
  using (Inverse; _⇿_; module Inverse)
20
 
  renaming (_∘_ to _⟪∘⟫_)
 
20
  using (Inverse; _↔_; module Inverse)
 
21
open import Function.LeftInverse as LeftInv
 
22
  using (LeftInverse; _↞_; module LeftInverse)
 
23
open import Function.Related
 
24
open import Function.Surjection as Surj
 
25
  using (Surjection; _↠_; module Surjection)
21
26
open import Level
22
27
open import Relation.Nullary
23
28
open import Relation.Binary
306
311
    }
307
312
    where open IsDecTotalOrder
308
313
 
 
314
  _⊎-<-isStrictTotalOrder_ :
 
315
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
 
316
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
 
317
    IsStrictTotalOrder ≈₁ <₁ → IsStrictTotalOrder ≈₂ <₂ →
 
318
    IsStrictTotalOrder (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
 
319
  sto₁ ⊎-<-isStrictTotalOrder sto₂ = record
 
320
    { isEquivalence = isEquivalence sto₁ ⊎-isEquivalence
 
321
                      isEquivalence sto₂
 
322
    ; trans         = trans    sto₁ ⊎-transitive     trans    sto₂
 
323
    ; compare       = compare  sto₁ ⊎-<-trichotomous compare  sto₂
 
324
    ; <-resp-≈      = <-resp-≈ sto₁ ⊎-≈-respects₂    <-resp-≈ sto₂
 
325
    }
 
326
    where open IsStrictTotalOrder
 
327
 
309
328
open Dummy public
310
329
 
311
330
------------------------------------------------------------------------
373
392
                      isDecTotalOrder to₂
374
393
  } where open DecTotalOrder
375
394
 
 
395
_⊎-<-strictTotalOrder_ :
 
396
  ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
 
397
  StrictTotalOrder p₁ p₂ p₃ → StrictTotalOrder p₄ p₅ p₆ →
 
398
  StrictTotalOrder _ _ _
 
399
sto₁ ⊎-<-strictTotalOrder sto₂ = record
 
400
  { _<_                = _<_ sto₁ ⊎-< _<_ sto₂
 
401
  ; isStrictTotalOrder = isStrictTotalOrder sto₁
 
402
                           ⊎-<-isStrictTotalOrder
 
403
                         isStrictTotalOrder sto₂
 
404
  } where open StrictTotalOrder
 
405
 
376
406
------------------------------------------------------------------------
 
407
-- Some properties related to "relatedness"
377
408
 
378
 
⊎-Rel⇿≡ : ∀ {a b} (A : Set a) (B : Set b) →
 
409
⊎-Rel↔≡ : ∀ {a b} (A : Set a) (B : Set b) →
379
410
          Inverse (P.setoid A ⊎-setoid P.setoid B) (P.setoid (A ⊎ B))
380
 
⊎-Rel⇿≡ _ _ = record
 
411
⊎-Rel↔≡ _ _ = record
381
412
  { to         = record { _⟨$⟩_ = id; cong = to-cong   }
382
413
  ; from       = record { _⟨$⟩_ = id; cong = from-cong }
383
414
  ; inverse-of = record
395
425
  from-cong : P._≡_ ⇒ (P._≡_ ⊎-Rel P._≡_)
396
426
  from-cong P.refl = P.refl ⊎-refl P.refl
397
427
 
398
 
_⊎-equivalent_ :
 
428
_⊎-⟶_ :
399
429
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
400
430
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
401
431
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
402
 
  Equivalent A B → Equivalent C D →
403
 
  Equivalent (A ⊎-setoid C) (B ⊎-setoid D)
404
 
_⊎-equivalent_ {A = A} {B} {C} {D} A⇔B C⇔D = record
405
 
  { to   = record { _⟨$⟩_ = to;   cong = to-cong   }
406
 
  ; from = record { _⟨$⟩_ = from; cong = from-cong }
 
432
  A ⟶ B → C ⟶ D → (A ⊎-setoid C) ⟶ (B ⊎-setoid D)
 
433
_⊎-⟶_ {A = A} {B} {C} {D} f g = record
 
434
  { _⟨$⟩_ = fg
 
435
  ; cong  = fg-cong
407
436
  }
408
437
  where
409
438
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
410
439
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)
411
440
 
412
 
  to = Sum.map (_⟨$⟩_ (Equivalent.to A⇔B))
413
 
               (_⟨$⟩_ (Equivalent.to C⇔D))
414
 
 
415
 
  to-cong : _≈AC_ =[ to ]⇒ _≈BD_
416
 
  to-cong (₁∼₂ ())
417
 
  to-cong (₁∼₁ x∼₁y) = ₁∼₁ $ F.cong (Equivalent.to A⇔B) x∼₁y
418
 
  to-cong (₂∼₂ x∼₂y) = ₂∼₂ $ F.cong (Equivalent.to C⇔D) x∼₂y
419
 
 
420
 
  from = Sum.map (_⟨$⟩_ (Equivalent.from A⇔B))
421
 
                 (_⟨$⟩_ (Equivalent.from C⇔D))
422
 
 
423
 
  from-cong : _≈BD_ =[ from ]⇒ _≈AC_
424
 
  from-cong (₁∼₂ ())
425
 
  from-cong (₁∼₁ x∼₁y) = ₁∼₁ $ F.cong (Equivalent.from A⇔B) x∼₁y
426
 
  from-cong (₂∼₂ x∼₂y) = ₂∼₂ $ F.cong (Equivalent.from C⇔D) x∼₂y
 
441
  fg = Sum.map (_⟨$⟩_ f) (_⟨$⟩_ g)
 
442
 
 
443
  fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
 
444
  fg-cong (₁∼₂ ())
 
445
  fg-cong (₁∼₁ x∼₁y) = ₁∼₁ $ F.cong f x∼₁y
 
446
  fg-cong (₂∼₂ x∼₂y) = ₂∼₂ $ F.cong g x∼₂y
 
447
 
 
448
_⊎-equivalence_ :
 
449
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
 
450
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
 
451
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
 
452
  Equivalence A B → Equivalence C D →
 
453
  Equivalence (A ⊎-setoid C) (B ⊎-setoid D)
 
454
A⇔B ⊎-equivalence C⇔D = record
 
455
  { to   = to   A⇔B ⊎-⟶ to   C⇔D
 
456
  ; from = from A⇔B ⊎-⟶ from C⇔D
 
457
  } where open Equivalence
427
458
 
428
459
_⊎-⇔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
429
460
        A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
430
461
_⊎-⇔_ {A = A} {B} {C} {D} A⇔B C⇔D =
431
 
  Inverse.equivalent (⊎-Rel⇿≡ B D) ⟨∘⟩
432
 
  A⇔B ⊎-equivalent C⇔D ⟨∘⟩
433
 
  Eq.sym (Inverse.equivalent (⊎-Rel⇿≡ A C))
 
462
  Inverse.equivalence (⊎-Rel↔≡ B D) ⟨∘⟩
 
463
  A⇔B ⊎-equivalence C⇔D ⟨∘⟩
 
464
  Eq.sym (Inverse.equivalence (⊎-Rel↔≡ A C))
 
465
  where open Eq using () renaming (_∘_ to _⟨∘⟩_)
 
466
 
 
467
_⊎-injection_ :
 
468
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
 
469
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
 
470
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
 
471
  Injection A B → Injection C D →
 
472
  Injection (A ⊎-setoid C) (B ⊎-setoid D)
 
473
_⊎-injection_ {A = A} {B} {C} {D} A↣B C↣D = record
 
474
  { to        = to A↣B ⊎-⟶ to C↣D
 
475
  ; injective = inj _ _
 
476
  }
 
477
  where
 
478
  open Injection
 
479
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
 
480
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)
 
481
 
 
482
  inj : ∀ x y →
 
483
        (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ x ≈BD (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ y →
 
484
        x ≈AC y
 
485
  inj (inj₁ x) (inj₁ y) (₁∼₁ x∼₁y) = ₁∼₁ (injective A↣B x∼₁y)
 
486
  inj (inj₂ x) (inj₂ y) (₂∼₂ x∼₂y) = ₂∼₂ (injective C↣D x∼₂y)
 
487
  inj (inj₁ x) (inj₂ y) (₁∼₂ ())
 
488
  inj (inj₂ x) (inj₁ y) ()
 
489
 
 
490
_⊎-↣_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
 
491
        A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D)
 
492
_⊎-↣_ {A = A} {B} {C} {D} A↣B C↣D =
 
493
  Inverse.injection (⊎-Rel↔≡ B D) ⟨∘⟩
 
494
  A↣B ⊎-injection C↣D ⟨∘⟩
 
495
  Inverse.injection (Inv.sym (⊎-Rel↔≡ A C))
 
496
  where open Inj using () renaming (_∘_ to _⟨∘⟩_)
 
497
 
 
498
_⊎-left-inverse_ :
 
499
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
 
500
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
 
501
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
 
502
  LeftInverse A B → LeftInverse C D →
 
503
  LeftInverse (A ⊎-setoid C) (B ⊎-setoid D)
 
504
A↞B ⊎-left-inverse C↞D = record
 
505
  { to              = Equivalence.to eq
 
506
  ; from            = Equivalence.from eq
 
507
  ; left-inverse-of = [ ₁∼₁ ∘ left-inverse-of A↞B
 
508
                      , ₂∼₂ ∘ left-inverse-of C↞D
 
509
                      ]
 
510
  }
 
511
  where
 
512
  open LeftInverse
 
513
  eq = LeftInverse.equivalence A↞B ⊎-equivalence
 
514
       LeftInverse.equivalence C↞D
 
515
 
 
516
_⊎-↞_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
 
517
        A ↞ B → C ↞ D → (A ⊎ C) ↞ (B ⊎ D)
 
518
_⊎-↞_ {A = A} {B} {C} {D} A↞B C↞D =
 
519
  Inverse.left-inverse (⊎-Rel↔≡ B D) ⟨∘⟩
 
520
  A↞B ⊎-left-inverse C↞D ⟨∘⟩
 
521
  Inverse.left-inverse (Inv.sym (⊎-Rel↔≡ A C))
 
522
  where open LeftInv using () renaming (_∘_ to _⟨∘⟩_)
 
523
 
 
524
_⊎-surjection_ :
 
525
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
 
526
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
 
527
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
 
528
  Surjection A B → Surjection C D →
 
529
  Surjection (A ⊎-setoid C) (B ⊎-setoid D)
 
530
A↠B ⊎-surjection C↠D = record
 
531
  { to         = LeftInverse.from inv
 
532
  ; surjective = record
 
533
    { from             = LeftInverse.to inv
 
534
    ; right-inverse-of = LeftInverse.left-inverse-of inv
 
535
    }
 
536
  }
 
537
  where
 
538
  open Surjection
 
539
  inv = right-inverse A↠B ⊎-left-inverse right-inverse C↠D
 
540
 
 
541
_⊎-↠_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
 
542
        A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D)
 
543
_⊎-↠_ {A = A} {B} {C} {D} A↠B C↠D =
 
544
  Inverse.surjection (⊎-Rel↔≡ B D) ⟨∘⟩
 
545
  A↠B ⊎-surjection C↠D ⟨∘⟩
 
546
  Inverse.surjection (Inv.sym (⊎-Rel↔≡ A C))
 
547
  where open Surj using () renaming (_∘_ to _⟨∘⟩_)
434
548
 
435
549
_⊎-inverse_ :
436
550
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
437
551
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
438
552
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
439
553
  Inverse A B → Inverse C D → Inverse (A ⊎-setoid C) (B ⊎-setoid D)
440
 
A⇿B ⊎-inverse C⇿D = record
441
 
  { to         = Equivalent.to   eq
442
 
  ; from       = Equivalent.from eq
 
554
A↔B ⊎-inverse C↔D = record
 
555
  { to         = Surjection.to   surj
 
556
  ; from       = Surjection.from surj
443
557
  ; inverse-of = record
444
 
    { left-inverse-of  = [ ₁∼₁ ∘ left-inverse-of A⇿B
445
 
                         , ₂∼₂ ∘ left-inverse-of C⇿D
446
 
                         ]
447
 
    ; right-inverse-of = [ ₁∼₁ ∘ right-inverse-of A⇿B
448
 
                         , ₂∼₂ ∘ right-inverse-of C⇿D
449
 
                         ]
 
558
    { left-inverse-of  = LeftInverse.left-inverse-of inv
 
559
    ; right-inverse-of = Surjection.right-inverse-of surj
450
560
    }
451
561
  }
452
562
  where
453
563
  open Inverse
454
 
  eq = equivalent A⇿B ⊎-equivalent equivalent C⇿D
455
 
 
456
 
_⊎-⇿_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
457
 
        A ⇿ B → C ⇿ D → (A ⊎ C) ⇿ (B ⊎ D)
458
 
_⊎-⇿_ {A = A} {B} {C} {D} A⇿B C⇿D =
459
 
  ⊎-Rel⇿≡ B D ⟪∘⟫ A⇿B ⊎-inverse C⇿D ⟪∘⟫ Inv.sym (⊎-Rel⇿≡ A C)
 
564
  surj = Inverse.surjection   A↔B ⊎-surjection
 
565
         Inverse.surjection   C↔D
 
566
  inv  = Inverse.left-inverse A↔B ⊎-left-inverse
 
567
         Inverse.left-inverse C↔D
 
568
 
 
569
_⊎-↔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
 
570
        A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
 
571
_⊎-↔_ {A = A} {B} {C} {D} A↔B C↔D =
 
572
  ⊎-Rel↔≡ B D ⟨∘⟩ A↔B ⊎-inverse C↔D ⟨∘⟩ Inv.sym (⊎-Rel↔≡ A C)
 
573
  where open Inv using () renaming (_∘_ to _⟨∘⟩_)
 
574
 
 
575
_⊎-cong_ : ∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
 
576
           A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
 
577
_⊎-cong_ {implication}         = Sum.map
 
578
_⊎-cong_ {reverse-implication} = λ f g → lam (Sum.map (app-← f) (app-← g))
 
579
_⊎-cong_ {equivalence}         = _⊎-⇔_
 
580
_⊎-cong_ {injection}           = _⊎-↣_
 
581
_⊎-cong_ {reverse-injection}   = λ f g → lam (app-↢ f ⊎-↣ app-↢ g)
 
582
_⊎-cong_ {left-inverse}        = _⊎-↞_
 
583
_⊎-cong_ {surjection}          = _⊎-↠_
 
584
_⊎-cong_ {bijection}           = _⊎-↔_