­jonoodle­ @ionchy@types.pl

Is it possible to define a mutual inductive type and coinductive type in Coq? I can do this in Agda by putting the declarations at the top but Coq only seems to have with

It's like a little logic puzzle and I got sniped

I need to stop

If you interpret r, s, t, u as sets (might as well), then ⊳ is some sort of pointwise order (every element of r is greater than every element of s), and ⊏ (not <, oops) is the subset relation
Axiom 4 says that if r is pointwise greater than s and u is a subset of s, then r is pointwise greater than u, which makes sense
Axiom 5 says that there is a set r s.t. if there is a set pointwise smaller than z, then z is a subset of r
Personally I think ax5 isn't independent of ax1 and ax4
I bet Axiom 5 could be proven from the other axioms
I bet I can find a shorter proof

Looks like there's two relations, _ ⊳ _ and _ < _
The first is meant to be some sort of order and the second one is some sort of subtyping relation

Definitions:

• S r ≡ r ⊳ r
• C r ≡ ∃s. r ⊳ s
• O r ≡ ∀s. r ⊳ s

Axioms:

• ax1: ∀r. ∃v. v ⊳ r
• ax2: ∀r. ∀s. ∀t. (r ⊳ s) → (s ⊳ t) → (r ⊳ t)
• ax3: ∀r. ∀s. (r ⊳ s) → (s ⊳ r) → r = s
• ax4: ∀r. ∀s. (r ⊳ s) → (u < s) → r ⊳ u
• ax5: ∃r. ∀z. C z → z < r, i.e. ∃r. ∀z. ∃s. z ⊳ s → z < r

Let's see... ax1 says that there always exists a greater element, ax2 is transitivity, ax3 is antisymmetry, and ax4 and ax5... well I can't tell what < is meant to be
In any case the G theorem just says that there's a unique maximal element that's reflexive under ⊳

Anyway, and is and, or is or, nor is nor, so is implication, for is inverse implication, and yet is like the inverse of but

They're all coordinating conjunctions but it doesn't seem like for or so could be used to coordinate anything but independent clauses, i.e. not noun phrases

In school we learned about FANBOYS:
For
And
Nor
But
Or
Yet
So

Might unironically listen to an 80s playlist https://www.youtube.com/playlist?list=PLahKLy8pQdCM0SiXNn3EfGIXX19QGzUG3

In contrast, a well-founded data type like [Integer] lives entirely in the moment.

McBride writes the funniest sentences

Okay people like this

But maybe you should ask yourself why you see what-you-don't-want-to-see in something that has never been related to what-you-don't-want-to-see...
(If the shape of the Coq logo makes you think to what-you-don't-want-to-see, maybe it's time to go to the doctor...?)

People like this annoy me so much

"It type checks but I have no idea what it means" is my slogan right now

They're doing the "yeah I agree" reply-all email chain on the Coq mailing list about Coq sounding like "cock" and the logo looking like a beige cock

There's no good way of pronouncing Coq anyway
Say it in English and it sounds like cock
Say it in French and it sounds like cuck