← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Sigma/Pointwise.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Sigma/Pointwise.agda
49
49
------------------------------------------------------------------------
50
50
-- Rel preserves many properties
51
51
 
52
 
private
53
 
 module Dummy {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b}
54
 
              {R₁ : B.Rel A ℓ₁} {R₂ : I.Rel B ℓ₂} where
 
52
module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b}
 
53
         {R₁ : B.Rel A ℓ₁} {R₂ : I.Rel B ℓ₂} where
55
54
 
56
55
  refl : B.Reflexive R₁ → I.Reflexive B R₂ →
57
56
         B.Reflexive (Rel B R₁ R₂)
77
76
                         (I.IsEquivalence.trans eq₂)
78
77
    }
79
78
 
80
 
open Dummy public
81
 
 
82
79
setoid : ∀ {b₁ b₂ i₁ i₂} →
83
80
         (A : B.Setoid b₁ b₂) → I.Setoid (B.Setoid.Carrier A) i₁ i₂ →
84
81
         B.Setoid _ _