text:
{-# OPTIONS --without-K #-}

module Lecture5 where

open import Lecture4 public

-- Section 5.1 Homotopies
_~_ : {i j : Level} {A : UU i} {B : A → UU j} (f g : (x : A) → B x) → UU (i ⊔ j)
f ~ g = (x : _) → Id (f x) (g x)

htpy-refl : {i j : Level} {A : UU i} {B : A → UU j} (f : (x : A) → B x) → f ~ f
htpy-refl f x = refl

htpy-inv : {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} → (f ~ g) → (g ~ f)
htpy-inv H x = inv (H x)

htpy-concat : {i j : Level} {A : UU i} {B : A → UU j} {f : (x : A) → B x} (g : (x : A) → B x) {h : (x : A) → B x} → (f ~ g) → (g ~ h) → (f ~ h)
htpy-concat g H K x = concat _ (H x) (K x)

htpy-assoc : {i j : Level} {A : UU i} {B : A → UU j} {f g h k : (x : A) → B x} → (H : f ~ g) → (K : g ~ h) → (L : h ~ k) → htpy-concat _ H (htpy-concat _ K L) ~ htpy-concat _ (htpy-concat _ H K) L
htpy-assoc H K L x = assoc (H x) (K x) (L x)

htpy-left-unit : {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} (H : f ~ g) → (htpy-concat _ (htpy-refl f) H) ~ H
htpy-left-unit H x = left-unit (H x)

htpy-right-unit : {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} (H : f ~ g) → (htpy-concat _ H (htpy-refl g)) ~ H
htpy-right-unit H x = right-unit (H x)

htpy-left-inv : {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} (H : f ~ g) → htpy-concat _ (htpy-inv H) H ~ htpy-refl g
htpy-left-inv H x = left-inv (H x)

htpy-right-inv : {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} (H : f ~ g) → htpy-concat _ H (htpy-inv H) ~ htpy-refl f
htpy-right-inv H x = right-inv (H x)

htpy-left-whisk : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} (h : B → C) {f g : A → B} → (f ~ g) → ((h ∘ f) ~ (h ∘ g))
htpy-left-whisk h H x = ap h (H x)

htpy-right-whisk : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} {g h : B → C} (H : g ~ h) (f : A → B) → ((g ∘ f) ~ (h ∘ f))
htpy-right-whisk H f x = H (f x)

-- Section 5.2 Bi-invertible maps
sec : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
sec {_} {_} {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ~ id)

retr : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
retr {_} {_} {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ~ id)

_retract-of_ : {i j : Level} → UU i → UU j → UU (i ⊔ j)
A retract-of B = Σ (A → B) retr

is-equiv : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-equiv f = sec f × retr f

-- this equivalence symbol is \simeq
_≃_ : {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
A ≃ B = Σ (A → B) (λ f → is-equiv f)

eqv-sec : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → sec f
eqv-sec e = pr1 e

eqv-secf : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → B → A
eqv-secf e = pr1 (eqv-sec e)

eqv-sech : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → (e : is-equiv f) → ((f ∘ eqv-secf e) ~ id)
eqv-sech e = pr2 (eqv-sec e)

eqv-retr : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → retr f
eqv-retr e = pr2 e

eqv-retrf : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → B → A
eqv-retrf e = pr1 (eqv-retr e)

eqv-retrh : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → (e : is-equiv f) → (((eqv-retrf e) ∘ f) ~ id)
eqv-retrh e = pr2 (eqv-retr e)

is-invertible : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-invertible {_} {_} {A} {B} f = Σ (B → A) (λ g → ((f ∘ g) ~ id) × ((g ∘ f) ~ id))

is-equiv-is-invertible : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-invertible f → is-equiv f
is-equiv-is-invertible (dpair g (dpair H K)) = pair (dpair g H) (dpair g K)

htpy-secf-retrf : {i j : Level} {A : UU i} {B : UU j} {f : A → B} (e : is-equiv f) → (eqv-secf e ~ eqv-retrf e)
htpy-secf-retrf {_} {_} {_} {_} {f} (dpair (dpair g issec) (dpair h isretr)) =
  htpy-concat (h ∘ (f ∘ g)) (htpy-inv (htpy-right-whisk isretr g)) (htpy-left-whisk h issec)

is-invertible-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → is-invertible f
is-invertible-is-equiv {_} {_} {_} {_} {f} (dpair (dpair g issec) (dpair h isretr)) = dpair g (pair issec (htpy-concat (h ∘ f) (htpy-right-whisk (htpy-secf-retrf (dpair (dpair g issec) (dpair h isretr))) f) isretr))

inv-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → B → A
inv-is-equiv E = pr1 (is-invertible-is-equiv E)

issec-inv-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → (E : is-equiv f) → (f ∘ (inv-is-equiv E)) ~ id
issec-inv-is-equiv E = pr1 (pr2 (is-invertible-is-equiv E))

isretr-inv-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → (E : is-equiv f) → ((inv-is-equiv E) ∘ f) ~ id
isretr-inv-is-equiv E = pr2 (pr2 (is-invertible-is-equiv E))

is-equiv-inv-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} → (E : is-equiv f) → is-equiv (inv-is-equiv E)
is-equiv-inv-is-equiv {_} {_} {_} {_} {f} E =
  pair (dpair f (isretr-inv-is-equiv E)) (dpair f (issec-inv-is-equiv E))

is-equiv-id : {i : Level} (A : UU i) → is-equiv (id {_} {A})
is-equiv-id A = pair (dpair id (htpy-refl id)) (dpair id (htpy-refl id))

inv-Pi-swap : {i j k : Level} {A : UU i} {B : UU j} (C : A → B → UU k) →
  ((y : B) (x : A) → C x y) → ((x : A) (y : B) → C x y)
inv-Pi-swap C g x y = g y x

is-equiv-swap : {i j k : Level} {A : UU i} {B : UU j} (C : A → B → UU k) → is-equiv (Pi-swap {_} {_} {_} {A} {B} {C})
is-equiv-swap C = pair (dpair (inv-Pi-swap C) (htpy-refl id)) (dpair (inv-Pi-swap C) (htpy-refl id))

-- Section 5.3 The identity type of a Σ-type

eq-pair' : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → (Σ (Id (pr1 s) (pr1 t)) (λ α → Id (tr B α (pr2 s)) (pr2 t))) → Id s t
eq-pair' (dpair x y) (dpair x' y') (dpair refl refl) = refl

eq-pair : {i j : Level} {A : UU i} {B : A → UU j} {s t : Σ A B} → (Σ (Id (pr1 s) (pr1 t)) (λ α → Id (tr B α (pr2 s)) (pr2 t))) → Id s t
eq-pair {i} {j} {A} {B} {s} {t} = eq-pair' s t

pair-eq' : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → (Id s t) → Σ (Id (pr1 s) (pr1 t)) (λ α → Id (tr B α (pr2 s)) (pr2 t))
pair-eq' s t refl = dpair refl refl

pair-eq  : {i j : Level} {A : UU i} {B : A → UU j} {s t : Σ A B} → (Id s t) → Σ (Id (pr1 s) (pr1 t)) (λ α → Id (tr B α (pr2 s)) (pr2 t))
pair-eq {i} {j} {A} {B} {s} {t} = pair-eq' s t

isretr-pair-eq : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → (((pair-eq' s t) ∘ (eq-pair' s t)) ~ id)
isretr-pair-eq (dpair x y) (dpair x' y') (dpair refl refl) = refl

issec-pair-eq : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → (((eq-pair' s t) ∘ (pair-eq' s t)) ~ id)
issec-pair-eq (dpair x y) .(dpair x y) refl = refl

is-equiv-eq-pair' : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → is-equiv (eq-pair' s t)
is-equiv-eq-pair' s t = pair (dpair (pair-eq' s t) (issec-pair-eq s t)) (dpair (pair-eq' s t) (isretr-pair-eq s t))

is-equiv-eq-pair : {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → is-equiv (eq-pair {i} {j} {A} {B} {s} {t})
is-equiv-eq-pair = is-equiv-eq-pair'

-- Exercises below

-- Exercise 5.1

singleton-ind-const-htpy : {i : Level} {A : UU i} (a : A) → (const 𝟙 A a) ~ (ind-unit a)
singleton-ind-const-htpy a star = refl

-- Exercise 5.2
ap-const-is-const-refl : {i j : Level} {A : UU i} {B : UU j} (b : B) {x y : A} → (ap (const A B b)) ~ (const (Id x y) (Id b b) refl)
ap-const-is-const-refl b refl = refl

-- Exercise 5.3
inv-inv-htpy : {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (inv (inv p)) p
inv-inv-htpy refl = refl

is-equiv-inv : {i : Level} {A : UU i} (x y : A) →
  is-equiv (λ (p : Id x y) → inv p)
is-equiv-inv x y = pair (dpair inv inv-inv-htpy) (dpair inv inv-inv-htpy)

concat-inv-left-htpy : {i : Level} {A : UU i} {x y z : A} (p : Id x y) → (q : Id y z) → Id ((inv p) · (p · q)) q
concat-inv-left-htpy refl q = refl

concat-inv-right-htpy : {i : Level} {A : UU i} {x y z : A} (p : Id x y) → (r : Id x z) → Id (p · ((inv p) · r)) r
concat-inv-right-htpy refl r = refl

is-equiv-concat : {i : Level} {A : UU i} (x y z : A) (p : Id x y) → (is-equiv λ (q : Id y z) → p · q)
is-equiv-concat x y z p = pair (dpair (λ (r : Id x z) → ((inv p) · r)) (λ (r : Id x z) → concat-inv-right-htpy p r)) (dpair (λ (r : Id x z) → (inv p) · r) (λ (q : Id y z) → concat-inv-left-htpy p q))

tr-inv-htpy : {i j : Level} {A : UU i} {B : A → UU j} {x y : A} (p : Id x y) (b : B x) → Id (tr B (inv p) (tr B p b)) b
tr-inv-htpy refl b = refl

tr-inv-htpy' : {i j : Level} {A : UU i} {B : A → UU j} {x y : A} (p : Id x y) (b : B y) → Id (tr B p (tr B (inv p) b)) b
tr-inv-htpy' refl b = refl

is-equiv-tr : {i j : Level} {A : UU i} (B : A → UU j) {x y : A} (p : Id x y) → is-equiv (λ b → (tr B p b))
is-equiv-tr B p = pair (dpair (tr B (inv p)) (tr-inv-htpy' p)) (dpair (tr B (inv p)) (tr-inv-htpy p))

-- Exercise 5.4
is-equiv-htpy : {i j : Level} {A : UU i} {B : UU j} {f g : A → B} →
  f ~ g → is-equiv g → is-equiv f
is-equiv-htpy H (dpair (dpair gs issec) (dpair gr isretr)) =
  pair
    (dpair gs (htpy-concat _ (htpy-right-whisk H gs) issec))
    (dpair gr (htpy-concat (gr ∘ _) (htpy-left-whisk gr H) isretr))

-- Exercise 5.5
is-equiv-comp : {i j k : Level} {A : UU i} {B : UU j} {X : UU k} {f : A → X} {g : B → X} {h : A → B} (H : f ~ (g ∘ h)) → is-equiv h → is-equiv g → is-equiv f
is-equiv-comp {i} {j} {k} {A} {B} {X} {f} {g} {h} H (dpair (dpair hs hs-issec) (dpair hr hr-isretr))
  (dpair (dpair gs gs-issec) (dpair gr gr-isretr)) =
  is-equiv-htpy H
    (pair
      (dpair (hs ∘ gs)
        (htpy-concat (g ∘ gs)
          (htpy-left-whisk g (htpy-right-whisk hs-issec gs)) gs-issec))
      (dpair (hr ∘ gr)
        (htpy-concat (hr ∘ h)
          (htpy-left-whisk hr (htpy-right-whisk gr-isretr h)) hr-isretr)))

-- Exercise 5.6
not-not-x-is-x : (x : bool) → Id (not (not x)) x
not-not-x-is-x true = refl
not-not-x-is-x false = refl

is-equiv-not : is-equiv not
is-equiv-not = pair (dpair not not-not-x-is-x) (dpair not not-not-x-is-x)

path-true-to-false-is-contra : (Id true false) → 𝟘
path-true-to-false-is-contra p = tr (ind-bool 𝟙 𝟘) p star

same-image-not-equiv : (f : bool → bool) → (p : Id (f true) (f false)) → (is-equiv f) → 𝟘
same-image-not-equiv f p (dpair f-is-sec (dpair g htpy)) = path-true-to-false-is-contra (true ==⟨ inv (htpy true) ⟩ g(f(true)) ==⟨ (ap g p) ⟩ g(f(false)) ==⟨ htpy false ⟩ false ==∎)
-- NOTE: ap g p is a path from g(f(true)) to g(f(false))

-- Exercise 5.7
zpred-zsucc-x-is-x : (x : ℤ) → Id (Zpred (Zsucc x)) x
zpred-zsucc-x-is-x (inl Nzero) = refl
zpred-zsucc-x-is-x (inl (Nsucc x)) = refl
zpred-zsucc-x-is-x (inr (inl star)) = refl
zpred-zsucc-x-is-x (inr (inr x)) = refl

zsucc-zpred-x-is-x : (x : ℤ) → Id (Zsucc (Zpred x)) x
zsucc-zpred-x-is-x (inl x) = refl
zsucc-zpred-x-is-x (inr (inl star)) = refl
zsucc-zpred-x-is-x (inr (inr Nzero)) = refl
zsucc-zpred-x-is-x (inr (inr (Nsucc x))) = refl

is-equiv-zsucc : is-equiv Zsucc
is-equiv-zsucc = dpair (dpair Zpred zsucc-zpred-x-is-x) (dpair Zpred zpred-zsucc-x-is-x)

-- Exercise 5.8
-- construct equivalences A + B <-> B + A and A x B <-> B x A
coprod-rev : {i j : Level} (A : UU i) (B : UU j) → (coprod A B) → (coprod B A)
coprod-rev A B (inl a) = inr a
coprod-rev A B (inr b) = inl b

coprod-rev-squared-is-id : {i j : Level} (A : UU i) (B : UU j) → (coprod-rev B A ∘ coprod-rev A B) ~ id
coprod-rev-squared-is-id A B (inl a) = refl
coprod-rev-squared-is-id A B (inr b) = refl

is-equiv-coprod-rev : {i j : Level} (A : UU i) (B : UU j) → is-equiv (coprod-rev A B)
is-equiv-coprod-rev A B = dpair (dpair (coprod-rev B A) (coprod-rev-squared-is-id B A)) (dpair (coprod-rev B A) (coprod-rev-squared-is-id A B))

prod-rev : {i j : Level} (A : UU i) (B : UU j) → (prod A B) → (prod B A)
prod-rev A B x = pair (pr2 x) (pr1 x)

prod-rev-squared-is-id : {i j : Level} (A : UU i) (B : UU j) → (prod-rev B A ∘ prod-rev A B) ~ id
prod-rev-squared-is-id A B (dpair a b) = refl

is-equiv-prod-rev : {i j : Level} (A : UU i) (B : UU j) → is-equiv (prod-rev A B)
is-equiv-prod-rev A B = dpair (dpair (prod-rev B A) (prod-rev-squared-is-id B A)) (dpair (prod-rev B A) (prod-rev-squared-is-id A B))

-- Exercise 5.9
--                             i      r
-- Consider a sec/retr pair A ---> B ---> A with H : r ∘ i ~ id. Show that x = y is a retr of i(x) = i(y)
-- path-is-retr-of-apsec : {j k : Level} {A : UU j} {B : UU k} (x : A) (y : A) → (i : A → B) → (r : B → A) → ((r ∘ i) ~ id) → ((Id x y) retract-of (Id (i x) (i y)))
-- path-is-retr-of-apsec x y i r H = dpair (ap i) ((dpair (( λ p → x ==⟨ inv (H x) ⟩ r (i x) ==⟨ (ap r p) ⟩ r (i y) ==⟨ (H y) ⟩ y ==∎ )) λ p → {!   !})

-- Exercise 5.10
-- Exercise 5.11
-- Exercise 5.12
-- Exercise 5.13


text:
module Inductive.Examples.Sum where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product
open import Data.List
open import Data.Vec

_⊎_ : Set → Set → Set
A ⊎ B = Inductive (((A ∷ []) , []) ∷ (((B ∷ []) , []) ∷ []))

inl : {A B : Set} → A → A ⊎ B
inl a = construct zero (a ∷ []) []

inr : {A B : Set} → B → A ⊎ B
inr b = construct (suc zero) (b ∷ []) []

case : {A B C : Set} → A ⊎ B → (A → C) → (B → C) → C
case x f g = rec (f ∷ (g ∷ [])) x

ext: agda

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
module Basic.BigStep where

import Data.Bool as Bool using (not)
open import Data.Bool hiding (not; if_then_else_)
open import Data.Empty
open import Data.Fin using (Fin; suc; zero; #_)
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Vec
open import Function
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Product
import Level as L

open import Utils.Decidable
open import Utils.NatOrdLemmas
open import Basic.AST

{-
The big-step semantics of the while language. It's chapter 2.1 in the book.

Note that we use a {n : ℕ} parameter to fix the size of the program state over
our derivations. This is fine since we don't have any derivation rule that
changes the size of the state.

The definitions themselves should come as no surprise to readers of the book.

I employ some syntactic shenanigans to make the definitions visually similar to the familiar
sequent/natural calculus notation (I borrow the formatting style from Conor McBride).
-}

infixr 4 _,_
data ⟨_,_⟩⟱_ {n : ℕ} : St n → State n → State n → Set where

  {- "[ x ]≔ value" is just the standard library definition of vector update -}
  ass :
                   ∀ {s x a}
    → ------------------------------------
      ⟨ x := a , s ⟩⟱ (s [ x ]≔ ⟦ a ⟧ᵉ s)

  skip :
           ∀ {s}
    → -----------------
      ⟨ skip , s ⟩⟱ s

  _,_ :
              ∀ {s₁ s₂ s₃ S₁ S₂} →
      ⟨ S₁ , s₁ ⟩⟱ s₂  →  ⟨ S₂ , s₂ ⟩⟱ s₃
    → -------------------------------------
             ⟨ (S₁ , S₂ ) , s₁ ⟩⟱ s₃

  {- The "T" in "T (⟦ b ⟧ᵉ s)" can be found in Data.Bool.Base. It's ⊤ on a true argument
     and ⊥ on a false argument, so it just lifts boolean values to proofs.
     "F" works the same way, except it's provable on a false argument -}

  if-true :
             ∀ {s s' S₁ S₂ b} →
       T (⟦ b ⟧ᵉ s)  →  ⟨ S₁ , s ⟩⟱ s'
    → -----------------------------------
       ⟨ if b then S₁ else S₂ , s ⟩⟱ s'

  if-false :
              ∀ {s s' S₁ S₂ b} →
       F (⟦ b ⟧ᵉ s)  →  ⟨ S₂ , s ⟩⟱ s'
    → -----------------------------------
       ⟨ if b then S₁ else S₂ , s ⟩⟱ s'

  while-true :
                          ∀ {s s' s'' S b} →
       T (⟦ b ⟧ᵉ s)  →  ⟨ S , s ⟩⟱ s'  →  ⟨ while b do S , s' ⟩⟱ s''
    → ----------------------------------------------------------------
                       ⟨ while b do S , s ⟩⟱ s''

  while-false :
            ∀ {s S b} →
            F (⟦ b ⟧ᵉ s)
    → ------------------------
      ⟨ while b do S , s ⟩⟱ s

{-
Example program and program derivation below.
Note the magnificient de Bruijn variables.

Program derivations are really slow to typecheck.
Brave souls may want to uncomment it and give it a try.
But other than that, we may should that the derivations look pretty clean and concise.
There's lots of details that Agda's inference can fill in for us.

-}
private
  prog : St 3
  prog =
    # 2 := lit 0 ,
    while lte (var (# 1)) (var (# 0)) do
      ( # 2 := add (var (# 2)) (lit 1) ,
        # 0 := sub (var (# 0)) (var (# 1)) )

  -- -- uncomment if you dare
  -- prog-deriv :
  --   ∀ {z} → ⟨ prog , 17 ∷ 5 ∷ z ∷ [] ⟩⟱ (2 ∷ 5 ∷ 3 ∷ [])
  -- prog-deriv =
  --   ass ,
  --   while-true tt (ass , ass)
  --     (while-true tt (ass , ass)
  --       (while-true tt (ass , ass)
  --         (while-false tt)))

{- A program diverges on a state if there is no derivation starting from it
   Since this is big-step semantics, we can't distinguish this from being stuck -}
_divergesOnₙ_ : ∀ {n} → St n → State n → Set
prog divergesOnₙ s = ∀ {s'} → ¬ ⟨ prog , s ⟩⟱ s'

{- A program is divergent if it diverges on all states -}
Divergentₙ : ∀ {n} → St n → Set
Divergentₙ prog = ∀ {s} → prog divergesOnₙ s

{-
The fun thing about the following proof of divergence is that we implicitly
rely on the finiteness of Agda data. Since we have apparent infinite recursion
in the proof, but all inductive Agda data are finite, this implies that no such
derivation may exist in the first place.
-}

private
  inf-loopₙ : ∀ {n} → Divergentₙ {n} (while tt do skip)
  inf-loopₙ (while-true x skip p₁) = inf-loopₙ p₁
  inf-loopₙ (while-false x) = x

-- Semantic equivalence
_⇔_ : ∀ {a b} → Set a → Set b → Set (a L.⊔ b)
A ⇔ B = (A → B) × (B → A)

SemanticEq : ∀ {n} → St n → St n → Set
SemanticEq pa pb = ∀ {s s'} → ⟨ pa , s ⟩⟱ s' ⇔ ⟨ pb , s ⟩⟱ s'

Semantic⇒ : ∀ {n} → St n → St n → Set
Semantic⇒ pa pb = ∀ {s s'} → ⟨ pa , s ⟩⟱ s' → ⟨ pb , s ⟩⟱ s'

private
  -- "while b do S" is equivalent to "if b then (S , while b do S) else skip"
  prog1 : ∀ {n} _ _ → St n
  prog1 b S = while b do S

  prog2 : ∀ {n} _ _ → St n
  prog2 b S = if b then (S , while b do S) else skip

  progeq : ∀ {n b S} → SemanticEq {n} (prog1 b S) (prog2 b S)
  progeq {n}{b}{S} = to , from
    where
    to : Semantic⇒ (prog1 b S) (prog2 b S)
    to (while-true x p1 p2) = if-true x (p1 , p2)
    to (while-false x) = if-false x skip

    from : Semantic⇒ (prog2 b S) (prog1 b S)
    from (if-true x (p1 , p2)) = while-true x p1 p2
    from (if-false x skip) = while-false x

-- The semantics is deterministic. Not much to comment on.
deterministic :
  ∀ {n}{p : St n}{s s' s''} → ⟨ p , s ⟩⟱ s' → ⟨ p , s ⟩⟱ s'' → s' ≡ s''
deterministic = go where
  go : ∀ {p s s' s''} → ⟨ p , s ⟩⟱ s' → ⟨ p , s ⟩⟱ s'' → s' ≡ s''
  go ass ass = refl
  go skip skip = refl
  go (p1 , p2) (p3 , p4) rewrite go p1 p3 | go p2 p4 = refl
  go (if-true x p1) (if-true x₁ p2) rewrite go p1 p2 = refl
  go (if-true x p1) (if-false x₁ p2) rewrite T→≡true x = ⊥-elim x₁
  go (if-false x p1) (if-true x₁ p2) rewrite T→≡true x₁ = ⊥-elim x
  go (if-false x p1) (if-false x₁ p2) rewrite go p1 p2 = refl
  go (while-true x p1 p2) (while-true x₁ p3 p4) rewrite go p1 p3 | go p2 p4 = refl
  go (while-true x p1 p2) (while-false x₁) rewrite T→≡true x = ⊥-elim x₁
  go (while-false x) (while-true x₁ p2 p3) rewrite T→≡true x₁ = ⊥-elim x
  go (while-false x) (while-false x₁) = refl

{-
Below is a proof that is not contained in the book. I did it to familiarize myself
with the style of proving in this semantics.

It proves that if we have a derivation for a loop, then we can construct a
derivation for a loop that goes on for one more iteration, because it has
a higher bound in the condition.

However, if we start out with a loop index that is already greater then the
loop bound, we get divergence. But just having a derivation as hypothesis
rules out divergence! We can show this to Agda by proving the divergence in that
case and getting a contradiction.
-}

private
  loop : St 2
  loop =
    while not (eq (var (# 0)) (var (# 1))) do
      (# 0 := add (lit 1) (var (# 0)))

  once-more :
    ∀ { i₀ lim₀ i₁} →
      ⟨ loop , i₀ ∷ lim₀     ∷ [] ⟩⟱ (i₁     ∷ lim₀     ∷ [])
    → ⟨ loop , i₀ ∷ suc lim₀ ∷ [] ⟩⟱ (1 + i₁ ∷ suc lim₀ ∷ [])

  once-more {i₀}{lim₀} p with cmp i₀ lim₀
  once-more (while-true x₁ ass p₁) | LT x =
    while-true (¬A→FalseA $ a<b⟶a≢sb _ _ x) ass (once-more p₁)

  once-more (while-false x₁) | LT x
    rewrite TrueA→A $ F-not-elim x₁
    = ⊥-elim (a≮a _ x)

  once-more (while-true x p p₁) | EQ refl =
    ⊥-elim (FalseA→¬A x refl)

  once-more (while-false x) | EQ refl =
    while-true (¬A→FalseA $ a≢sa _) ass (while-false (F-not-add $ A→TrueA refl))

  once-more p | GT x =
    ⊥-elim (diverges x p)
    where
    diverges : ∀ {i₀ lim₀} → lim₀ < i₀ → loop divergesOnₙ (i₀ ∷ lim₀ ∷ [])
    diverges p1 (while-true x ass p3) = diverges (<-weakenr1 _ _ p1) p3
    diverges p1 (while-false x) rewrite TrueA→A $ F-not-elim x = a≮a _ p1

{-
Correctness of a factorial program.

This task made me ponder the nature of meta- and object languages a bit.

Our job here is to prove that the factorial program computes a factorial. But in order to
be able to state this property, we had to define the notion of factorial in Agda. But this
Agda ⟦fac⟧ function is already executable! Luckily for us, Agda and Coq and co. already
have computational meaning. So if our goal is to simply have a correct factorial program,
then we should just write it in Agda or Coq (although neither supports software development
in an acceptable manner, unfortunately).

Some languages are just better as metalanguages, but if those metalanguages are also
satisfactory as object languages then we might make do with just a single
language, instead of multiple languages and multiple semantics.

Turning back to the actual proof, note that unlike the manual factorial proof in
Chapter 6.1 of the book, this one looks pretty neat and it's also concise.
It's also structurally similar to the program itself.
-}

module Fac where

  ⟦fac⟧ : ℕ → ℕ
  ⟦fac⟧ zero    = 1
  ⟦fac⟧ (suc n) = suc n * ⟦fac⟧ n

  fac-loop : St 3
  fac-loop =
    while lt (var (# 1)) (var (# 0)) do
        (# 1 := add (lit 1) (var (# 1)) ,
         # 2 := mul (var (# 1)) (var (# 2)) )

  fac : St 3
  fac =
    # 1 := lit 0 ,
    # 2 := lit 1 ,
    fac-loop

  fac-loop-ok :
    ∀ d i
    → ⟨ fac-loop , d + i ∷ i ∷ ⟦fac⟧ i ∷ [] ⟩⟱ (d + i ∷ d + i ∷ ⟦fac⟧ (d + i) ∷ [])
  fac-loop-ok zero i = while-false (¬A→FalseA $ a≮a i )
  fac-loop-ok (suc d) i with fac-loop-ok d (suc i)
  ... | next rewrite +-suc d i = while-true (A→TrueA $ a<sb+a i d) (ass , ass) next

  fac-ok :
    ∀ n {i acc} → ⟨ fac , n ∷ i ∷ acc ∷ [] ⟩⟱ (n ∷ n ∷ ⟦fac⟧ n ∷ [])
  fac-ok n with fac-loop-ok n 0
  ... | loop-ok rewrite +-comm n 0 = ass , ass , loop-ok

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
postulate
  A : Set

open import Agda.Builtin.Equality

-- here the solution g := (\ (@0 x) (@0 y) → f y x) is not well-typed
-- in a non-erased context, which is how `g` is declared.
bar : (f : A → A → A) (g : @0 A → @0 A → A)
    → @0 _≡_ {A = @0 A → @0 A → A} g (\ (@0 x) (@0 y) → f y x)
    → @0 A → @0 A → A
bar f g refl = g

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Category.Monoidal

module Categories.Category.Monoidal.Traced {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open Category C

open import Level

open import Data.Product using (_,_)

open import Categories.Category.Monoidal.Symmetric M

private
  variable
    A B X Y : Obj
    f g : A ⇒ B

------------------------------------------------------------------------------
-- Def from http://ncatlab.org/nlab/show/traced+monoidal+category
--
-- A symmetric monoidal category (C,⊗,1,b) (where b is the symmetry) is
-- said to be traced if it is equipped with a natural family of functions
--
-- TrXA,B:C(A⊗X,B⊗X)→C(A,B)
-- satisfying three axioms:
--
-- Vanishing: Tr1A,B(f)=f (for all f:A→B) and
-- TrX⊗YA,B=TrXA,B(TrYA⊗X,B⊗X(f)) (for all f:A⊗X⊗Y→B⊗X⊗Y)
--
-- Superposing: TrXC⊗A,C⊗B(idC⊗f)=idC⊗TrXA,B(f) (for all f:A⊗X→B⊗X)
--
-- Yanking: TrXX,X(bX,X)=idX

-- Traced monoidal category
--  is a symmetric monoidal category with a trace operation
--
-- note that the definition in this library is significantly easier than the previous one because
-- we adopt a simpler definition of monoidal category to begin with.
record Traced : Set (levelOfTerm M) where
  field
    symmetric : Symmetric

  open Symmetric symmetric public

  field
    trace : ∀ {X A B} → A ⊗₀ X ⇒ B ⊗₀ X → A ⇒ B

    vanishing₁  : trace {X = unit} (f ⊗₁ id) ≈ f
    vanishing₂  : trace {X = X} (trace {X = Y} (associator.to ∘ f ∘ associator.from))
                ≈ trace {X = X ⊗₀ Y} f
    superposing : trace {X = X} (associator.to ∘ id {Y} ⊗₁ f ∘ associator.from) ≈ id {Y} ⊗₁ trace {X = X} f
    yanking     : trace (braiding.⇒.η (X , X)) ≈ id

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Structure.Category
open import Type

module Structure.Category.Monad.Category
  {ℓₒ ℓₘ ℓₑ}
  {cat : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}}
  where

import      Data.Tuple as Tuple
import      Function.Equals
open        Function.Equals.Dependent
import      Lvl
open import Structure.Category.Functor
open import Structure.Category.Monad{cat = cat}
open import Structure.Category.Monad.ExtensionSystem{cat = cat}
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Setoid
open import Syntax.Transitivity

open CategoryObject(cat)
open Category.ArrowNotation(category)
open Category(category)
private open module MorphismEquiv {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()

module _ (T : Object → Object) ⦃ extSys : ExtensionSystem(T) ⦄ where
  open ExtensionSystem(extSys)
  open Functor(functor)
  open Monad ⦃ functor ⦄ (monad) using (μ-functor-[∘]-identityₗ)

  -- Also called: Kleisli category
  categoryₑₓₜ : Category(\x y → (x ⟶ T(y)))
  Category._∘_ categoryₑₓₜ = _∘ₑₓₜ_
  Category.id  categoryₑₓₜ = idₑₓₜ
  BinaryOperator.congruence (Category.binaryOperator categoryₑₓₜ {x}{y}{z}) {f₁}{f₂} {g₁}{g₂} f₁f₂ g₁g₂ =
    f₁ ∘ₑₓₜ g₁           🝖[ _≡_ ]-[]
    ext f₁ ∘ g₁          🝖[ _≡_ ]-[ congruence₂(_∘_) (congruence₁(ext) f₁f₂) g₁g₂ ]
    ext f₂ ∘ g₂          🝖[ _≡_ ]-[]
    f₂ ∘ₑₓₜ g₂           🝖-end
  Morphism.Associativity.proof (Category.associativity categoryₑₓₜ) {x} {y} {z} {w} {f} {g} {h} =
    (f ∘ₑₓₜ g) ∘ₑₓₜ h     🝖[ _≡_ ]-[]
    ext(ext(f) ∘ g) ∘ h   🝖[ _≡_ ]-[ congruence₂ₗ(_∘_)(_) ext-distribute ]
    (ext(f) ∘ ext(g)) ∘ h 🝖[ _≡_ ]-[ Morphism.associativity(_∘_) ]
    ext(f) ∘ (ext(g) ∘ h) 🝖[ _≡_ ]-[]
    f ∘ₑₓₜ (g ∘ₑₓₜ h)     🝖-end
  Morphism.Identityₗ.proof (Tuple.left (Category.identity categoryₑₓₜ)) {x} {y} {f} =
    idₑₓₜ ∘ₑₓₜ f           🝖[ _≡_ ]-[]
    ext(η(y)) ∘ f          🝖[ _≡_ ]-[ congruence₂ₗ(_∘_)(f) ext-inverse ]
    id ∘ f                 🝖[ _≡_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    f                      🝖-end
  Morphism.Identityᵣ.proof (Tuple.right (Category.identity categoryₑₓₜ)) {x} {y} {f} =
    f ∘ₑₓₜ idₑₓₜ  🝖[ _≡_ ]-[]
    ext(f) ∘ η(x) 🝖[ _≡_ ]-[ ext-identity ]
    f             🝖-end

module _ (T : Object → Object) ⦃ functor : Functor(category)(category)(T) ⦄ ⦃ monad : Monad(T) ⦄ where
  open Functor(functor)
  open Monad(monad) hiding (ext)
  open ExtensionSystem(monad-to-extensionSystem) hiding (η ; μ)

  -- Note: This is the supposed to be the same as categoryₑₓₜ but proven from a monad directly.
  monad-category : Category(\x y → (x ⟶ T(y)))
  Category._∘_ monad-category f g = ext(f) ∘ g
  Category.id monad-category {x} = η(x)
  BinaryOperator.congruence (Category.binaryOperator monad-category {x}{y}{z}) {f₁}{f₂} {g₁}{g₂} f₁f₂ g₁g₂ =
    ext(f₁) ∘ g₁         🝖[ _≡_ ]-[]
    (μ(z) ∘ map f₁) ∘ g₁ 🝖-[ Morphism.associativity(_∘_) ]
    μ(z) ∘ (map f₁ ∘ g₁) 🝖-[ congruence₂ᵣ(_∘_)(μ(z)) (congruence₂(_∘_) (congruence₁(map) f₁f₂) g₁g₂) ]
    μ(z) ∘ (map f₂ ∘ g₂) 🝖-[ Morphism.associativity(_∘_) ]-sym
    (μ(z) ∘ map f₂) ∘ g₂ 🝖[ _≡_ ]-[]
    ext(f₂) ∘ g₂         🝖-end
  Morphism.Associativity.proof (Category.associativity monad-category) {x} {y} {z} {w} {f} {g} {h} =
    ext(ext(f) ∘ g) ∘ h   🝖-[ congruence₂ₗ(_∘_)(_) (ext-distribute) ]
    (ext(f) ∘ ext(g)) ∘ h 🝖-[ Morphism.associativity(_∘_) ]
    ext(f) ∘ (ext(g) ∘ h) 🝖-end
  Morphism.Identityₗ.proof (Tuple.left (Category.identity monad-category)) {x} {y} {f} =
    ext(η(y)) ∘ f          🝖[ _≡_ ]-[]
    (μ(y) ∘ map(η(y))) ∘ f 🝖-[ congruence₂ₗ(_∘_)(f) (_⊜_.proof μ-functor-[∘]-identityₗ) ]
    id ∘ f                 🝖-[ Morphism.identityₗ(_∘_)(id) ]
    f                      🝖-end
  Morphism.Identityᵣ.proof (Tuple.right (Category.identity monad-category)) {x} {y} {f} = ext-identity

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

-- The definitions of lexicographic orderings used here is suitable if
-- the argument order is a (non-strict) partial order.

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Binary.Lex.NonStrict where

open import Data.Empty using (⊥)
open import Function
open import Data.Unit.Base using (⊤; tt)
open import Data.Product
open import Data.List.Base
open import Data.List.Relation.Binary.Pointwise using (Pointwise; [])
import Data.List.Relation.Binary.Lex.Strict as Strict
open import Level
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.Construct.NonStrictToStrict as Conv

------------------------------------------------------------------------
-- Publically re-export definitions from Core

open import Data.List.Relation.Binary.Lex.Core as Core public
  using (base; halt; this; next; ¬≤-this; ¬≤-next)

------------------------------------------------------------------------
-- Strict lexicographic ordering.

module _ {a ℓ₁ ℓ₂} {A : Set a} where

  Lex-< : (_≈_ : Rel A ℓ₁) (_≼_ : Rel A ℓ₂) → Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-< _≈_ _≼_ = Core.Lex ⊥ _≈_ (Conv._<_ _≈_ _≼_)

  -- Properties

  module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _<_ = Lex-< _≈_ _≼_

    <-irreflexive : Irreflexive _≋_ _<_
    <-irreflexive = Strict.<-irreflexive (Conv.<-irrefl _≈_ _≼_)

    <-asymmetric : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
                   Antisymmetric _≈_ _≼_ → Asymmetric _<_
    <-asymmetric eq resp antisym  =
      Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
                        (Conv.<-asym _≈_ _ antisym)
                        where open IsEquivalence eq

    <-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
                      Antisymmetric _≋_ _<_
    <-antisymmetric sym antisym =
      Core.antisymmetric sym
        (Conv.<-irrefl _≈_ _≼_)
        (Conv.<-asym _ _≼_ antisym)

    <-transitive : IsPartialOrder _≈_ _≼_ → Transitive _<_
    <-transitive po =
      Core.transitive isEquivalence
        (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
        (Conv.<-trans _ _≼_ po)
      where open IsPartialOrder po

    <-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _<_ Respects₂ _≋_
    <-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)

    <-compare : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
                Total _≼_ → Trichotomous _≋_ _<_
    <-compare sym _≟_ antisym tot =
      Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≟_ antisym tot)

    <-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _<_
    <-decidable _≟_ _≼?_ =
      Core.decidable (no id) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)

    <-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ →
                             IsStrictPartialOrder _≋_ _<_
    <-isStrictPartialOrder po =
      Strict.<-isStrictPartialOrder
        (Conv.<-isStrictPartialOrder _ _ po)

    <-isStrictTotalOrder : Decidable _≈_ → IsTotalOrder _≈_ _≼_ →
                           IsStrictTotalOrder _≋_ _<_
    <-isStrictTotalOrder dec tot =
      Strict.<-isStrictTotalOrder
        (Conv.<-isStrictTotalOrder₁ _ _ dec tot)

<-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ →
                       StrictPartialOrder _ _ _
<-strictPartialOrder po = record
  { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
  } where open Poset po

<-strictTotalOrder : ∀ {a ℓ₁ ℓ₂} → DecTotalOrder a ℓ₁ ℓ₂ →
                     StrictTotalOrder _ _ _
<-strictTotalOrder dtot = record
  { isStrictTotalOrder = <-isStrictTotalOrder _≟_ isTotalOrder
  } where open DecTotalOrder dtot

------------------------------------------------------------------------
-- Non-strict lexicographic ordering.

module _ {a ℓ₁ ℓ₂} {A : Set a} where

  Lex-≤ : (_≈_ : Rel A ℓ₁) (_≼_ : Rel A ℓ₂) → Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-≤ _≈_ _≼_ = Core.Lex ⊤ _≈_ (Conv._<_ _≈_ _≼_)

  ≤-reflexive : ∀ _≈_ _≼_ → Pointwise _≈_ ⇒ Lex-≤ _≈_ _≼_
  ≤-reflexive _≈_ _≼_ = Strict.≤-reflexive _≈_ (Conv._<_ _≈_ _≼_)

  -- Properties
  module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _≤_ = Lex-≤ _≈_ _≼_

    ≤-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ →
                      Antisymmetric _≋_ _≤_
    ≤-antisymmetric sym antisym =
      Core.antisymmetric sym
        (Conv.<-irrefl _≈_ _≼_)
        (Conv.<-asym _ _≼_ antisym)

    ≤-transitive : IsPartialOrder _≈_ _≼_ → Transitive _≤_
    ≤-transitive po =
      Core.transitive isEquivalence
        (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
        (Conv.<-trans _ _≼_ po)
      where open IsPartialOrder po

    ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
    ≤-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)

    ≤-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
    ≤-decidable _≟_ _≼?_ =
      Core.decidable (yes tt) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)

    ≤-total : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
              Total _≼_ → Total _≤_
    ≤-total sym dec-≈ antisym tot =
      Strict.≤-total sym (Conv.<-trichotomous _ _ sym dec-≈ antisym tot)

    ≤-isPreorder : IsPartialOrder _≈_ _≼_ → IsPreorder _≋_ _≤_
    ≤-isPreorder po =
      Strict.≤-isPreorder
        isEquivalence (Conv.<-trans _ _ po)
        (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      where open IsPartialOrder po

    ≤-isPartialOrder : IsPartialOrder _≈_ _≼_ → IsPartialOrder _≋_ _≤_
    ≤-isPartialOrder po =
      Strict.≤-isPartialOrder
        (Conv.<-isStrictPartialOrder _ _ po)

    ≤-isTotalOrder : Decidable _≈_ → IsTotalOrder _≈_ _≼_ →
                     IsTotalOrder _≋_ _≤_
    ≤-isTotalOrder dec tot =
      Strict.≤-isTotalOrder
        (Conv.<-isStrictTotalOrder₁ _ _ dec tot)

    ≤-isDecTotalOrder : IsDecTotalOrder _≈_ _≼_ →
                        IsDecTotalOrder _≋_ _≤_
    ≤-isDecTotalOrder dtot =
      Strict.≤-isDecTotalOrder
        (Conv.<-isStrictTotalOrder₂ _ _ dtot)

≤-preorder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ → Preorder _ _ _
≤-preorder po = record
  { isPreorder = ≤-isPreorder isPartialOrder
  } where open Poset po

≤-partialOrder : ∀ {a ℓ₁ ℓ₂} → Poset a ℓ₁ ℓ₂ → Poset _ _ _
≤-partialOrder po = record
  { isPartialOrder = ≤-isPartialOrder isPartialOrder
  } where open Poset po

≤-decTotalOrder : ∀ {a ℓ₁ ℓ₂} → DecTotalOrder a ℓ₁ ℓ₂ →
                  DecTotalOrder _ _ _
≤-decTotalOrder dtot = record
  { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
  } where open DecTotalOrder dtot


text:
{-# OPTIONS --exact-split #-}

module ExactSplitMin where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

min : ℕ → ℕ → ℕ
min zero    y       = zero
min x       zero    = zero
min (suc x) (suc y) = suc (min x y)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------------
-- Division program
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- This module define a division program using repeated subtraction
-- (Dybjer 1985).

-- Peter Dybjer. Program verification in a logical theory of
-- constructions. In Jean-Pierre Jouannaud, editor. Functional
-- Programming Languages and Computer Architecture, volume 201 of
-- LNCS, 1985, pages 334-349. Appears in revised form as Programming
-- Methodology Group Report 26, June 1986.

module LTC-PCF.Program.Division.Division where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities

------------------------------------------------------------------------------

divh : D → D
divh g = lam (λ i → lam (λ j →
             if (lt i j) then zero else (succ₁ (g · (i ∸ j) · j))))

div : D → D → D
div i j = fix divh · i · j

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.DecPropositional directly.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Data.Vec.Relation.Equality.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where

open import Data.Vec.Relation.Binary.Equality.DecPropositional _≟_ public


text:
-- Andreas, 2016-05-19, issue 1986, after report from Nisse
-- Andreas, 2016-06-02 fixed
-- This has been reported before as issue 842

-- {-# OPTIONS -v tc.cover:20 #-}
-- {-# OPTIONS -v tc.cc:20 -v reduce.compiled:100 #-}

open import Common.Equality

data Bool : Set where
  true false : Bool

not : Bool → Bool
not true = false
not      = λ _ → true

not-true : not true ≡ false
not-true = refl

not-false : not false ≡ true
not-false = refl


text:
module Cats.Category.Constructions.Unique where

open import Data.Unit using (⊤)
open import Level

open import Cats.Category.Base
open import Cats.Util.Conv

module Build {lo la l≈} (Cat : Category lo la l≈) where

  open Category Cat

  IsUniqueSuchThat : ∀ {lp A B} → (A ⇒ B → Set lp) → A ⇒ B → Set (la ⊔ l≈ ⊔ lp)
  IsUniqueSuchThat P f = ∀ {g} → P g → f ≈ g

  IsUnique : ∀ {A B} → A ⇒ B → Set (la ⊔ l≈)
  IsUnique {A} {B} = IsUniqueSuchThat {A = A} {B} (λ _ → ⊤)

  IsUniqueSuchThat→≈ : ∀ {lp A B} {P : A ⇒ B → Set lp} {f}
    → IsUniqueSuchThat P f
    → ∀ {g h}
    → P g
    → P h
    → g ≈ h
  IsUniqueSuchThat→≈ unique Pg Ph = ≈.trans (≈.sym (unique Pg)) (unique Ph)

  record ∃!′ {lp A B} (P : A ⇒ B → Set lp) : Set (la ⊔ l≈ ⊔ lp) where
    constructor ∃!-intro
    field
      arr : A ⇒ B
      prop : P arr
      unique : IsUniqueSuchThat P arr

  instance
    HasArrow-∃! : ∀ {lp A B} {P : A ⇒ B → Set lp}
      → HasArrow (∃!′ P) lo la l≈
    HasArrow-∃! = record { Cat = Cat ; _⃗ = ∃!′.arr }

  syntax ∃!′ (λ f → P) = ∃![ f ] P

  ∃!″ : ∀ {lp A B} (P : A ⇒ B → Set lp) → Set (la ⊔ l≈ ⊔ lp)
  ∃!″ = ∃!′

  syntax ∃!″ {A = A} {B} (λ f → P) = ∃![ f ∈ A ⇒ B ] P

  ∃! : (A B : Obj) → Set (la ⊔ l≈)
  ∃! A B = ∃![ f ∈ A ⇒ B ] ⊤

  ∃!→≈ : ∀ {lp A B} {P : A ⇒ B → Set lp}
    → ∃!′ P
    → ∀ {g h}
    → P g
    → P h
    → g ≈ h
  ∃!→≈ (∃!-intro _ _ unique) = IsUniqueSuchThat→≈ unique

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Oscar.Category.Functor where

open import Oscar.Category.Setoid
open import Oscar.Category.Category
open import Oscar.Category.Semifunctor
open import Oscar.Level

record Categories 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
  constructor _,_
  field
    category₁ : Category 𝔬₁ 𝔪₁ 𝔮₁
    category₂ : Category 𝔬₂ 𝔪₂ 𝔮₂

  module 𝔊₁ = Category category₁
  module 𝔊₂ = Category category₂

  semigroupoids : Semigroupoids _ _ _ _ _ _
  Semigroupoids.semigroupoid₁ semigroupoids = 𝔊₁.semigroupoid
  Semigroupoids.semigroupoid₂ semigroupoids = 𝔊₂.semigroupoid

module _
  {𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂} (categories : Categories 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂)
  where
  open Categories categories

  record IsFunctor
    {μ : 𝔊₁.⋆ → 𝔊₂.⋆}
    (𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y)
    : Set (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂) where
    instance _ = 𝔊₁.IsSetoid↦
    instance _ = 𝔊₂.IsSetoid↦
    field
      ⦃ isSemifunctor ⦄ : IsSemifunctor semigroupoids 𝔣
    field
      identity : (x : 𝔊₁.⋆) → 𝔣 (𝔊₁.ε {x = x}) ≋ 𝔊₂.ε
    open IsSemifunctor isSemifunctor public

open IsFunctor ⦃ … ⦄ public

open import Oscar.Category.Morphism

record Functor 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
  constructor _,_
  field
    categories : Categories 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂
  open Categories categories public

  field
    {μ} : 𝔊₁.⋆ → 𝔊₂.⋆
    𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y
    ⦃ isFunctor ⦄ : IsFunctor categories 𝔣
  open IsFunctor isFunctor public

-- module _
--   {𝔬₁ 𝔪₁ 𝔮₁} (category₁ : Category 𝔬₁ 𝔪₁ 𝔮₁)
--   {𝔬₂ 𝔪₂ 𝔮₂} (category₂ : Category 𝔬₂ 𝔪₂ 𝔮₂)
--   where

--   private module 𝔊₁ = Category category₁
--   private module 𝔊₂ = Category category₂

--   record IsFunctor
--     (μ : 𝔊₁.⋆ → 𝔊₂.⋆)
--     (𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y)
--     : Set (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂) where
--     field
--       ⦃ isSemifunctor ⦄ : IsSemifunctor 𝔊₁.semigroupoid 𝔊₂.semigroupoid μ 𝔣
--     field
--       identity : (x : 𝔊₁.⋆) → 𝔣 (𝔊₁.ε {x = x}) ≋ 𝔊₂.ε

-- open IsFunctor ⦃ … ⦄ public

-- record Functor 𝔬₁ 𝔪₁ 𝔮₁ 𝔬₂ 𝔪₂ 𝔮₂ : Set (lsuc (𝔬₁ ⊔ 𝔪₁ ⊔ 𝔮₁ ⊔ 𝔬₂ ⊔ 𝔪₂ ⊔ 𝔮₂)) where
--   field
--     category₁ : Category 𝔬₁ 𝔪₁ 𝔮₁
--     category₂ : Category 𝔬₂ 𝔪₂ 𝔮₂

--   module 𝔊₁ = Category category₁
--   module 𝔊₂ = Category category₂

--   field
--     μ : 𝔊₁.⋆ → 𝔊₂.⋆
--     𝔣 : ∀ {x y} → x 𝔊₁.↦ y → μ x 𝔊₂.↦ μ y
--     ⦃ isFunctor ⦄ : IsFunctor category₁ category₂ μ 𝔣


text:
module Impossible where

{-# IMPOSSIBLE #-}


text:
module _ where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection renaming (returnTC to return; bindTC to _>>=_)

_>>_ : {A B : Set} → TC A → TC B → TC B
m >> m' = m >>= λ _ → m'

macro
  solve : Nat → Term → TC ⊤
  solve blocker hole = do
    unify hole (lam visible (abs "x" (var 0 [])))
    meta x _ ← withNormalisation true (quoteTC blocker)
      where _ → return _
    blockOnMeta x

mutual
  blocker : Nat
  blocker = _

  bug : Bool
  bug = (solve blocker) true

  unblock : blocker ≡ 0
  unblock = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Nat

data Sing : Nat → Set where
  i : (k : Nat) → Sing k

toSing : (n : Nat) → Sing n
toSing n = i n

fun : (n : Nat) → Nat
fun n with toSing n
fun .n       | i n with toSing n
fun .(n + n) | i .n | i n = {!!}


text:
module PrintNat where

import PreludeShow
open PreludeShow

mainS = showNat 42

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The sublist relation over propositional equality.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Binary.Subset.Propositional
  {a} {A : Set a} where

import Data.List.Relation.Binary.Subset.Setoid as SetoidSubset
open import Relation.Binary.PropositionalEquality using (setoid)

------------------------------------------------------------------------
-- Re-export parameterised definitions from setoid sublists

open SetoidSubset (setoid A) public


text:
open import Common.Prelude renaming (Nat to ℕ; _+_ to _+ℕ_)
open import Common.Product
open import Common.Equality

postulate
  _≤ℕ_ : (n m : ℕ) → Set
  maxℕ : (n m : ℕ) → ℕ

When : (b : Bool) (P : Set) → Set
When true P = P
When false P = ⊤

infix 30 _⊕_
infix 20 _+_
infix 10 _≤_
infix 10 _<_

infixr 4 _,_

mutual

  data Cxt : Set where
    ∘   : Cxt
    _,_ : (Δ : Cxt) (b : Size Δ) → Cxt

  data Var : (Δ : Cxt) → Set where
    vz : ∀{Δ b}             → Var (Δ , b)
    vs : ∀{Δ b} (i : Var Δ) → Var (Δ , b)

  data Base (Δ : Cxt) : Set where
    zero : Base Δ
    ∞    : Base Δ
    var  : Var Δ → Base Δ

  record Size (Δ : Cxt) : Set where
    inductive
    constructor _⊕_
    field h : Base Δ
          n : ℕ

↑ : ∀{Δ} (a : Size Δ) → Size Δ
↑ (h ⊕ n) = h ⊕ suc n

_+_ : ∀{Δ} (a : Size Δ) (m : ℕ) → Size Δ
(h ⊕ n) + m = h ⊕ (n +ℕ m)

_-_ : ∀{Δ} (a : Size Δ) (m : ℕ) → Size Δ
(h ⊕ n) - m = h ⊕ (n ∸ m)

ClosedSize = Size ∘

data _≤_ : (a b : ClosedSize) → Set where
  leZZ : ∀{n m} (p : n ≤ℕ m) → zero ⊕ n ≤ zero ⊕ m
  leZ∞ : ∀{n m}               → zero ⊕ n ≤ ∞ ⊕ m
  le∞∞ : ∀{n m} (p : n ≤ℕ m) → ∞ ⊕ n ≤ ∞ ⊕ m

_<_ : (a b : ClosedSize) → Set
a < b = ↑ a ≤ b

max : (a b : ClosedSize) → ClosedSize
max (zero ⊕ n) (zero ⊕ n') = zero ⊕ maxℕ n n'
max (zero ⊕ n) (∞ ⊕ n') = ∞ ⊕ n'
max (zero ⊕ n) (var () ⊕ n')
max (∞ ⊕ n) (zero ⊕ n') = ∞ ⊕ n
max (∞ ⊕ n) (∞ ⊕ n') =  ∞ ⊕ maxℕ n n'
max (∞ ⊕ n) (var () ⊕ n')
max (var () ⊕ n)

-- Closed size valuation
mutual

  data Val (chk : Bool) : (Δ : Cxt) → Set where
    ∘    : Val chk ∘
    _,_<_∣_ : ∀{Δ} (ξ : Val chk Δ) (a : ClosedSize) b (p : When chk (a < eval ξ b)) → Val chk (Δ , b)

  lookup : ∀{Δ chk} (ξ : Val chk Δ) (x : Var Δ) → ClosedSize
  lookup (ξ , a < b ∣ p) vz     = a
  lookup (ξ , a < b ∣ p) (vs x) = lookup ξ x

  evalBase : ∀{Δ chk} (ξ : Val chk Δ) (a : Base Δ) → ClosedSize
  evalBase ξ zero    = zero ⊕ 0
  evalBase ξ ∞       = ∞ ⊕ 0
  evalBase ξ (var x) = lookup ξ x

  eval : ∀{Δ chk} (ξ : Val chk Δ) (a : Size Δ) → ClosedSize
  eval ξ (h ⊕ n) = evalBase ξ h + n

UVal = Val false  -- unsound valuation
SVal = Val true   -- sound valuation

update : ∀{Δ} (ρ : UVal Δ) (x : Var Δ) (f : ClosedSize → ClosedSize) → UVal Δ
update (ρ , a < b ∣ _) vz     f = ρ , f a < b ∣ _
update (ρ , a < b ∣ _) (vs x) f = update ρ x f , a < b ∣ _

data _≤V_ {chk chk'} : ∀ {Δ} (ρ : Val chk Δ) (ξ : Val chk' Δ) → Set where
  ∘   : ∘ ≤V ∘
  _,_ : ∀{Δ} {ρ : Val chk Δ} {ξ : Val chk' Δ} {a a' b p q}
        (r : ρ ≤V ξ) (s : a ≤ a') → (ρ , a < b ∣ p) ≤V (ξ , a' < b ∣ q)

lemma-str :  ∀ {Δ} (x : Var Δ) {n} {a} {ρ : UVal Δ} {ξ : SVal Δ}
  → (p : ρ ≤V ξ)
  → (q : a < lookup ξ x + n)
  → update ρ x (max (↑ a - n)) ≤V ξ
lemma-str vz     (p , s) q = {!q!}
lemma-str (vs x) (p , s) q = {!q!}


text:
open import Categories
open import Functors
open import RMonads

module RMonads.RKleisli.Functors {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                                 {J : Fun C D}(M : RMonad J) where

open import Library
open import RMonads.RKleisli M
open import RAdjunctions

open Cat
open Fun
open RMonad M

RKlL : Fun C Kl
RKlL = record{
  OMap  = id;
  HMap  = λ f → comp D η (HMap J f);
  fid   =
    proof
    comp D η (HMap J (iden C))
    ≅⟨ cong (comp D η) (fid J) ⟩
    comp D η (iden D)
    ≅⟨ idr D ⟩
    η ∎;
  fcomp = λ{_ _ _ f g} →
    proof
    comp D η (HMap J (comp C f g))
    ≅⟨ cong (comp D η) (fcomp J) ⟩
    comp D η (comp D (HMap J f) (HMap J g))
    ≅⟨ sym (ass D) ⟩
    comp D (comp D η (HMap J f)) (HMap J g)
    ≅⟨ cong (λ f → comp D f (HMap J g)) (sym law2) ⟩
    comp D (comp D (bind (comp D η (HMap J f))) η) (HMap J g)
    ≅⟨ ass D ⟩
    comp D (bind (comp D η (HMap J f))) (comp D η (HMap J g))
    ∎}

RKlR : Fun Kl D
RKlR = record{
  OMap  = T;
  HMap  = bind;
  fid   = law1;
  fcomp = law3}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
postulate B : Set

module M where
  record ⊤ : Set where

module P (A : Set) where
  open M public

module PB = P B


text:
{-# OPTIONS --experimental-irrelevance #-}
{-# OPTIONS --sized-types #-}

open import Agda.Primitive
  public using (lzero; lsuc)

open import Agda.Builtin.Size
  public using (Size; ↑_) renaming (∞ to oo)

open import Agda.Builtin.Nat
  public using (suc) renaming (Nat to ℕ)

_+_ : Size → ℕ → Size
s + 0 = s
s + suc n = ↑ (s + n)

data Nat : ..(i : Size) → Set where
  zero : ∀ .i → Nat (↑ i)
  suc  : ∀ .i → Nat i → Nat (↑ i)

caseof : ∀{a b} {A : Set a} (B : A → Set b) → (x : A) → ((x : A) → B x) → B x
caseof B x f = f x

syntax caseof B x f = case x return B of f

fix : ∀{ℓ}
  (T : ..(i : Size) → Nat i → Set ℓ)
  (f : ∀ .j → ((x : Nat j) → T j x) → (x : Nat (↑ j)) → T (↑ j) x)
  .{i}
  (x : Nat i)
  → T i x
fix T f (zero j)  = f j (fix T f) (zero j)
fix T f (suc j n) = f j (fix T f) (suc j n)

max_stars_repo_name: andreasabel/S

max_issues_repo_name: andreasabel/Sit

max_forks_repo_name: andreasabel/Sit


text:
import Oscar.Class.Reflexivity.Function
import Oscar.Class.Transextensionality.Proposequality -- FIXME why not use the instance here?
open import Oscar.Class
open import Oscar.Class.Category
open import Oscar.Class.HasEquivalence
open import Oscar.Class.IsCategory
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Precategory
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.[IsExtensionB]
open import Oscar.Data.Proposequality
open import Oscar.Prelude
open import Oscar.Property.Category.Function
open import Oscar.Property.Setoid.Proposextensequality
open import Oscar.Property.Setoid.Proposequality

module Oscar.Property.Category.Proposequality where

module _
  {a} {A : Ø a}
  where

  instance

    𝓣ransassociativityProposequality : Transassociativity.class Proposequality⟦ A ⟧ Proposequality transitivity
    𝓣ransassociativityProposequality .⋆ ∅ _ _ = !
{-
module _
  {a} {A : Ø a}
  where

  instance

    𝓣ransextensionalityProposequality : Transextensionality.class Proposequality⟦ A ⟧ Proposequality transitivity
    𝓣ransextensionalityProposequality .⋆ ∅ ∅ = !
-}
module _
  {a} {A : Ø a}
  where

  instance

    𝓣ransleftidentityProposequality : Transleftidentity.class Proposequality⟦ A ⟧ Proposequality ε transitivity
    𝓣ransleftidentityProposequality .⋆ {f = ∅} = ∅

module _
  {a} {A : Ø a}
  where

  instance

    𝓣ransrightidentityProposequality : Transrightidentity.class Proposequality⟦ A ⟧ Proposequality ε transitivity
    𝓣ransrightidentityProposequality .⋆ = ∅
{-
module _
  {a} (A : Ø a)
  where

  instance

    HasEquivalenceExtension : ∀ {x y : A} ⦃ _ : [IsExtensionB] B ⦄ → HasEquivalence (Extension B x y) _
    HasEquivalenceExtension = ∁ Proposextensequality
-}
module _
  {a} {A : Ø a}
  where

  instance

    IsPrecategoryProposequality : IsPrecategory Proposequality⟦ A ⟧ Proposequality transitivity
    IsPrecategoryProposequality = ∁

    IsCategoryProposequality : IsCategory Proposequality⟦ A ⟧ Proposequality ε transitivity
    IsCategoryProposequality = ∁

module _
  {a} (A : Ø a)
  where

  PrecategoryProposequality : Precategory _ _ _
  PrecategoryProposequality = ∁ Proposequality⟦ A ⟧ Proposequality transitivity

  CategoryProposequality : Category _ _ _
  CategoryProposequality = ∁ Proposequality⟦ A ⟧ Proposequality ε transitivity


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.SemiTensor.Core {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Matrix.Tensor struct
open import MLib.Algebra.Operations struct

open Nat using () renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)

open import MLib.Fin.Parts.Simple

open import Data.Nat.LCM
open import Data.Nat.Divisibility

chunkVec : ∀ {m n} → Table S (m *ℕ n) → Table (Table S n) m
chunkVec {m} {n} t .lookup i .lookup j = lookup t (fromParts (i , j))

-- Case 1 of semi-tensor inner product of vectors

_⋉ᵥ₁_ : ∀ {n t} → Table S (t *ℕ n) → Table S t → Table S n
(_⋉ᵥ₁_ {n} {t} X Y) .lookup i = ∑[ k < t ] (X′ .lookup k .lookup i *′ Y .lookup k)
  where X′ = chunkVec {t} X

-- Case 2 of semi-tensor inner product of vector

_⋉ᵥ₂_ : ∀ {n s} → Table S s → Table S (s *ℕ n) → Table S n
(_⋉ᵥ₂_ {n} {s} X Y) .lookup i = ∑[ k < s ] (X .lookup k *′ Y′ .lookup k .lookup i)
  where Y′ = chunkVec {s} Y

module Defn {n p t : ℕ} (lcm : LCM n p t) where
  -- Left semi-Tensor product

  n∣t = LCM.commonMultiple lcm .proj₁
  p∣t = LCM.commonMultiple lcm .proj₂

  t/n = quotient n∣t
  t/p = quotient p∣t

  Iₜₙ = 1● {t/n}
  Iₜₚ = 1● {t/p}

  module _ where
    open ≡.Reasoning

    abstract
      lem₁ : n *ℕ t/n ≡ t
      lem₁ = begin
        n *ℕ t/n ≡⟨ Nat.*-comm n _ ⟩
        t/n *ℕ n ≡⟨ ≡.sym (_∣_.equality n∣t) ⟩
        t ∎

      lem₂ : p *ℕ t/p ≡ t
      lem₂ = begin
        p *ℕ t/p ≡⟨ Nat.*-comm p _ ⟩
        t/p *ℕ p ≡⟨ ≡.sym (_∣_.equality p∣t) ⟩
        t ∎

  module _ {m q} (A : Matrix S m n) (B : Matrix S p q) where
    A′ = A ⊠ Iₜₙ
    B′ = B ⊠ Iₜₚ
    A′′ = ≡.subst (Matrix S (m *ℕ t/n)) {y = t} lem₁ A′
    B′′ = ≡.subst (λ h → Matrix S h (q *ℕ t/p)) {y = t} lem₂ B′

    stp : Matrix S (m *ℕ t/n) (q *ℕ t/p)
    stp = A′′ ⊗ B′′

infixl 7 _⋉_

_⋉_ : ∀ {m n p q} → Matrix S m n → Matrix S p q → Matrix S _ _
_⋉_ {m} {n} {p} {q} = Defn.stp {n} {p} (lcm n p .proj₂)


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.BiInvInt where

open import Cubical.Data.Int.MoreInts.BiInvInt.Base public

open import Cubical.Data.Int.MoreInts.BiInvInt.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{-# OPTIONS --sized-types --show-implicit #-}

module WrongSizeAssignment2 where

open import Common.Size renaming (↑_ to _^)

data Empty : Set where

data N : {_ : Size} -> Set where
  zero : N {∞}
  suc  : forall {i} -> N {i ^} -> N {i}

lift : forall {i} -> N {i} -> N {i ^}
lift zero    = zero
lift (suc x) = suc (lift x)

f : forall {i} -> N {i} -> Empty
f x = f (suc (lift x))


text:
postulate
  U V : Set
  T   : V → Set
  H   : ∀ v → T v → Set
  f   : U → V

data D : Set where d : D

foo : (u : U) (t : T (f u)) (h : H (f u) t) → H (f u) t
foo u t h with f u | d
... | fu | x = h


text:
module RandomAccessList.Standard.Properties where

open import BuildingBlock
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
import      BuildingBlock.BinaryLeafTree as BLT

open import RandomAccessList.Standard
open import RandomAccessList.Standard.Core
open import RandomAccessList.Standard.Core.Properties

open import Data.Nat
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple
open import Data.Product as Prod
open import Data.Product hiding (map)
open import Data.Empty using (⊥-elim)
open import Function
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (False; True; fromWitnessFalse)
open import Relation.Nullary.Negation using (contraposition)

open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

tailₙ-suc : ∀ {n A} → (xs : 0-1-RAL A n) → (p : ⟦ xs ⟧ ≢ 0)
           → suc ⟦ tailₙ xs p ⟧ₙ ≡ ⟦ xs ⟧ₙ
tailₙ-suc {n} {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {n}) refl))
tailₙ-suc (  0∷ xs) p =
    begin
        2 + (2 * ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ)
    ≡⟨ sym (+-*-suc 2 ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ) ⟩
        2 * suc ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ
    ≡⟨ cong (_*_ 2) (tailₙ-suc xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p)) ⟩
        2 * ⟦ xs ⟧ₙ
    ∎
tailₙ-suc (x 1∷ xs) p = refl

tail-suc : ∀ {A} → (xs : 0-1-RAL A 0) → (p : ⟦ xs ⟧ ≢ 0)
          → suc ⟦ tail xs p ⟧ ≡ ⟦ xs ⟧
tail-suc {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {0}) refl))
tail-suc (0∷ xs) p =
    begin
        2 + (2 * ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ + 0)
    ≡⟨ sym (+-assoc 2 (2 * ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ) 0)  ⟩
        2 + 2 * ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ + 0
    ≡⟨ cong (λ x → x + 0) (sym (+-*-suc 2 ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ)) ⟩
        2 * suc ⟦ tailₙ xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p) ⟧ₙ + 0
    ≡⟨ cong (λ x → 2 * x + 0) (tailₙ-suc xs (⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p)) ⟩
        2 * ⟦ xs ⟧ₙ + 0
    ∎
tail-suc (x 1∷ xs) p = refl

headₙ-tailₙ-consₙ : ∀ {n A} → (xs : 0-1-RAL A n) → (p : ⟦ xs ⟧ ≢ 0)
                 → consₙ (headₙ xs p) (tailₙ xs p) ≡ xs
headₙ-tailₙ-consₙ {n} {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {n}) refl))
headₙ-tailₙ-consₙ (0∷ xs) p = let p' = contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p in
    begin
        consₙ (headₙ (0∷ xs) p) (tailₙ (0∷ xs) p)
    ≡⟨ refl ⟩
        consₙ (proj₁ (BLT.split (headₙ xs p'))) ((proj₂ (BLT.split (headₙ xs p'))) 1∷ tailₙ xs p')
    ≡⟨ refl ⟩
        0∷ (consₙ (Node ((proj₁ (BLT.split (headₙ xs p')))) ((proj₂ (BLT.split (headₙ xs p'))))) (tailₙ xs p'))
    ≡⟨ cong (λ x → 0∷ consₙ x (tailₙ xs p')) (BLT.split-merge (headₙ xs p')) ⟩
        0∷ consₙ (headₙ xs (p')) (tailₙ xs p')
    ≡⟨ cong 0∷_ (headₙ-tailₙ-consₙ xs p') ⟩
        0∷ xs
    ∎
headₙ-tailₙ-consₙ (x 1∷ xs) p = refl

head-tail-cons : ∀ {A} → (xs : 0-1-RAL A 0) → (p : ⟦ xs ⟧ ≢ 0)
               → cons (head xs p) (tail xs p) ≡ xs
head-tail-cons {A} [] p = ⊥-elim (p (⟦[]⟧≡0 ([] {A} {0}) refl))
head-tail-cons (0∷ xs) p = let p' = contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p in
    begin
        cons (head (0∷ xs) p) (tail (0∷ xs) p)
    ≡⟨ cong (λ x → consₙ x (proj₂ (BLT.split (headₙ xs p')) 1∷ tailₙ xs p')) (lemma (proj₁ (BLT.split (headₙ xs p')))) ⟩
        0∷ consₙ (Node (proj₁ (BLT.split (headₙ xs p'))) (proj₂ (BLT.split (headₙ xs p')))) (tailₙ xs p')
    ≡⟨ cong (λ x → 0∷ consₙ x (tailₙ xs p')) (BLT.split-merge (headₙ xs p')) ⟩
        0∷ consₙ (headₙ xs p') (tailₙ xs p')
    ≡⟨ cong 0∷_ (headₙ-tailₙ-consₙ xs p') ⟩
        0∷ xs
    ∎
    where
        lemma : ∀ {A} → (xs : BinaryLeafTree A 0) → Leaf (BLT.head xs) ≡ xs
        lemma (Leaf x) = refl
head-tail-cons (Leaf x 1∷ xs) p = refl

{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --without-K #-}

open import lib.Base

module lib.types.List where

data List {i} (A : Type i) : Type i where
  nil : List A
  _::_ : A → List A → List A

data HList {i} : List (Type i) → Type (lsucc i) where
  nil : HList nil
  _::_ : {A : Type i} {L : List (Type i)} → A → HList L → HList (A :: L)

hlist-curry-type : ∀ {i j} (L : List (Type i))
  (B : HList L → Type (lmax i j)) → Type (lmax i j)
hlist-curry-type nil B = B nil
hlist-curry-type {j = j} (A :: L) B =
  (x : A) → hlist-curry-type {j = j} L (λ xs → B (x :: xs))

hlist-curry : ∀ {i j} {L : List (Type i)} {B : HList L → Type (lmax i j)}
  (f : Π (HList L) B) → hlist-curry-type {j = j} L B
hlist-curry {L = nil} f = f nil
hlist-curry {L = A :: _} f = λ x → hlist-curry (λ xs → f (x :: xs))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Leftunit
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity

module Oscar.Class.Transleftidentity where

module Transleftidentity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  (ε : Reflexivity.type _∼_)
  (transitivity : Transitivity.type _∼_)
  = ℭLASS (_∼_ ,, (λ {x y} → _∼̇_ {x} {y}) ,, (λ {x} → ε {x}) ,, (λ {x y z} → transitivity {x} {y} {z}))
          (∀ {x y} {f : x ∼ y} → Leftunit.type _∼̇_ ε (flip transitivity) f)

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  {ε : Reflexivity.type _∼_}
  {transitivity : Transitivity.type _∼_}
  where
  transleftidentity = Transleftidentity.method _∼_ _∼̇_ ε transitivity

module Transleftidentity!
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  ⦃ _ : Reflexivity.class _∼_ ⦄
  ⦃ _ : Transitivity.class _∼_ ⦄
  = Transleftidentity (_∼_) (_∼̇_) reflexivity transitivity

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  ⦃ _ : Reflexivity.class _∼_ ⦄
  ⦃ _ : Transitivity.class _∼_ ⦄
  where
  transleftidentity! = Transleftidentity!.method _∼_ _∼̇_

module _ where

  transleftidentity[_] : ∀
    {𝔬} {𝔒 : Ø 𝔬}
    {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
    {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
    ⦃ _ : Reflexivity.class _∼_ ⦄
    ⦃ _ : Transitivity.class _∼_ ⦄
    ⦃ _ : Transleftidentity!.class _∼_ _∼̇_ ⦄
    → Transleftidentity!.type _∼_ _∼̇_
  transleftidentity[ _ ] = transleftidentity

module _ where

  open import Oscar.Data.Proposequality

  module ≡̇-Transleftidentity!
    {𝔬} {𝔒 : Ø 𝔬}
    {𝔣} (F : 𝔒 → Ø 𝔣)
    {𝔱} (T : {x : 𝔒} → F x → 𝔒 → Ø 𝔱)
    (let _∼_ : ∀ x y → Ø 𝔣 ∙̂ 𝔱
         _∼_ = λ x y → (f : F x) → T f y)
    ⦃ _ : Reflexivity.class _∼_ ⦄
    ⦃ _ : Transitivity.class _∼_ ⦄
    = Transleftidentity (_∼_) _≡̇_


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Bicategory.Construction.Spans.Properties where

open import Level

open import Data.Product using (_,_; _×_)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Reasoning.Setoid as SR
open import Function.Equality as SΠ renaming (id to ⟶-id)

open import Categories.Category
open import Categories.Category.Helper
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical

open import Categories.Diagram.Pullback

open import Categories.Bicategory
open import Categories.Bicategory.Monad

import Categories.Category.Diagram.Span as Span
import Categories.Bicategory.Construction.Spans as Spans

--------------------------------------------------------------------------------
-- Monads in the Bicategory of Spans are Categories

module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where

  private
    module T = Monad T

    open Span (Setoids (o ⊔ ℓ) ℓ)
    open Spans (pullback o ℓ)
    open Span⇒
    open Bicategory Spans

    open Setoid renaming (_≈_ to [_][_≈_])

  -- We can view the roof of the span as a hom set! However, we need to partition
  -- this big set up into small chunks with known domains/codomains.
  record Hom (X Y : Carrier T.C) : Set (o ⊔ ℓ) where
    field
      hom : Carrier (Span.M T.T)
      dom-eq : [ T.C ][ Span.dom T.T ⟨$⟩ hom ≈ X ]
      cod-eq : [ T.C ][ Span.cod T.T ⟨$⟩ hom ≈ Y ]

  open Hom

  private
    ObjSetoid : Setoid (o ⊔ ℓ) ℓ
    ObjSetoid = T.C

    HomSetoid : Setoid (o ⊔ ℓ) ℓ
    HomSetoid = Span.M T.T

    module ObjSetoid = Setoid ObjSetoid
    module HomSetoid = Setoid HomSetoid

    id⇒ : (X : Carrier T.C) → Hom X X
    id⇒ X = record
      { hom = arr T.η ⟨$⟩ X
      ; dom-eq = commute-dom T.η (refl T.C)
      ; cod-eq = commute-cod T.η (refl T.C)
      }

    _×ₚ_ : ∀ {A B C} → (f : Hom B C) → (g : Hom A B) → FiberProduct (Span.cod T.T) (Span.dom T.T)
    _×ₚ_ {B = B} f g = record
      { elem₁ = hom g
      ; elem₂ = hom f
      ; commute = begin
        Span.cod T.T ⟨$⟩ hom g ≈⟨ cod-eq g ⟩
        B                      ≈⟨ ObjSetoid.sym (dom-eq f) ⟩
        Span.dom T.T ⟨$⟩ hom f ∎
      }
      where
        open SR ObjSetoid

    _∘⇒_ : ∀ {A B C} (f : Hom B C) → (g : Hom A B) → Hom A C
    _∘⇒_ {A = A} {C = C} f g = record
      { hom = arr T.μ ⟨$⟩ (f ×ₚ g)
      ; dom-eq = begin
        Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ (commute-dom T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl)) ⟩
        Span.dom T.T ⟨$⟩ hom g                  ≈⟨ dom-eq g ⟩
        A                                       ∎
      ; cod-eq = begin
        Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl) ⟩
        Span.cod T.T ⟨$⟩ hom f                  ≈⟨ cod-eq f ⟩
        C                                       ∎
      }
      where
        open SR ObjSetoid

  SpanMonad⇒Category : Category (o ⊔ ℓ) (o ⊔ ℓ) ℓ
  SpanMonad⇒Category = categoryHelper record
    { Obj = Setoid.Carrier T.C
    ; _⇒_ = Hom
    ; _≈_ = λ f g → [ HomSetoid ][ hom f ≈ hom g ]
    ; id = λ {X} → id⇒ X
    ; _∘_ = _∘⇒_
    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} →
      let f×ₚ⟨g×ₚh⟩ = record
            { elem₁ = record
              { elem₁ = hom f
              ; elem₂ = hom g
              ; commute = FiberProduct.commute (g ×ₚ f)
              }
            ; elem₂ = hom h
            ; commute = FiberProduct.commute (h ×ₚ g)
            }
      in begin
        arr T.μ ⟨$⟩ ((h ∘⇒ g) ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl)) ⟩
        arr T.μ ⟨$⟩ _                ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} {f×ₚ⟨g×ₚh⟩} ((HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl) ⟩
        arr T.μ ⟨$⟩ _                ≈⟨ (cong (arr T.μ) (cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl)) ⟩
        arr T.μ ⟨$⟩ (h ×ₚ (g ∘⇒ f)) ∎
    ; identityˡ = λ {A} {B} {f} → begin
      arr T.μ ⟨$⟩ (id⇒ B ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.η) (ObjSetoid.sym (cod-eq f))) ⟩
      arr T.μ ⟨$⟩ _             ≈⟨ T.identityʳ HomSetoid.refl ⟩
      hom f                     ∎
    ; identityʳ = λ {A} {B} {f} → begin
      arr T.μ ⟨$⟩ (f ×ₚ id⇒ A) ≈⟨ cong (arr T.μ) (cong (arr T.η) (ObjSetoid.sym (dom-eq f)) , HomSetoid.refl) ⟩
      arr T.μ ⟨$⟩ _             ≈⟨ T.identityˡ HomSetoid.refl ⟩
      hom f                     ∎
    ; equiv = record
      { refl = HomSetoid.refl
      ; sym = HomSetoid.sym
      ; trans = HomSetoid.trans
      }
    ; ∘-resp-≈ = λ f≈h g≈i → cong (arr T.μ) (g≈i , f≈h)
    }
      where
        open SR HomSetoid


text:
{-# OPTIONS --rewriting --without-K #-}

open import Agda.Primitive
open import Prelude

{- Syntax for the Type theory for globular sets -}
module GSeTT.Syntax where

  data Pre-Ty : Set
  data Pre-Tm : Set

  data Pre-Ty where
    ∗ : Pre-Ty
    ⇒ : Pre-Ty → Pre-Tm → Pre-Tm → Pre-Ty

  data Pre-Tm where
    Var : ℕ → Pre-Tm

  Pre-Ctx : Set₁
  Pre-Ctx = list (ℕ × Pre-Ty)

  Pre-Sub : Set₁
  Pre-Sub = list (ℕ × Pre-Tm)

  ⇒= : ∀ {A B t t' u u'} → A == B → t == t' → u == u' → ⇒ A t u == ⇒ B t' u'
  ⇒= idp idp idp = idp

  =⇒ : ∀ {A B t t' u u'} → ⇒ A t u == ⇒ B t' u' → (A == B × t == t') × u == u'
  =⇒ idp = (idp , idp) , idp

  tgt= : ∀ {A B t t' u u'} → ⇒ A t u == ⇒ B t' u' →  u == u'
  tgt= idp = idp

  Var= : ∀ {v w} → v == w → Var v == Var w
  Var= idp = idp

  =Var : ∀ {v w} → Var v == Var w → v == w
  =Var idp = idp

  {- Dimension of a type and aof a context -}
  -- Careful: dimension of ∗ should be -1
  dim : Pre-Ty → ℕ
  dim ∗ = O
  dim (⇒ A t u) = S (dim A)

  -- Careful: dimension of the empty context should be -1
  dimC : Pre-Ctx → ℕ
  dimC nil = O
  dimC (Γ :: (x , A)) = max (dimC Γ) (dim A)

  {- Action of substitutions on types and terms on a syntactical level -}
  _[_]Pre-Ty : Pre-Ty → Pre-Sub → Pre-Ty
  _[_]Pre-Tm : Pre-Tm → Pre-Sub → Pre-Tm

  ∗ [ γ ]Pre-Ty = ∗
  ⇒ A t u [ γ ]Pre-Ty = ⇒ (A [ γ ]Pre-Ty) (t [ γ ]Pre-Tm) (u [ γ ]Pre-Tm)
  Var x [ nil ]Pre-Tm = Var x
  Var x [ γ :: (v , t) ]Pre-Tm = if x ≡ v then t else ((Var x) [ γ ]Pre-Tm)

  _∘_ : Pre-Sub → Pre-Sub → Pre-Sub
  nil ∘ γ = nil
  (γ :: (x , t)) ∘ δ = (γ ∘ δ) :: (x , (t [ δ ]Pre-Tm))

  {- Identity and canonical projection -}
  Pre-id : ∀ (Γ : Pre-Ctx) → Pre-Sub
  Pre-id nil = nil
  Pre-id (Γ :: (x , A)) = (Pre-id Γ) :: (x , Var x)

  Pre-π : ∀ (Γ : Pre-Ctx) (x : ℕ) (A : Pre-Ty) → Pre-Sub
  Pre-π Γ x A = Pre-id Γ

  {- The pairing (x#A) ∈ Γ  -}
  _#_∈_ : ℕ → Pre-Ty → Pre-Ctx → Set
  _ # _ ∈ nil = ⊥
  x # A ∈ (Γ :: (y , B)) = (x # A ∈ Γ) + ((x == y) × (A == B))

  _∈_ : ℕ → Pre-Ctx → Set
  _ ∈ nil = ⊥
  x ∈ (Γ :: (y , _)) = (x ∈ Γ) + (x == y)

  eqdec-PreCtx : eqdec Pre-Ctx
  eqdec-PreTy : eqdec Pre-Ty
  eqdec-PreTm : eqdec Pre-Tm

  eqdec-PreCtx nil nil = inl idp
  eqdec-PreCtx nil (_ :: _) = inr λ()
  eqdec-PreCtx (_ :: _) nil = inr λ()
  eqdec-PreCtx (Γ :: (n , A)) (Δ :: (m , B)) with eqdec-PreCtx Γ Δ | eqdecℕ n m | eqdec-PreTy A B
  ... | inl idp | inl idp | inl idp = inl idp
  ... | inl idp | inl idp | inr A≠B = inr λ Γ,A=Γ,B → A≠B (snd (=, (snd (=:: Γ,A=Γ,B))))
  ... | inl idp | inr n≠m | _ = inr λ Γ,A=Γ,B → n≠m (fst (=, (snd (=:: Γ,A=Γ,B))))
  ... | inr Γ≠Δ | _ | _ = inr λ{idp → Γ≠Δ idp}

  eqdec-PreTy ∗ ∗ = inl idp
  eqdec-PreTy ∗ (⇒ _ _ _) = inr λ()
  eqdec-PreTy (⇒ _ _ _) ∗ = inr λ()
  eqdec-PreTy (⇒ A t u) (⇒ B v w) with eqdec-PreTy A B | eqdec-PreTm t v | eqdec-PreTm u w
  ... | inl idp | inl idp | inl idp = inl idp
  ... | inl idp | inl idp | inr u≠w = inr λ A=B → u≠w (snd (=⇒ A=B))
  ... | inl idp | inr t≠v | _ = inr λ A=B → t≠v (snd (fst (=⇒ A=B)))
  ... | inr A≠B | _ | _ = inr λ{idp → A≠B idp}

  eqdec-PreTm (Var a) (Var b) with eqdecℕ a b
  ... | inl idp = inl idp
  ... | inr a≠b = inr λ{idp → a≠b idp}

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Unary using ( _∈_ ; _∉_ ; _⊆_ )
open import Web.Semantic.DL.Concept.Model using
  ( _⟦_⟧₁ ; ⟦⟧₁-resp-≈ ; ⟦⟧₁-resp-≃; ⟦⟧₁-refl-≃ )
open import Web.Semantic.DL.Role.Model using
  ( _⟦_⟧₂ ; ⟦⟧₂-resp-≈ ; ⟦⟧₂-resp-≃ ; ⟦⟧₂-refl-≃ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; Axioms ; ε ; _,_ ;_⊑₁_ ; _⊑₂_ ; Dis ; Ref ; Irr ; Tra )
open import Web.Semantic.DL.TBox.Interp using ( Interp )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( _≃_ ; ≃-sym )
open import Web.Semantic.Util using ( True ; tt ; _∘_ )

module Web.Semantic.DL.TBox.Model {Σ : Signature} where

infixr 2 _⊨t_

_⊨t_ : Interp Σ → TBox Σ → Set
I ⊨t ε         = True
I ⊨t (T , U)   = (I ⊨t T) × (I ⊨t U)
I ⊨t (C ⊑₁ D)  = I ⟦ C ⟧₁ ⊆ I ⟦ D ⟧₁
I ⊨t (Q ⊑₂ R)  = I ⟦ Q ⟧₂ ⊆ I ⟦ R ⟧₂
I ⊨t (Dis Q R) = ∀ {xy} → (xy ∈ I ⟦ Q ⟧₂) → (xy ∉ I ⟦ R ⟧₂)
I ⊨t (Ref R)   = ∀ x → ((x , x) ∈ I ⟦ R ⟧₂)
I ⊨t (Irr R)   = ∀ x → ((x , x) ∉ I ⟦ R ⟧₂)
I ⊨t (Tra R)   = ∀ {x y z} →
  ((x , y) ∈ I ⟦ R ⟧₂) → ((y , z) ∈ I ⟦ R ⟧₂) → ((x , z) ∈ I ⟦ R ⟧₂)

Axioms✓ : ∀ I T {t} → (t ∈ Axioms T) → (I ⊨t T) → (I ⊨t t)
Axioms✓ I ε         ()         I⊨T
Axioms✓ I (T , U)   (inj₁ t∈T) (I⊨T , I⊨U) = Axioms✓ I T t∈T I⊨T
Axioms✓ I (T , U)   (inj₂ t∈U) (I⊨T , I⊨U) = Axioms✓ I U t∈U I⊨U
Axioms✓ I (C ⊑₁ D)  refl       I⊨T         = I⊨T
Axioms✓ I (Q ⊑₂ R)  refl       I⊨T         = I⊨T
Axioms✓ I (Dis Q R) refl       I⊨T         = I⊨T
Axioms✓ I (Ref R)   refl       I⊨T         = I⊨T
Axioms✓ I (Irr R)   refl       I⊨T         = I⊨T
Axioms✓ I (Tra R)   refl       I⊨T         = I⊨T

⊨t-resp-≃ : ∀ {I J : Interp Σ} → (I ≃ J) → ∀ T → (I ⊨t T) → (J ⊨t T)
⊨t-resp-≃ {I} {J} I≃J ε _ =
  tt
⊨t-resp-≃ {I} {J} I≃J (T , U) (I⊨T , I⊨U) =
  (⊨t-resp-≃ I≃J T I⊨T , ⊨t-resp-≃ I≃J U I⊨U)
⊨t-resp-≃ {I} {J} I≃J (C ⊑₁ D) I⊨C⊑D =
  ⟦⟧₁-refl-≃ I≃J D ∘ I⊨C⊑D ∘ ⟦⟧₁-resp-≃ (≃-sym I≃J) C
⊨t-resp-≃ {I} {J} I≃J (Q ⊑₂ R) I⊨Q⊑R = ⟦⟧₂-refl-≃ I≃J R ∘ I⊨Q⊑R ∘
  ⟦⟧₂-resp-≃ (≃-sym I≃J) Q
⊨t-resp-≃ {I} {J} I≃J (Dis Q R) I⊨DisQR = λ xy∈⟦Q⟧ xy∈⟦R⟧ →
  I⊨DisQR (⟦⟧₂-resp-≃ (≃-sym I≃J) Q xy∈⟦Q⟧) (⟦⟧₂-resp-≃ (≃-sym I≃J) R xy∈⟦R⟧)
⊨t-resp-≃ {I} {J} I≃J (Ref R) I⊨RefR = λ x → ⟦⟧₂-refl-≃ I≃J R (I⊨RefR _)
⊨t-resp-≃ {I} {J} I≃J (Irr R) I⊨IrrR = λ x xx∈⟦R⟧ →
  I⊨IrrR _ (⟦⟧₂-resp-≃ (≃-sym I≃J) R xx∈⟦R⟧)
⊨t-resp-≃ {I} {J} I≃J (Tra R) I⊨TraR = λ xy∈⟦R⟧ yz∈⟦R⟧ →
  ⟦⟧₂-refl-≃ I≃J R (I⊨TraR
    (⟦⟧₂-resp-≃ (≃-sym I≃J) R xy∈⟦R⟧)
    (⟦⟧₂-resp-≃ (≃-sym I≃J) R yz∈⟦R⟧))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
-- Andreas, 2017-01-13, regression introduced by the fix of #1899
-- test case and report by Nisse

-- {-# OPTIONS -v term:40 #-}

open import Agda.Builtin.Size

mutual

  D : Size → Set
  D i = D′ i

  record D′ (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → D j

test : D′ ω
D′.force test = test

-- Same without sizes (they are not used)

mutual
  E = E'
  record E' : Set where
    coinductive
    field force : E

testE : E'
E'.force testE = testE

-- Both should succeed, no termination errors.

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
{-# OPTIONS --without-K #-}

module PInj where

open import Codata.Delay renaming (length to dlength ; map to dmap )
open import Codata.Thunk

open import Relation.Binary.PropositionalEquality

open import Size
open import Level
open import Data.Product

-- A pair of partial functions that are supposed to form a partial bijection.
record _⊢_⇔_ (i : Size) {ℓ : Level} (A : Set ℓ) (B : Set ℓ) : Set ℓ where
  constructor pre-pinj-i
  field
    forward  : A -> Delay B i
    backward : B -> Delay A i

open _⊢_⇔_

max_stars_repo_name: kztk-m/sparcl-agda

max_issues_repo_name: kztk-m/sparcl-agda

max_forks_repo_name: kztk-m/sparcl-agda