agda / cubical

An experimental library for Cubical Agda

Agda 2

Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.

Documentation

• User manual (per-commit pdf can be downloaded from the github actions page)
• CHANGELOG

Getting Started

• Installation
• Quick guide to editing, type checking and compiling Agda code

Contributing to Agda

• Contribution how-to: HACKING
• Haskell style-guide

cubical's Issues

Naming convention?

I see the definitions' names are in a mess, names like binnat, HitInt are used together .
Should we have a convention for naming? Like following the stdlib directly?

Include clearer installation instructions

Currently the readme talks about making an agda sandbox, but doesn't specify what to do afterwards. For those who aren't so familiar with agda, this isn't completely obvious. Could you add some clearer installation instructions?

Add CI?

I think we can make use of CIs to improve PR process and ensure this library is working under at least a specific revision of Agda (and we update this revision from time to time).

Another question: Travis or Circle?

Feature request: pattern matching on identity path

It would be very nice to have cubical Agda to internally translate pattern matching on refl (with --without-K) to path induction. This would not only make proofs more readable, but also would allow existing Agda developments to migrate seamlessly to cubical Agda.

In particular, I am eager to try my own existing development with cubical Agda. I deliberately designed it so that all "univalent" features are explicit assumptions (univalence, functional extensionality, propositional truncation, and everything).

However, because my developement doesn't use J, I can't just supply such assumptions as data and test the computational behaviour of cubical Agda. Because my codebase has 30k lines, it is not an option to just manually convert all uses of pattern matching on refl to uses of J.

In principle we know the theory to convert the use of pattern matching to eliminators automatically, at least if one uses --exact-split, which I do. Moreover, I take care of making definitions in Agda so that I know that they are more or less directly translatable in an automatic way to Martin-Loef combinators.

It should be possible to translate "well behaved code" that relies on without-K-pattern-matching-on-refl to cubicaltt combinators automatically internally in Agda in a transparent way.

Error running Primitives.agda "Not a valid pattern"

When I run Primitives.agda, I get:

C:\Users\wand\Dropbox\Work\Research\Cubicaltt 2018\cubical-agda\Cubical\Core\Primitives.agda:86,10: Not a valid pattern: i = i0
=<ERROR>
 Set
  sys i (i = i1) = Set

I am running Agda version 2.5.4.1

What am I doing wrong?

The binary conversion inverses question

I asked this yesterday on SO, but I haven't gotten any bites. At this point I think that people who know Cubical Agda and the people who answer Agda questions on SO do not have much overlap so I am passing it here to see if anybody is interested.

The Cubical library is fairly advanced and I would like to see more tutorial material before I try studying it seriously.

Remove stale branches

We have quite a few stale branches in this repo at the moment. Since most of these have been merged or abandoned, can we delete them?

Adding ghcomp and ghfill to the library?

I can think of at least one use case for ghcomp namely the definition of compPath. This definition is judgmentally equal to the current one.

ghcomp : ∀ {ℓ} {A : Set ℓ} {φ : I}
           (u : I → Partial φ A)
           (u0 : Sub A φ (u i0)) → A
ghcomp {φ = φ} u u0 = hcomp {φ = φ ∨ ~ φ}
                            (λ { j (φ = i1) → u j 1=1
                               ; j (φ = i0) → ouc u0} )
                            (ouc u0)

ghfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
           (u : I → Partial φ A)
           (u0 : Sub A φ (u i0))
           ------------------------
           (i : I) → A
ghfill {φ = φ} u u0 i = ghcomp (λ { j (φ = i1) → u (i ∧ j) 1=1
                                  ; j (i = i0) → ouc (u0)})
                               (inc {φ = φ ∨ ~ i} (ouc u0))

compPath : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
compPath p q i = ghcomp {φ = i} (λ j _ → q j) (inc (p i))

fillPath : {A : Set} {x y z : A} (p : x ≡ y) (q : y ≡ z)
         → I → I → A
fillPath {x = x} p q j i = ghfill {φ = i} (λ j _ → q j) (inc (p i)) j

What is the reasoning behind the interval type being non-inductively defined?

I've read that the interval is supposed to be defined on the real line. I find this absolutely mystifying given that its purpose is to map between discrete types in various places.

Add website generated with the HTML backend like the stdlib?

So we can browse this project easier.

BTW I need an admin (like @UlfNorell) to enable gh-pages rendering for this repo.

user-manual and Cubical/Core/README.md are outdated

https://github.com/agda/cubical/blob/master/Cubical/Core/README.md mentions HoTT-UF which does not exist.

This is referred from agda/doc/user-manual/language/cubical, which is likely outdated.

Show that the (already defined) truncations are modalities

as discussed in #134

module dependency circle

I wonder what's the standard practice to solve module dependency circle? Say I have two modules A.agda and B.agda. In A.agda there is

import B
fooA = ...
barA = ...fooB...

while in B.agda there is

import A
fooB = ...fooA...
barB = ...barA...

This makes a dependency circle which agda won't be happy about. The first solution is of course better modulization. But some times it just feel more "right" to split definitions like the above (and I believe there are numerous examples of these). In that case, how do we handle this?

Define truncations as nullification modalities

as discussed in #134

I suppose this issue also includes defining localization and finally showing that the two definitions of truncation are the same.

The color scheme fail to indicate that types don't check

For the following code, the type doesn't check but the color scheme makes it look like checked.

{-# OPTIONS --cubical #-}
open import Cubical.Core.Prelude
open import Cubical.Basics.Nat

Nat-test : ℕ → ℕ
Nat-test 0 = 0
Nat-test (suc n) = suc n

Nat-test-id : (Nat-test ≡ (\ x → x))
Nat-test-id i x = x
-- Nat-test-id i 0 = 0
-- Nat-test-id i (suc n) = suc n

Agda complains
Nat-test x != x of type ℕ when checking the definition of Nat-test-id

But what I got on screen was the following (so the color "checks", type doesn't):

I'm not sure if this is an issue of Agda or Cubical (or simply due to something silly for this particular color scheme, I'm using the default one). But if I do similar things in Agda without --cubical it does complain with color:

---

On a side note, I wish

Nat-test-id : (Nat-test ≡ (\ x → x))
Nat-test-id i x = x

just checks. (Why doesn't it? Just because Nat-test was defined by pattern matching?)

Make the empty system definable

See: https://github.com/agda/cubical/blob/master/Cubical/Core.agda#L88

Help with reversing an application of `sym` to `ua` and `isoToEquiv`

For my master thesis about cubical type theory, I am proving a kind of structure invariance principle for magmas with this library.

At some point in the proof I have the following given:

• A bijection between types: f : ℕ → ℕ₀
• The isomorphism constructed with f: fIso : Iso ℕ ℕ₀
• A function that gives the inverse isomorphism of an isomorphism: invIso : Iso A B → Iso B A

Now, I would like to prove that
sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso))
Is this a valid theorem in HoTT? Are there built-in functions in this library that may help in the proof?

Generate the "Everything" modules directly?

I don't think they should be hand written. We can have a script for that purpose.

Normalizing proof of commutativity +-comm

Normalizing the application of +-comm to cubical numerals fails for relatively low values such as for example in +-comm 4 6. Is this normal expected behaviour? Normalization works for any number when the implementation of the numerals in the standard library is used.

Library structure - follow standard library?

This library seems to be getting a lot of development effort at the moment, and it looks like it's going to develop into a useful base library for those interested in using cubical Agda. I'm not sure how much thought has been put into its layout? I was wondering if you'd considered using the structure of the standard library (where applicable)?

The advantages would be:

1. It would make it far easier for many users to make the switch from non-cubical to cubical Agda (and visa-versa).
2. In the standard library we've already put quite a lot of effort into designing a structure that is reasonably extensible. Adopting it now would hopefully save quite a lot of non-backwards compatible content shuffling later on in this library's life.

Obviously I realise it wouldn't be possible to mimic everything!

Properties for the HITs?

I see there's a lot of HITs, it's good.
Can we have properties for them? Like plus/times assoc/comm?

Non-standard definition of fiber

Most people define the fiber of f : X -> Y by fiber f y = Sigma(x:X), f x = y.

Examples:

• Voevodsky.
• HoTT Book.
• My own UF library.

and probably all HoTT/UF libraries around, in Agda, Coq and Lean.

I suggest that, for the sake of compatibility, we adopt this definition both for the cubical path type, and for the cubical identity type. This involves not only changing the definition but also changing a few proofs/constructions. I haven't checked whether we have the definition of contractibility with the usual conventions yet.

Check whitespace in Makefile

There is a tool in Agda to fix the whitespace issue. The following is the explanation from the tool

Background: Agda was reported to fail to compile on Windows because a file did not end with a newline character (Agda uses -Werror).

If this is still an issue, then this check should be included in the Makefile so that Travis can check it as well.

Unfortunately, I will be unavailable for a few week, so I won't be able to make a PR on this.

Not supporting HIT in dependent type?

In the following code I was trying to define Sphere n as a HIT depending on n. If I do this with S² or S³ it works fine. But it won't check Sphere n if I uncomment cell. In theory this should work, right?

PtType : Set₁
PtType = Σ Set (λ A → A)

Ω1 : PtType → PtType
Ω1 A = ((A .snd) ≡ (A .snd)) , refl

Ω : (n : ℕ) → PtType → PtType
Ω 0 A = A
Ω (suc n) A = Ω1 (Ω n A)

data S² : Set where
  base : S²
  surf : (Ω 2 (S² , base)) .fst

data S³ : Set where
  base : S³
  cell : (Ω 3 (S³ , base)) .fst

data Sphere : ℕ → Set where
  base : (n : ℕ) → Sphere n
  --cell : (n : ℕ) → (Ω n (Sphere n , base n)) .fst

Why bother with Agda.Builtin.Cubical.Id?

The following is a question/comment, rather than a bug report.

As I understand it, Agda.Builtin.Cubical.Id hardwires into
Agda-cubical Andrew Swan's trick for creating an identity type with
definitional computational rule within the cubical sets model of Type
Theory.

Why bother? There is already a perfectly good identity type with
definitional computational rule within Agda, given by
Agda.Builtin.Equality (≡). This can be proved to be path equivalent to
Agda-cubical's path type (here denoted ~ to distinguish it from
≡) -- see the proof
here.

The advantage of ≡ over Id from Agda.Builtin.Cubical.Id is that we
have access to pattern matching on refl.

Add univalence as an explicit definition

There's a comment in Cubical.Core.Glue that it contains a proof of univalence:

Proof of univalence using that unglue is an equivalence (EquivContr)

and then there is a module at the end with

EquivContr : ∀ {ℓ} (A : Set ℓ) → isContr (Σ[ T ∈ Set ℓ ] T ≃ A)

module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
  pathToEquiv : A ≃ B

Do these prove univalence? Do they provide all the kit needed to prove it? I have absolutely no idea. As a regular user, what would be useful is if there was an explicitly spelled out univalence witness:

univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)

One more HIT Int

I was playing with Cubical Agda and got https://gist.github.com/phadej/527ad34e3bed28e5ea3e8cf9d9a2cb79 to work.

data ℤ : Set where
  zero : ℤ
  succ : ℤ → ℤ
  pred : ℤ → ℤ

  succpred : ∀ z → succ (pred z) ≡ z
  predsucc : ∀ z → pred (succ z) ≡ z

  trunc : isSet ℤ

...

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

Should it be included in this library: it demonstrates the truncation problem as mentioned in http://www.cs.nott.ac.uk/~psztxa/talks/bonn18.pdf

Make example definitions private?

I see there're definitions of 1024 in different representations of int/nats, it's good to have them. But they're exposed as a public function, it's not what we expect for a library.

Is it better to make them private?

What does `transp` do when the second argument is i1?

The paper states this about transport.

transport : ∀ {A B : Set} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

This is defined using another primitive of Cubical Agda called transp. It is a generalization of the regular transport principle which lets us specify where the transport is the identity function. In particular, when the second argument to transp is i1 it will reduce to a, which let us prove that transp A r a is always path equal to a (cf. addp later).

So I'd expect something like the following to hold based on that description.

transport : ∀ {A B : Set} → A ≡ B → A → A
transport p a = transp (λ i → p i) i1 a

It gives me a type error. Also, I'd expect the first argument to not matter when the second is i1 since it is stated that it reduces to a in that case, but experimenting I haven't found this to be true. The function is not symmetric in the second argument and playing around, I haven't be able to make it pass typechecking. So what is it supposed to be doing?

Travis couldn't finish

Currently travis didn't finish. Can someone restart?

A better name for `cong`?

I realized that cong is actually function composition on path lambdas. Is it a good idea to rename it into _∘_, which is function composition in the stdlib?

Eliminate all uses of reversals from core library

It would be better if the core library does not rely on reversals so that it is compatible with the simplicial set model

Adding modalities for truncations and other things

One of the things I like about the HoTT-coq library is that truncations are defined as modalities, then many results about truncations come from their more general counter-parts for modalities. it will be a bit of a long project to write a modalities library for cubical agda but I think it could be done. The advantage would be that many results such as Blakers-Massey will end up holding in much greater generality, I have been trying to prove GBMT for a while in HoTT-coq now but there are many technical small lemmas that are needed. It would be very interesting to see if cubical can help.

Another thing I would be interested to see is Bruneries 3x3 lemma in cubical. Showing that pushouts commute with pushouts on a 3x3 square of span rows and columns. This has been proven in the agda library but I struggled to prove it in coq.

ListedFiniteSets: prove equivalence with sorted duplication-free lists

See #110 (review)

Also @L-TChen has developed more about finite sets

https://github.com/L-TChen/FiniteSets/blob/master/FiniteSets/List/Properties.agda#L47

Rename Set to Type

It is rather unfortunate that Agda calls its univereses Set. Renaming it to Type will be much more readable.

1. We need a good way to rename Set into Type.
2. We need to go about replacing all occurrences of Set with Type.

I have no idea how these will be achieved in Agda. Some people discussed possible solutions in #77 so let's collect them here and discuss.

Sign for integers and rationals

I'm hoping to add functions to get the sign of integers (from HitInt) and rationals (for an eventual PR). So far I have this:

{-# OPTIONS --cubical --exact-split #-}

module hello-world where

open import IO
open import Cubical.HITs.HitInt renaming ( Sign to Sign'; sign to sign' )
open import Cubical.HITs.Rational
open import Cubical.Core.PropositionalTruncation
open import Cubical.Core.Everything
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Foundations.Function

data Sign : Set where
  pos neg zero : Sign

sign-ℤ : ℤ → Sign
sign-ℤ (pos zero) = zero
sign-ℤ (pos (suc n)) = pos
sign-ℤ (neg zero) = zero
sign-ℤ (neg (suc n)) = neg
sign-ℤ (posneg i) = zero

sign-ℚ : ℚ → Sign
sign-ℚ (con u a x) = case sign-ℤ u , sign-ℤ a of λ
  { (pos , pos) → pos
  ; (pos , neg) → neg
  ; (neg , pos) → neg
  ; (neg , neg) → pos
  ; (_ , zero) → {!!}
  ; (zero , _) → zero
  }
sign-ℚ (path u a v b x i) = {!!}
sign-ℚ (trunc q q₁ x y i i₁) = {!!}

I am however stuck on how to fill in the holes remaining. I'm still new to CTT. Any help would be appreciated.

Licence?

Unlike the main Agda repository, this one doesn't have a licence file in it. It would probably be a good idea to add one, perhaps similar to the one in the main Agda repository? That one appears to be based on the MIT licence.

The library build fails on Windows 10

PS E:\TheoremProving\CubicalAgdaStuff\cubical> make
cabal exec -- fix-agda-whitespace --check
Warning: The exec command is a part of the legacy v1 style of cabal usage.

Please switch to using either the new project style and the new-exec command
or the legacy v1-exec alias as new-style projects will become the default in
the next version of cabal-install. Please file a bug if you cannot replicate a
working v1- use case with the new-style commands.

For more information, see: https://wiki.haskell.org/Cabal/NewBuild

cabal: The program 'fix-agda-whitespace' is required but it could not be
found.

make: *** [GNUmakefile:11: check-whitespace] Error 1

I know that make which I got through Chocolatey works as I needed to use it for Proof General + Coq. I tried cabal install fix-agda-whitespace, but am getting nothing.

Also I get a type error when I try to typecheck the Cubical.Core.Primitives file.

E:\TheoremProving\CubicalAgdaStuff\cubical\Cubical\Core\Primitives.agda:193,3-196,16
A (i ∧ i0) → A (i ∧ i1) !=< A i of type
Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1)))
when checking that the inferred type of an application
  A (i ∧ i0) → A (i ∧ i1)
matches the expected type
  A i

This is for ...

-- Heterogeneous filling defined using comp
fill : (A : ∀ i → Type (ℓ′ i))
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i
fill A {φ = φ} u u0 i =
  comp (λ j → A (i ∧ j))
       (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                ; (i = i0) → outS u0 })
       (outS u0)

I do not think this error is related to the build failure which makes it that much more puzzling. I got Agda 2.6.0.1 just now. Should I try going back to 2.6.0?

Cubical.Core.Glue is broken now

agda/agda@13d516f

Cubical discussion forum

I'll open this "issue" as a place to discuss various cubical things, like "how to prove X cubically", as suggested by @3abc .

Let me open up with two questions that came up in agda/agda#3599.

1. Give a direct cubical proof that:

transport p ≡ transport q → p ≡ q

2. Is there a more direct proof of

https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda#L104

A slick proof that transport is an equivalence is the following:

isEquivTransport : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → isEquiv (transport p)
isEquivTransport {A = A} {B = B} p =
  transport (λ i → isEquiv (λ x → transp (λ j → p (i ∧ j)) (~ i) x)) (idIsEquiv A)

transportEquiv : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A ≃ B
transportEquiv p = (transport p , isEquivTransport p)

What's going on in pathToEquiv is very similar, but I can't figure out how to get an analogous proof to typecheck... Any ideas? @Saizan

3x3 via symmetric double pushout

I wonder if we can make the proof of the 3x3 lemma for pushouts shorter in the following way:

Given the 3x3 commutative diagram, we can encode this data as 4 types (the corners), 4 type families indexed by types on the edge (the edges) and finally a type family over the total spaces of the four type families (the middle).

It is easy to show that the 4 homotopies witnessing the commutativity of the diagram can also be recovered from this "type theoretric" encoding of a 3x3 diagram. You can get the original 3x3 by looking at the total spaces of the families and the original maps become the projection maps.

Now from this consider the HIT with 4 point constructors for each of the 4 corner types. 4 path constructors making sure that coming from the middle of an edge through a corner agrees and finally a square constructor for these 4 paths.

Now the idea is that it should be simpler to show that a double pushout is equivalent to this symmetric double pushout HIT. Which you can do both ways.

I tried to formalise this in coq earlier this year, but the path algebra got a bit heavy for me. Seeing the success of the Torus, I expect this to work easily.

This was originally Mike Shulmans idea.

Here is the following coq code you can use as pseudocode:

 Section Push.
    Context
      {A00 A10 A01 A11 : Type}
      {A0x : A00 -> A01 -> Type}
      {A1x : A10 -> A11 -> Type}
      {Ax0 : A00 -> A10 -> Type}
      {Ax1 : A01 -> A11 -> Type}
      (Axx : forall a00 a01 a10 a11,
        A0x a00 a01 ->
        A1x a10 a11 ->
        Ax0 a00 a10 ->
        Ax1 a01 a11 -> Type).

  Local Definition B00 := A00.
  Local Definition B10 := A10.
  Local Definition B01 := A01.
  Local Definition B11 := A11.

  Local Definition B0x := {a00 : A00 & {a01 : A01 & A0x a00 a01}}.
  Local Definition B1x := {a10 : A10 & {a11 : A11 & A1x a10 a11}}.
  Local Definition Bx0 := {a00 : A00 & {a10 : A10 & Ax0 a00 a10}}.
  Local Definition Bx1 := {a01 : A01 & {a11 : A11 & Ax1 a01 a11}}.

  Local Definition Bxx := {a00 : A00 & {a01 : A01 & {a10 : A10 & {a11 : A11 &
             {a0x : A0x a00 a01 & {a1x : A1x a10 a11 &
             {ax0 : Ax0 a00 a10 & {ax1 : Ax1 a01 a11 &
              Axx a00 a01 a10 a11 a0x a1x ax0 ax1}}}}}}}}.

  Local Definition fi0 : Bx0 -> B00 := pr1.
  Local Definition fj0 : Bx0 -> B10 := fun x => pr1 (pr2 x).

  Local Definition f'ix : Bxx -> B0x := fun a => (a.1; a.2.1; a.2.2.2.2.1).
  Local Definition fjx : Bxx -> B1x := fun a => (a.2.2.1; a.2.2.2.1; a.2.2.2.2.2.1).

  Local Definition fi1 : Bx1 -> B01 := pr1.
  Local Definition fj1 : Bx1 -> B11 := fun x => pr1 (pr2 x).
  
  Local Definition f0i : B0x -> B00 := pr1.
  Local Definition f0j : B0x -> B01 := fun x => pr1 (pr2 x).
  
  Local Definition fxi : Bxx -> Bx0 := fun a => (a.1; a.2.2.1; a.2.2.2.2.2.2.1).
  Local Definition fxj : Bxx -> Bx1 := fun a => (a.2.1; a.2.2.2.1; a.2.2.2.2.2.2.2.1).

  Local Definition f1i : B1x -> B10 := pr1.
  Local Definition f1j : B1x -> B11 := fun x => pr1 (pr2 x).

    Private Inductive SymP :=
      | a : B00 -> SymP
      | b : B10 -> SymP
      | c : B01 -> SymP
      | d : B11 -> SymP.

    Axiom H1 : a o f0i == c o f0j.
    Axiom H2 : a o fi0 == b o fj0.
    Axiom H3 : c o fi1 == d o fj1.
    Axiom H4 : b o f1i == d o f1j.

    Axiom sq 
      : forall x,
        Square (H1 (f'ix x)) (H4 (fjx x)) (H2 (fxi x)) (H3 (fxj x)).

Cubical.Core.Glue is broken

After the commit agda/agda@13d516f, Cubical.Core.Glue isn't working anymore. Here is the error message:

unglueIsEquiv A (~ i0 ∨ i0)
(λ { (i0 = i0) → A , idEquiv A ; (i0 = i1) → w })
!= idIsEquiv A of type isEquiv (unglue (~ i0 ∨ i0))
when checking that the expression
λ i →
  let f : PartialP (~ i ∨ i) (λ x → Σ-syntax (Set ℓ) λ T → T ≃ A)
      f = λ { (i = i0) → A , idEquiv A ; (i = i1) → w }
  in Glue A f , unglueEquiv _ _ f
has type (A , idEquiv A) ≡ w

How are cubical subtypes supposed to be used?

_[_↦_] : ∀ {ℓ} (A : Set ℓ) (φ : I) (u : Partial φ A) → Setω
A [ φ ↦ u ] = Sub A φ u

There is just too little information in the documentation on how to use these or what are their purpose. Because Sub is built in, I can't gleam anything from it.

inc : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : A) → A [ φ ↦ (λ _ → u) ]
ouc : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A

Also these two do not seem to be in the library. Are they supposed to be builtins or is it possible to define them?

master incompatible with Agda-2.6.0

I checked out the master branch and ran make. GHC 8.0.2 and Agda 2.6.0. Error:
agda Cubical/Core/Everything.agda Checking Cubical.Core.Everything (/Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Everything.agda). Checking Cubical.Core.Primitives (/Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Primitives.agda). /Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Primitives.agda:193,3-196,16 A (i ∧ i0) → A (i ∧ i1) !=< A i of type Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1))) when checking that the inferred type of an application A (i ∧ i0) → A (i ∧ i1) matches the expected type A i make: *** [check] Error 1

Cubical.Data.Rational: define operations and equivalence with HoTT def.

Right now Cubical.Data.Rational only contains the datatype.

Arithmetic is there to be implemented!

The Book defines rationals as the set quotient Z x N / ~ where
(a, b) ~ (c, d) iff a(d + 1) = c(b + 1)
and it would be good to provide an equivalence.

Typo in HLevels.agda

cubical/Cubical/Foundations/HLevels.agda

Lines 28 to 34 in 27ec388

	private
	variable
	ℓ ℓ' : Level
	A : Type ℓ
	B : A → Type ℓ
	x y : A
	n : ℕ

Has

B : A → Type ℓ

should it rather be

B : A → Type ℓ' -- primed

Clean up and make Cubical.Foundations.Logic universe polymorphic

The file https://github.com/agda/cubical/blob/master/Cubical/Foundations/Logic.agda should be made universe polymorphic and Ω should be removed in favour of hProp

Bugs in transp

@Saizan : There are some issues with transp:

https://github.com/agda/cubical/blob/master/Cubical/Basics/Int.agda#L50

Make use of the generalization feature?

Now, with variable keyword, codes like

f0 : forall {i} {A : Set i} -> blabla
f1 : forall {i} {A : Set i} -> blabla

can be replaced with

variable
  i : Level
  A : Set i
f0 : blabla
f1 : blabla

which makes the code more readable.

Modify the Core library to reflect the documentation and update README

There will soon be some proper documentation for Cubical Agda (agda/agda#3571). Once this has been merged I plan to shrink the core a bit (some parts are just there as documentation and have now been incorporated into the proper documentation) and update the README so that it reflects what is actually in the library.