Guillermo Calderon | 28 Jun 20:27 2016
Picon

Formalization of Linear Algebra in agda

Dear all,

I am looking for a formalization  in Agda
of vectorial spaces (over a field).
My concern is to work in the formalization of some concepts involved 
with Grassman and Clifford algebras which are defined as extensions of
vectorial spaces.

I would be very grateful if anyone can give me some references on this 
topic.

Thanks,

Guillermo
Ren Rise | 24 Jun 23:14 2016
Picon

Re: help required for installing GHC or whole Haskell platform

Please see below my perpetual efforts to get Agda installed on my Windows 10 workstation and to start exploring Agda is resulting in failures after failures over the last 7-8 days.
Please come to my aid. I am not one to give up, never until I get what I want. 
 
C:\Users\SurajZ>cd C:\Program Files\Haskell Platform
C:\Program Files\Haskell Platform>cabal install agda2
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
cabal: There is no package named 'agda2'.
You may need to run 'cabal update' to get the latest list of available
packages.
C:\Program Files\Haskell Platform>cabal update
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
C:\Program Files\Haskell Platform>cabal install Agda
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
cabal: There is no package named 'Agda'.
You may need to run 'cabal update' to get the latest list of available
packages.
C:\Program Files\Haskell Platform>
 
Sent: Friday, June 24, 2016 at 12:02 AM
From: "Oleg Lobachev" <lobachev <at> Mathematik.Uni-Marburg.de>
To: "Ren Rise" <ren.rise <at> gmx.com>
Subject: Re: [Agda] help required for installing GHC or whole Haskell platform
Not cabal install, but cabal install agda2 or how it was again. 

Sent from my iPhone

On 22.06.2016, at 07:53, Ren Rise <ren.rise <at> gmx.com> wrote:
 
I have just downloaded cabal by running cabal update. Please see the followins lines from my command prompt: 
 
C:\Program Files\Haskell Platform>cabal update
Downloading the latest package list from hackage.haskell.org
 
But when I run cabal install, it again throws up exceptions:
 
C:\Program Files\Haskell Platform>cabal install
cabal: Error reading local package.
Couldn't find .cabal file in: .
C:\Program Files\Haskell Platform>
 
Now what do I do?
 
Sent: Wednesday, June 22, 2016 at 9:49 AM
From: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
To: "Ren Rise" <ren.rise <at> gmx.com>
Subject: Re: [Agda] help required for installing GHC or whole Haskell platform
On 21 June 2016 at 23:08, Ren Rise <ren.rise <at> gmx.com> wrote:
> C:\Program Files\Haskell Platform>cabal install Agda
> 'cabal' is not recognized as an internal or external command,

The cabal program is not in your path.


--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
_______________________________________________
Agda mailing list
Agda <at> lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Jeremy Yallop | 23 Jun 10:18 2016
Picon

PEPM 2017 Call for Papers

CALL FOR PAPERS
Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017)

http://conf.researchr.org/home/PEPM-2017

Paris, France, January 16th - 17th, 2017
(co-located with POPL 2017)

PEPM is the premier forum for discussion of semantics-based program
manipulation.  The first ACM SIGPLAN PEPM symposium took place in
1991, and meetings have been held in affiliation with POPL every year
since 2006.

PEPM 2017 will be based on a broad interpretation of semantics-based
program manipulation, reflecting the expanded scope of PEPM in recent
years beyond the traditionally covered areas of partial evaluation and
specialization.  Specifically, PEPM 2017 will include practical
applications of program transformations such as refactoring tools, and
practical implementation techniques such as rule-based transformation
systems.  In addition, the scope of PEPM covers manipulation and
transformations of program and system representations such as
structural and semantic models that occur in the context of
model-driven development.  In order to maintain the dynamic and
interactive nature of PEPM and to encourage participation by
practitioners, we also solicit submissions of short papers, including
tool demonstrations, and of posters.

Scope
-----

Topics of interest for PEPM 2017 include, but are not limited to:

* Program and model manipulation techniques such as: supercompilation,
  partial evaluation, fusion, on-the-fly program adaptation, active
  libraries, program inversion, slicing, symbolic execution,
  refactoring, decompilation, and obfuscation.

* Program analysis techniques that are used to drive program/model
  manipulation such as: abstract interpretation, termination checking,
  binding-time analysis, constraint solving, type systems, automated
  testing and test case generation.

* Techniques that treat programs/models as data objects including
  metaprogramming, generative programming, embedded domain-specific
  languages, program synthesis by sketching and inductive programming,
  staged computation, and model-driven program generation and
  transformation.

* Application of the above techniques including case studies of
  program manipulation in real-world (industrial, open-source)
  projects and software development processes, descriptions of robust
  tools capable of effectively handling realistic applications,
  benchmarking.  Examples of application domains include legacy
  program understanding and transformation, DSL implementations,
  visual languages and end-user programming, scientific computing,
  middleware frameworks and infrastructure needed for distributed and
  web-based applications, embedded and resource-limited computation,
  and security.

This list of categories is not exhaustive, and we encourage
submissions describing applications of semantics-based program
manipulation techniques in new domains.  If you have a question as to
whether a potential submission is within the scope of the workshop,
please contact the programme chairs.

Submission categories and guidelines
------------------------------------

Three kinds of submissions will be accepted: Regular Research Papers,
Short Papers and Posters.

* Regular Research Papers should describe new results, and will be
  judged on originality, correctness, significance and clarity.
  Regular research papers must not exceed 12 pages in ACM Proceedings
  style (including appendix).

* Short Papers may include tool demonstrations and presentations of
  exciting if not fully polished research, and of interesting
  academic, industrial and open-source applications that are new or
  unfamiliar.  Short papers must not exceed 6 pages in ACM Proceedings
  style (including appendix).

* Posters should describe work relevant to the PEPM community, and
  must not exceed 2 pages in ACM Proceedings style.  We invite poster
  submissions that present early work not yet ready for submission to
  a conference or journal, identify new research problems, showcase
  tools and technologies developed by the author(s), or describe
  student research projects.

At least one author of each accepted contribution must attend the
workshop and present the work.  In the case of tool demonstration
papers, a live demonstration of the described tool is expected.
Suggested topics, evaluation criteria, and writing guidelines for both
research tool demonstration papers will be made available on the PEPM
2017 web site.

Student participants with accepted papers can apply for a SIGPLAN PAC
grant to help cover travel expenses and other support.  PAC also
offers other support, such as for child-care expenses during the
meeting or for travel costs for companions of SIGPLAN members with
physical disabilities, as well as for travel from locations outside of
North America and Europe.  For details on the PAC programme, see its
web page.

Publication and special issue
-----------------------------

All accepted papers, short papers and posters included, will appear in
formal proceedings published by ACM Press.  Accepted papers will be
included in the ACM Digital Library.  Authors of selected papers from
PEPM 2016 and PEPM 2017 will also be invited to expand their papers
for publication in a special issue of the journal Computer Languages,
Systems and Structures (COMLAN, Elsevier).

Best paper award
----------------

PEPM 2017 continues the tradition of a Best Paper award.  The winner
will be announced at the workshop.

Submission
----------

Papers should be submitted electronically via HotCRP.

   https://pepm17.hotcrp.com/

Authors using LaTeX to prepare their submissions should use the new
improved SIGPLAN proceedings style, and specifically the
sigplanconf.cls 9pt template.

Important Dates
---------------

For Regular Research Papers and Short Papers:

 * Abstract submission : Tuesday 13th September 2016
 * Paper submission    : Friday 16th September 2016
 * Author notification : Monday 24th October 2016
 * Camera ready        : Monday 28th November 2016

For Posters:

 * Poster submission   : Sunday 30th October 2016
 * Author notification : Friday 10th November 2016
 * Camera ready        : Monday 28th November 2016

PEPM workshop:

 * Workshop            : Monday 16th - Tuesday 17th January 2017

The proceedings will be published 2 weeks pre-conference.

AUTHORS TAKE NOTE: The official publication date is the date the
proceedings are made available in the ACM Digital Library. This date
may be up to two weeks prior to the first day of your conference. The
official publication date affects the deadline for any patent filings
related to published work. (For those rare conferences whose
proceedings are published in the ACM Digital Library after the
conference is over, the official publication date remains the first
day of the conference.).

PEPM'17 Programme Co-Chairs
-------------------

Ulrik Schultz (University of Southern Denmark), ups@...
Jeremy Yallop (University of Cambridge), jeremy.yallop@...
Ren Rise | 22 Jun 23:01 2016
Picon

Fw: Re: Re: help required for installing GHC or whole Haskell platform

 
 
Sent: Thursday, June 23, 2016 at 2:31 AM
From: "Ren Rise" <ren.rise <at> gmx.com>
To: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
Subject: Re: Re: [Agda] help required for installing GHC or whole Haskell platform
where do I install the C Compiler? Into Haskell Platform folder or elsewhere in the C root directory?
 
Sent: Thursday, June 23, 2016 at 1:37 AM
From: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
To: "Ren Rise" <ren.rise <at> gmx.com>
Cc: "Agda users" <agda <at> lists.chalmers.se>
Subject: Re: Re: [Agda] help required for installing GHC or whole Haskell platform
On 22 June 2016 at 14:29, Ren Rise <ren.rise <at> gmx.com> wrote:
> No,I don't have any C compiler installed. If you insist, I can install a C
> compiler.


After installing the C compiler, try to install the old-time library using

cabal install old-time


--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Ren Rise | 22 Jun 07:53 2016
Picon

Re: help required for installing GHC or whole Haskell platform

I have just downloaded cabal by running cabal update. Please see the followins lines from my command prompt: 
 
C:\Program Files\Haskell Platform>cabal update
Downloading the latest package list from hackage.haskell.org
 
But when I run cabal install, it again throws up exceptions:
 
C:\Program Files\Haskell Platform>cabal install
cabal: Error reading local package.
Couldn't find .cabal file in: .
C:\Program Files\Haskell Platform>
 
Now what do I do?
 
Sent: Wednesday, June 22, 2016 at 9:49 AM
From: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
To: "Ren Rise" <ren.rise <at> gmx.com>
Subject: Re: [Agda] help required for installing GHC or whole Haskell platform
On 21 June 2016 at 23:08, Ren Rise <ren.rise <at> gmx.com> wrote:
> C:\Program Files\Haskell Platform>cabal install Agda
> 'cabal' is not recognized as an internal or external command,

The cabal program is not in your path.


--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Ren Rise | 21 Jun 20:28 2016
Picon

help required for installing GHC or whole Haskell platform

Hi all,
 
I have downloaded Stack into my C root of Windows 10 workstation and GHC 7.10.3. Now how do I proceed on installing cabal and Agda? 
Last time, I downloaded the Whole Haskell Platform 8.0.1 from here: https://www.haskell.org/platform/
But it did not work last time. 
Or should I again download 8.01. and then try to modify my cabal config file before starting to install and run Agda?
 
Please help!.
 
Ren
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andrés Sicard-Ramírez | 21 Jun 17:31 2016
Picon

[ANNOUNCE] Agda 2.5.1.1

Dear all,

The Agda Team is very pleased to announce the release of Agda 2.5.1.1.

GHC supported versions
======================

Agda 2.5.1.1 has been tested with GHC 7.6.3, 7.8.4, 7.10.3 and 8.0.1 (new)

Installation
============

  cabal update && cabal install Agda

Standard library
================

Agda standard library 0.12 available at

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary

is compatible with Agda 2.5.1.1.

What is new?
============

Agda 2.5.1.1 fixes a severe performance bug with instance arguments:

  * https://github.com/agda/agda/issues/1952
  * https://github.com/agda/agda/issues/1955
  * https://github.com/agda/agda/issues/1998
  * https://github.com/agda/agda/issues/2025

as well as the following minor issues:

  * https://github.com/agda/agda/issues/1322
  * https://github.com/agda/agda/issues/2034 (function type instance goals)
  * https://github.com/agda/agda/issues/1950 (case split in with-function)
  * https://github.com/agda/agda/issues/1951 (mixfix binders not
working in 'syntax')
  * https://github.com/agda/agda/issues/1967 (too eager instance search error)
  * https://github.com/agda/agda/issues/1974 (lost constraint dependencies)
  * https://github.com/agda/agda/issues/1982 (internal error in unifier)

More information about the changes included in Agda 2.5.1.1 can be found in

  http://hackage.haskell.org/package/Agda-2.5.1.1/changelog

Enjoy Agda 2.5.1.1

--
Andrés, on behalf of the Agda Team
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y
puede contener información confidencial, material privilegiado o información protegida por
derecho de autor. Está prohibida cualquier copia, utilización, indebida retención,
modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí contenida es
responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo
que el mensaje contenga. The information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information protected by copyright. Its
prohibited any copy, use, improper retention, modification, dissemination, distribution or total or
partial reproduction. If you receive this message by error, please contact the sender and delete it. The
information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is
not responsible for what the message contains.
Graham Hutton | 21 Jun 17:20 2016
Picon
Picon

Programming in Haskell - 2nd Edition

Dear all,

I'm delighted to announce that the 2nd edition of Programming
in Haskell will be published in August 2016!  The new edition
has been extensively updated and expanded to include recent and
more advanced features of Haskell, new examples and exercises,
selected solutions, and freely downloadable lecture slides and
example code.  Further details, including how to preorder and
obtain inspection copies, are provided below.

Best wishes,

Graham

=================================================================

*** BOOK ANNOUNCEMENT ***

Programming in Haskell - 2nd Edition

Graham Hutton, University of Nottingham

Cambridge University Press, August 2016

320 pages, 120 exercises, ISBN 9781316626221

http://tinyurl.com/PIH-2e

=================================================================

DESCRIPTION:

Haskell is a purely functional language that allows programmers
to rapidly develop clear, concise, and correct software.  The
language has grown in popularity in recent years, both in teaching
and in industry.  This book is based on the author's experience
of teaching Haskell for more than twenty years.  All concepts
are explained from first principles and no programming experience
is required, making this book accessible to a broad spectrum
of readers.  While Part I focuses on basic concepts, Part II
introduces the reader to more advanced topics.

This new edition has been extensively updated and expanded to
include recent and more advanced features of Haskell, new examples
and exercises, selected solutions, and freely downloadable lecture
slides and example code.  The presentation is clean and simple,
while also being fully compliant with the latest version of
the language, including recent changes concerning applicative,
monadic, foldable, and traversable types.

=================================================================

CONTENTS:

Foreword
Preface
Part I. Basic Concepts:
1. Introduction
2. First steps
3. Types and classes
4. Defining functions
5. List comprehensions
6. Recursive functions
7. Higher-order functions
8. Declaring types and classes
9. The countdown problem
Part II. Going Further:
10. Interactive programming
11. Unbeatable tic-tac-toe
12. Monads and more
13. Monadic parsing
14. Foldables and friends
15. Lazy evaluation
16. Reasoning about programs
17. Calculating compilers
Appendix A. Selected solutions
Appendix B. Standard prelude
Bibliography
Index

=================================================================

AUTHOR:

Graham Hutton is Professor of Computer Science at the University
of Nottingham.  He has taught Haskell to thousands of students
and received numerous best lecturer awards.  Hutton has served as
an editor of the Journal of Functional Programming, Chair of the
Haskell Symposium and the International Conference on Functional
Programming, and Vice-Chair of the ACM Special Interest Group on
Programming Languages, and he is an ACM Distinguished Scientist.

=================================================================

FURTHER DETAILS:

The following web page includes details for how the book can be
preordered, and how lecturers can obtain inspection copies:

http://tinyurl.com/PIH-2e

=================================================================

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.
Jasmin Blanchette | 21 Jun 15:18 2016
Picon

ITP 2016: Call for participation

The 7th International Conference on Interactive Theorem Proving
22 to 27 August 2016 in Nancy, France
https://itp2016.inria.fr

Early registration deadline: 30 June
Main conference: 22 August to 25 August (morning)
Affiliated events: 25 August (afternoon) to 27 August

ITP is the premier international conference for researchers from all areas of
interactive theorem proving and its applications. The program committee
accepted 27 regular papers and 5 rough diamonds this year:

    https://itp2016.inria.fr/program/

There will be invited talks by

    Viktor Kuncak (EPFL)
    Grant Olney Passmore (Aesthetic Integration and University of Cambridge)
    Nikhil Swamy (Microsoft Research)

The following affiliated events will take place after the main conference:

    Coq Workshop 2016
    Isabelle Workshop 2016
    Mathematical Components, an Introduction

Up-to-date information and online registration can be found at

    https://itp2016.inria.fr
Janis Voigtlaender | 21 Jun 12:51 2016
Picon
Gravatar

WFLP 2016 - Final Call for Papers

Register an abstract within the next 48 hours, and a full paper,
work-in-progress report or system description 7 days later!

***********************************************************

24th International Workshop on
Functional and (Constraint) Logic Programming (WFLP 2016)

https://wflp2016.github.io/

September 13-14, part of the
Leipzig Week of Declarative Programming (L-DEC 2016)

Formal proceedings will be published by EPTCS (http://www.eptcs.org/).

Both full technical papers and less formal work-in-progress report
submissions are welcome, as are system descriptions. More details
below and on the web page.

***********************************************************

Deadlines:

* abstract submission: June 22, 2016 (extended)
* paper submission: June 29, 2016 (extended)
* notification: July 15, 2016
* camera-ready (workshop) version due: August 10, 2016

Submissions can be directly accepted for publication in the formal
EPTCS proceedings, or accepted for presentation at the workshop and
invited to another round of reviewing after revision.

***********************************************************

The international workshops on functional and (constraint) logic
programming aim at bringing together researchers, students, and
practitioners interested in functional programming, logic programming,
and their integration. This year the workshop is co-located with two
other events as part of http://nfa.imn.htwk-leipzig.de/LDEC2016/
in order to promote the cross-fertilizing exchange of ideas and
experiences among and between the communities interested in the
foundations, applications, and combinations of high-level,
declarative programming languages and related areas.

Topics of interest for WFLP include (but are not limited to):

* Functional programming
* Logic programming
* Constraint programming
* Deductive databases, data mining
* Extensions of declarative languages, objects
* Multi-paradigm declarative programming
* Foundations, semantics, nonmonotonic reasoning, dynamics
* Parallelism, concurrency
* Program analysis, abstract interpretation
* Program transformation, partial evaluation, meta-programming
* Specification, verification, declarative debugging
* Knowledge representation, machine learning
* Interaction of declarative programming with other formalisms
* Implementation of declarative languages
* Advanced programming environments and tools
* Software engineering for declarative programming
* Applications

The primary focus is on new and original research results, but
submissions describing innovative products, prototypes under
development, application systems, or interesting experiments
(e.g., benchmarks) are also encouraged.

There are separate submission categories for work-in-progress reports
and system descriptions. Authors are welcome to indicate that they
want to present their work in a talk but not include a paper in the
formal proceedings.

Submission is via EasyChair at
https://easychair.org/conferences/?conf=wflp2016

The formal proceedings are prepared jointly with WLP 2016 and will be
published in EPTCS: http://www.eptcs.org/

More details about submission format, LaTeX style etc., can be found
on the web page: https://wflp2016.github.io/

***********************************************************

Program Committee:

* Slim Abdennadher, German University in Cairo, Egypt
* Sergio Antoy, Portland State University, USA
* Sebastian Fischer, Freelancer, Germany
* Francisco J. Lopez Fraguas, Universidad Complutense de Madrid, Spain
* Michael Hanus, University of Kiel, Germany
* Sebastiaan Joosten, University of Innsbruck, Austria
* Kazutaka Matsuda, Tohoku University, Japan
* Martin Sulzmann, Karlsruhe University of Applied Sciences, Germany
* Janis Voigtlaender (Chair), University of Bonn, Germany
Katsutoshi Itoh | 20 Jun 22:23 2016
Picon
Gravatar

excluded-middle

Hi all.

I'd like to use excluded-middle like below:

```
 A∪Aᶜ≈U : ∀ {ℓ} {X : Set ℓ} {A : Pred X lzero} → A ∪ A ᶜ ≈ U
  A∪Aᶜ≈U {A = A} = record { eql = A∪Aᶜ⊆U A , A∪Aᶜ⊇U A }
    where
      A∪Aᶜ⊆U : ∀ {ℓ} {X : Set ℓ} (A : Pred X lzero) → A ∪ A ᶜ ⊆ U
      A∪Aᶜ⊆U A x∈A∪Aᶜ = tt

      A∪Aᶜ⊇U : ∀ {ℓ} {X : Set ℓ} (A : Pred X lzero) → A ∪ A ᶜ ⊇ U
      A∪Aᶜ⊇U A {x} tt = excluded-middle
        where
          postulate
            excluded-middle : ∀ {a} {P : Set a} → P ⊎ ¬ P
```

On the other hand, in standard library,
I found excluded-middle at Relation.Nullary.Negation module.
but, I didn't understand how to use it.

```
excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
```

Please teach me how to apply it in my case.

-- 
----
いとう かつとし
cutsea110 <at> gmail.com
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane