Dominique Devriese | 27 Jan 09:50 2015

Mutual data definitions

Hi all,

Can anyone tell me if the following is supposed to work, or if I
should use old-style mutual blocks for this?  Or maybe I've forgotten
something else?  I currently get an error about a missing definition
for B.

  data B : Set

  data A : Set where
    bA : B → A

  data B : Set where
    aB : A → B
    b : B

Alan Jeffrey | 23 Jan 23:53 2015

Univalence via Agda's primTrustMe again

Hi all,

OK, I made another shot at a computational version of univalence, using 
Agda's primTrustMe to get beta-reduction.

In the attached Agda code, there's a construction of the 2-categorical 
version of univalence such that many of the equivalences are 
beta-reductions. In particular:

   ap(ua(e))(a)  beta reduces to  e(a)

I only did the 2-categorical version, which lifts up the skeletal 
equivalence on Set_0 to a non-skeletal equivalence on Set_1. It would be 
interesting to see if it goes through for any Set_n, to get an 
n-categorical model, but this may require more book-keeping than I am 
capable of.

Let ≣ be the skeletal equivalence satisfying K.

The identity type on Set₀ is (a ≡₀ b) whenever (a ≣ b). From this, we 
can define (A ≃₁ B : Set₀) as per usual (half-adjoint equivalences).

The definition of the identity type on Set₁ is (a ≡₁ b : A) whenever:

- p : (a ≣ b)
- q : ∀ C → (C a ≃₁ C b)
- r : ∀ C D → (q (C ∘ D)) ≣ (≃₁-cong C (q D))

from which we can define (A ≃₂ B : Set₁), and show the 2-categorical 
version of univalence:
(Continue reading)

Sergei Meshveliani | 21 Jan 20:55 2015


Who knows, please,

what has Standard library to express the type constructor 

  \ (P : A → Set) (f : A → A) → (∀ {x} → P x → P (f x))

(f Respects P), (f Preserves P)   do not seem to fit.


Sergei Meshveliani | 18 Jan 13:11 2015

printed goal type

how to fix the attached program?
(about 100 lines).

It ends with 

  e | yes k≡k'  with d
  e | yes k≡k' | suc _ =  PE.refl
  e | yes k≡k' | 0     =  ⊥-elim $ <→≢ d>0 $ PE.sym d≡0
                          d>0 : d > 0
                          d>0 = m<n→n∸m>0 m<m'

                          d≡0 : d ≡ 0
                          d≡0 = ?

The only remaining point is as follows.
In the last branch of  "0",  d ≡ 0  needs, of course, to have a proof.
But I fail to provide such.

I tried     inspect PE.inspect (_≟_ k) k'  ... 
and failed.

Then, I try to write an explicit goal  e'  for  (yes k≡k'),  in a hope
that it will be easier to simplify a proof of  e'.  I set "?" for e' and
copy the type expression given by interactive Agda:  

  e | yes k≡k' = e'                                                    
(Continue reading)

Carlos Camarao | 18 Jan 12:38 2015

Set properties


I implemented SetProperties.agda, with sets represented by lists, that
proves set properties related to deletion, membership, union,
difference, taking of subsets, disjointness. I don't know if they can
be of any use to anybody, or what I could do with it. I'd pleased to
receive any comments. The module is available at

All the best,

Sergei Meshveliani | 18 Jan 11:19 2015

Re: Issue 1402 in agda: Where clauses in rewrite RHS cause internal error

On Sat, 2015-01-17 at 21:22 +0000, agda@... wrote:
> Updates:
> 	Summary: Where clauses in rewrite RHS cause internal error
> 	Owner: andreas....@...
> 	Labels: Rewrite Where
> Comment #4 on issue 1402 by andreas....@...: Where clauses in
> RHS cause internal error
> Here is a simpled instance of the problem encounterd in the original report  
> (#1 might be a different problem).
> open import Common.Equality
> postulate eq : Set1 ≡ Set1
> test : Set1
> test rewrite eq = bla
>    where bla = Set
> It seems that somehow it is assumed that `rewrite` is not followed by  
> `where`.

So far, I have an obscure notion about using `inspect'.
Trying to guess how to use it on practice.
Also I use a certain successful piece of code:

(Continue reading)

Carlos Camarao | 17 Jan 18:31 2015

Set properties


I implemented the attached module SetProperties.agda, with sets
represented by lists, that proves set properties related to deletion,
membership, union, difference, taking of subsets and disjointness.
I don't know if they can be of any use to anybody, or what I could do
with it (if not just leave it to rest). I'd pleased to receive any comments
or suggestions.

All the best,

Attachment (SetProperties.agda): application/octet-stream, 97 KiB
Agda mailing list
Andreas Abel | 17 Jan 12:07 2015

Agda master is anti-classical, injective type constructors are back

This concerns only the unreleased Agda master development branch.

Using heterogeneous equality and big forced indices in a data type SING, 
I manage to prove injectivity of type constructor

   SING : (Set -> Set) -> Set

The rest follows Chung-Kil Hur's refutation of excluded middle, as 
published in January 2010 on the Coq and Agda lists.

My development was fathered by my surprise that I could prove

   inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m

but not by directly matching on the heterogeneous equality (which Agda 
refuses as Fin n = Fin m does not yield n = m), but by first matching on 
i and j, which exposes n and m in the constructor patterns and makes 
then available for unification.

   inj-Fin-≅ {i = zero}  {zero} ≅refl = refl  -- matching on ≅refl succeeds!
   inj-Fin-≅ {i = zero}  {suc j} ()
   inj-Fin-≅ {i = suc i} {zero} ()
   inj-Fin-≅ {i = suc i} {suc j} p = {!p!}   -- Splitting on p succeeds!

This is weird.

A fix would be to not generate any unification constraints for forced 
constructor arguments, for instance

   fzero : (n : Nat) -> Fin (suc n)
(Continue reading)

Alan Jeffrey | 16 Jan 22:03 2015

Univalence via Agda's primTrustMe?

Hi everyone,

In the Agda development of Homotopy Type Theory at the univalence axiom is given by 
three postulates (the map from (A ≃ B) to (A ≡ B) and its β and η rules).

I wonder whether these postulates could be replaced by uses of primTrustMe?

As a reminder, primTrustMe is a trusted function which inhabits the type 
(M ≡ N) for any M and N. It is possible to introduce contradictions 
(e.g. 0 ≡ 1) in the same way as with postulates, so it has to be handled 
with care. The semantics is as for postulates, but with an extra beta 

   primTrustMe M M → refl

In the attached Agda code, primTrustMe is used to define:

     trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q) ≡ p))
     trustme p = ⟨ primTrustMe , primTrustMe ⟩

from which we get the map from (A ≃ B) to (A ≡ B) and its β rule:

   ≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
   ≃-to-≡ p with trustme p
   ≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl

   ≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡ p)
   ≃-to-≡-β p with trustme p
(Continue reading)

Carlos Camarao | 15 Jan 18:55 2015

Termination checking (perhaps could be smarter)


I am writing a simple insertion sort program in Agda, and proving its
correctness. I am using the following predicate (the full code of the
program is attached; I am using Agda version

sorted : List A → Bool
sorted []           = true
sorted (_ ∷ [])    = true
sorted (a ∷ b ∷ x) with a ≤? b
... | yes _ = sorted (b ∷ x)
... | no  _ = false

Agda hightlights the name of function sorted (in light salmon),
indicating that it could not determine the function's termination. But argument
(b ∷ x) is structurally smaller than (a ∷ b ∷ x), right? Any comments?

Please feel free to send me also any other comments you think it is
appropriate, related to the attached Agda code (for example related to
module parameters).


Attachment (insertionSort.agda): application/octet-stream, 2545 bytes
Agda mailing list
(Continue reading)

José Pedro Magalhães | 15 Jan 14:32 2015

Mathematics of Program Construction (MPC 2015): final call for papers

Apologies for multiple copies.


12th International Conference on Mathematics of Program Construction, MPC 2015
Königswinter, Germany, 29 June - 1 July 2015


The MPC conferences aim to promote the development of mathematical principles
and techniques that are demonstrably practical and effective in the process
of constructing computer programs, broadly interpreted.

The 2015 MPC conference will be held in Königswinter, Germany, from 29th June
to 1st July 2015. The previous conferences were held in Twente, The
Netherlands (1989), Oxford, UK (1992), Kloster Irsee, Germany (1995),
Marstrand, Sweden (1998), Ponte de Lima, Portugal (2000), Dagstuhl, Germany
(2002), Stirling, UK (2004, colocated with AMAST), Kuressaare, Estonia (2006,
colocated with AMAST), Marseille, France (2008), Québec City, Canada (2010,
colocated with AMAST), and Madrid, Spain (2012).


Papers are solicited on mathematical methods and tools put to use in program
construction. Topics of interest range from algorithmics to support for
program construction in programming languages and systems. The notion of
"program" is broad, from algorithms to hardware. Some typical areas are type
systems, program analysis and transformation, programming-language semantics,
security, and program logics. Theoretical contributions are welcome, provided
(Continue reading)