MarcelineVQ

module Foo where

{-

https://arxiv.org/pdf/1912.10642.pdf

I'd like to learn categroy theory finally.
To this end I'm going to show it.

Ultimately I'd like to reconcile it with homotopy and make use

MarcelineVQ

module _ where
  open import Data.Nat
  open import Data.Bool
  open import Relation.Binary.PropositionalEquality
   
  data Tree : Set where
      Leaf : Tree
      Node : Tree -> Tree -> ℕ -> Tree
   

MarcelineVQ

foo : (m : Nat) -> (n : Nat) -> Dec (LT m n)
foo Z Z = No absurd
foo Z (S k) = Yes (LTESucc LTEZero)
foo (S k) Z = No absurd
foo (S k) (S j) = case foo k j of
                    (Yes prf) => Yes (LTESucc prf)
                    (No contra) => No (\(LTESucc r) => contra r)

foo2 : (m : Nat) -> (n : Nat) -> Dec (LT m n)

MarcelineVQ

emptyOnsenM : OnsenM ()

namespace AttribElem {
elem : String -> List Char -> OnsenM a -> OnsenM a
}
namespace Elem {
elem : String -> OnsenM a -> OnsenM a
}

-- ^ above is solely to avoid writing []

MarcelineVQ

data ExactlyOne {A : Set} : (xs : List A) → Set where
  TheOne : ∀ {x} → ExactlyOne (x ∷ [])

exactlyOne : ∀ {a} → (xs : List a) → Dec (ExactlyOne xs)
exactlyOne [] = no (λ ())
exactlyOne (x ∷ []) = yes TheOne
exactlyOne (x ∷ y ∷ xs) = no λ ()

MarcelineVQ

    { to = λ ¬[a⊎b] → (λ a → inj₁ a ↯ ¬[a⊎b])
                    , (λ b → inj₂ b ↯ ¬[a⊎b])

MarcelineVQ

module ≤-Reasoning where
  open import plfa.part1.Relations using (_≤_;≤-trans;s≤s;z≤n;≤-refl)
  open import Data.Nat hiding (_≤_)
  open import Data.Nat.Properties using (+-comm;+-suc)
  
  infix  1 begin_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_
  infix  3 _∎

MarcelineVQ

module plfa.part1.Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where

MarcelineVQ

-- working idris version, uses record accesors for Ext to skip casing the container.
record Container where
  constructor MkC
  shape : Type
  position : shape -> Type

Ext : Container -> Type -> Type
Ext c a = (v : shape c ** position c v -> a)

mapE : (a -> b) -> Ext c a -> Ext c b

MarcelineVQ

data Eventually_s : {p : a -> Type} -> Stream a -> Type where
  Ev_b : p x -> Eventually_s {p} (x :: xs)
  Ev_r : Not (p x) -> Eventually_s {p} xs -> Eventually_s {p} (x :: xs)

eventually_s_inv : Eventually_s {p} s -> s = x :: s' -> Not (p x) -> Eventually_s {p} s'
eventually_s_inv (Ev_b z) Refl y = void $ y z
eventually_s_inv (Ev_r f x) Refl y = x