871 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
3
votes
0
answers
53
views
Defining Sets with extra structure and homomorphisms
suppose
Structure : (M : Type l -> Type l) -> Type (lsuc l)
Structure M = Σ (Type l) (λ A -> M A)
I want
homomorphism :
{M : Type l -> Type l} -> (sA sB : Structure M)
(f : sA.fst -...
0
votes
1
answer
54
views
Replacing a function by this definition
I have this code in Agda:
tm-sim : TM → Term
tm-sim tm = (G tm) · (G tm)
refl-clos-sim : ∀(tm : TM) → ∀ (l1 l2 : List (Fin (suc (tm-Symbols tm)))) →
tm-sim tm · Config2ƛ {tm} ⟨ l1 ! ...
2
votes
2
answers
80
views
Pattern matching without K in agda
I was trying to prove K (with without-K) using J to see what goes wrong when we try to do that.
That's all well and good, but in the process of playing around I noticed that agda refuses to match with ...
0
votes
1
answer
46
views
Inference issues with implicit parameters to lambdas in Agda
If you write the following definition:
f : {N} → N
f = λ {n} → n
You'll get the following error:
error: [UnequalTerms]
{n : _210} → _210 !=< N
when checking that the expression λ {n} → n has type ...
0
votes
1
answer
102
views
Example of terminating program that cannot be written in safe Agda
In Agda with --safe, it is impossible to write a nonterminating program. Acknowledging the halting problem, it follows that there are terminating programs that cannot be written in safe Agda. But I ...
2
votes
1
answer
59
views
Returning the type of a constructor by a function
I am trying to write a simple tuple type
open import Agda.Builtin.List
mutual
f : List Set -> Set
f T = g T T where
g : List Set -> List Set -> Set
g [] T = Tuple T
g (t ∷ ...
1
vote
0
answers
56
views
How to tell a function to take nonzero natural number as an argument?
My function lessen didn't have the requirement that the argument had to be non-zero at first, so it didn't work:
isHamming : Int -> Bool
isHamming what = lessen what 2 where
lessen : (dividend :...
1
vote
1
answer
57
views
Providing strict total ordering for pair type
I'm trying to generate some haskell from agda using agda2hs. In this code snippet I define some agda fields that will generate some haskell typeclasses.
open import Haskell.Prelude
open import Data....
0
votes
0
answers
29
views
Agda: Proving that the dependent recursion property of free loops implies the universal property of the circle
I am trying to define the induction principle of the circle S1 and prove properties with it along the chapter 6 of the HoTT book. The original difficulty is that the HoTT book uses judgmental ...
2
votes
1
answer
58
views
Agda: how to prove lemma 4.2.5 in HoTT book
there is a small lemma in the HoTT book
lemma-4-2-5 : ∀ {n m : Level} {A : Set n} {B : Set m} {f : A → B} {y : B} {(⟨ x , p ⟩) (⟨ x' , p' ⟩) : fiber-map f y}
→ (⟨ x , p ⟩ ≡ ⟨ x' , p' ⟩) ≃...
0
votes
1
answer
48
views
Agda: cannot instantiate metavariable
I'm fairly new to Agda and I'm trying to construct the Interval's lattice. So far I've defined the Lattice datatype as follows:
data I : Set where
⊤ : I
⊥ : I
-∞ : Z → I
_+∞ : Z → I
I : ...
1
vote
1
answer
56
views
Agda: is there a way to use the information provided by with-abstraction in the function definition?
I'm trying to construct the lattice of intervals with the datatype defined as follows:
data I : Set where
⊤ : I
⊥ : I
-∞ : Z → I
_+∞ : Z → I
I : (l : Z) → (u : Z) → {l ≤ u} → I
...
2
votes
1
answer
62
views
How to prove in Agda that every equivalence in the type 𝟚 is either id or a permutation?
I would like to prove in Agda that every equivalence of the type 2 is either the identity, or the permutation of two elements.
2-equivalences-characterization: ∀ (f : 2 ≃ 2) → ((proj1 f) ≡ id) ⊎ ...
8
votes
4
answers
417
views
Can I write a dependent left fold in terms of a dependent right fold?
Suppose we have
data Nat = Z | S Nat
type Vec :: Nat -> Type -> Type
data Vec n a where
Nil :: Vec Z a
(:::) :: Vec n a -> Vec (S n) a
infixr 4 :::
deriving instance Foldable (Vec n)
...
1
vote
0
answers
52
views
Agda : what is the difference between using braces or not in a lambda expression?
what's the difference between the lambda expression
λ {(tr u) → refl}
and without braces,
λ (tr u) → refl
I noticed that using one or the other causes an error.
While proving lemman 3.9.1 of the ...