Using irrelevant fields
<p>Is it possible to declare fields in a record irrelevant but still use them somewhere?</p>

<p>Suppose I have</p>

<pre><code>postulate f : ℕ → ℕ
record Silly x : Set where
  field
    n : ℕ
    s : f n ≡ x

open Silly
</code></pre>

<p>Then, I can</p>

<pre><code>same-silly : ∀{x} {p q : Silly x} → f (n p) ≡ f(n q)
same-silly {x} {p} {q} = ≡-trans (s p) (≡-sym (s q))
</code></pre>

<p>But if I use dotted-fields,</p>

<pre><code>record Silly x : Set where
  field
    n : ℕ
    .s : f n ≡ x  -- note the dot
</code></pre>

<p>then <code>same-silly</code> can no longer be proven ---not by me at least.
When I attempt to use <code>s</code>, as in the definition above, Agda informs me <code>Identifier s is declared irrelevant, so it cannot be used here</code>.</p>

<p>I understand that I declared <code>s</code> irrelevant by dotting it, but I still want a bit of access to it: enough access to define <code>same-silly</code>. Is there a way to have this little bit but not complete access? What I mean is that I am thinking of <code>s</code> as a coherency condition that I'd like to use once in a blue-moon, but not terrible important and so the dot. Maybe ignore this paragraph.</p>

<p>Is it possible to form <code>same-silly</code> and have <code>s</code> be dotted?</p>

<p>(</p>

<p>Aside: does the dotted pattern mean propositional equality coincides with the relation</p>

<pre><code>_~_ : ∀{x} (p q : Silly x) → Set
p ~ q = n p ≡ n q
</code></pre>

<p>? In particular, by adding to the record <code>constructor _#_</code>, I can show</p>

<pre><code>eq : ∀{m x}{p q : f m ≡ x} → (m # p) ≡ (m # q) 
eq = ≡-refl
</code></pre>

<p>but I'm not yet certain that dotting fields means that definitionally equality ignores the dotted fields.</p>

<p>I'm browsing <a href="http://wiki.portal.chalmers.se/agda/agda.php?n=ForkedReferenceManual.Records#Irrelevantfields" rel="nofollow">http://wiki.portal.chalmers.se/agda/agda.php?n=ForkedReferenceManual.Records#Irrelevantfields</a>; which says that there are projections for dotted fields, but it seems I cannot use them anywhere.</p>

<p>)</p>

<p>Any help is appreciated!</p>