Re: [Agda] What is wrong about this proof for A ⊆ A ∪ B

[Katsutoshi Itoh]

Hi Andreas.

> Just a short in the dark:  I would guess that Agda cannot infer the universe > levels for A and B, so you should write

I got it, and I modified my code as below.

```
  A⊆A∪B : ∀ {ℓ₀ ℓ₁ ℓ} {X : Set ℓ} (A : Pred X ℓ₀) → (B : Pred X ℓ₁) → A ⊆ A ∪ B
  A⊆A∪B x∈A B x = inj₁ x
```
This code works perfectly, so there are no any warnings.

Thanks.


2016-06-15 17:52 GMT+09:00 Andreas Abel <abela at chalmers.se>:
> This works:
>
>   A⊆A∪B' : ∀ {ℓ₀ ℓ₁} {X : Set ℓ₀} {A B : Pred X ℓ₁} → A ⊆ A ∪ B
>   A⊆A∪B' x∈A = inj₁ x∈A
>
> On 15.06.2016 02:31, Katsutoshi Itoh wrote:
>>
>> Hi all.
>>
>> I'm studying sets theory by using agda(2.5.1).
>> Now, I've proved a theorem A ⊆ A ∪ B by 2 kind of solutions,
>> and I get warnings(yellow highlight) occured around both codes,
>> But I couldn't understand what's happen.
>> Please teach me what is wrong about these?
>>
>> ```
>>    A⊆A∪B : ∀ A B → A ⊆ A ∪ B
>
>
> Just a short in the dark:  I would guess that Agda cannot infer the universe
> levels for A and B, so you should write
>
>   (A B : FILLMEIN) -> A \subseteq A \cup B
>
> instead.
>
>>    A⊆A∪B x∈A B x = inj₁ x
>>
>>    A⊆A∪B' : ∀ {ℓ₀ ℓ₁ X} {A : Pred X ℓ₀} {B : Pred X ℓ₁} → A ⊆ A ∪ B
>>    A⊆A∪B' x∈A = inj₁ x∈A
>> ```
>>
>> I attach all my program file.
>>
>> Regards.
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/



-- 
----
いとう かつとし
cutsea110 at gmail.com