text:
module Oscar.Prelude where

module _ where -- Objectevel

  open import Agda.Primitive public
    using ()
    renaming ( Level to Ł
             ; lzero to ∅̂
             ; lsuc to ↑̂_
             ; _⊔_ to _∙̂_ )

  infix 0 Ø_
  Ø_ : ∀ 𝔬 → Set (↑̂ 𝔬)
  Ø_ 𝔬 = Set 𝔬

  Ø₀ = Ø ∅̂
  Ø₁ = Ø (↑̂ ∅̂)

postulate
  magic : ∀ {a} {A : Ø a} → A

module _ where -- Function

  infixr 9 _∘_
  _∘_ : ∀ {a b c}
          {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
          (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
          ((x : A) → C (g x))
  f ∘ g = λ x → f (g x)

  infixr 9 _∘′_
  _∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
           (B → C) → (A → B) → (A → C)
  f ∘′ g = f ∘ g

  ¡ : ∀ {𝔬} {𝔒 : Ø 𝔬} → 𝔒 → 𝔒
  ¡ 𝓞 = 𝓞

  infixl -10 ¡
  syntax ¡ {𝔒 = A} x = x ofType A

  ¡[_] : ∀ {𝔬} (𝔒 : Ø 𝔬) → 𝔒 → 𝔒
  ¡[ _ ] = ¡

  _∋_ : ∀ {a} (A : Set a) → A → A
  A ∋ x = x

  _∞ : ∀ {a} {A : Set a} → A → ∀ {b} {B : Set b} → B → A
  _∞ x = λ _ → x

  _∞⟦_⟧ : ∀ {a} {A : Set a} → A → ∀ {b} (B : Set b) → B → A
  x ∞⟦ B ⟧ = _∞ x {B = B}

  _∞₁ : ∀ ..{a} ..{A : Set a} → A → ∀ ..{b} ..{B : Set b} → ∀ ..{h} ..{H : Set h} → .(_ : B) .{_ : H} → A
  _∞₁ f _ = f

  _∞₃ : ∀ ..{a} ..{A : Set a} → A → ∀ ..{b} ..{B : Set b} → ∀ ..{h₁ h₂ h₃} ..{H₁ : Set h₁} ..{H₂ : Set h₂} ..{H₃ : Set h₃} → .(_ : B) .{_ : H₁} .{_ : H₂} .{_ : H₃} → A
  _∞₃ f _ = f

  hid : ∀ {a} {A : Set a} {x : A} → A
  hid {x = x} = x

  it : ∀ {a} {A : Set a} {{x : A}} → A
  it {{x}} = x
  {-# INLINE it #-}

  ! = it

  asInstance : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ {{x}} → B x) → B x
  asInstance x f = f {{x}}
  {-# INLINE asInstance #-}

  flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} → (∀ x y → C x y) → ∀ y x → C x y
  flip f x y = f y x
  {-# INLINE flip #-}

  infixr -20 _$_
  _$_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
  f $ x = f x

  infixr -20 _$′_
  _$′_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → A → B
  f $′ x = f x

  -- The S combinator. (Written infix as in Conor McBride's paper
  -- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
  -- and evaluation".)

  _ˢ_ : ∀ {a b c}
          {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
        ((x : A) (y : B x) → C x y) →
        (g : (x : A) → B x) →
        ((x : A) → C x (g x))
  f ˢ g = λ x → f x (g x)

  infixr 0 case_of_ case_return_of_

  case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
  case x of f = f x

  case_return_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
  case x return B of f = f x

  infixl 8 _on_
  _on_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x y → B x → B y → Set c} →
           (∀ {x y} (z : B x) (w : B y) → C x y z w) → (f : ∀ x → B x) → ∀ x y →
           C x y (f x) (f y)
  h on f = λ x y → h (f x) (f y)
  {-# INLINE _on_ #-}

Function : ∀ {a} → Ø a → Ø a → Ø a
Function A B = A → B

Function⟦_⟧ : ∀ a → Ø a → Ø a → Ø a
Function⟦ a ⟧ = Function {a = a}

MFunction : ∀ {a b} (M : Ø a → Ø b) → Ø a → Ø a → Ø b
MFunction M A B = M A → M B

Arrow : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔞} {𝔟} → (𝔛 → Ø 𝔞) → (𝔛 → Ø 𝔟) → 𝔛 → 𝔛 → Ø 𝔞 ∙̂ 𝔟
Arrow 𝔄 𝔅 x y = 𝔄 x → 𝔅 y

module _ where

  Extension : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) → 𝔒 → 𝔒 → Ø 𝔭
  Extension 𝔓 = Arrow 𝔓 𝔓

module _ where

  _⟨_⟩→_ : ∀ {𝔬} {𝔒 : Ø 𝔬} → 𝔒 → ∀ {𝔭} → (𝔒 → Ø 𝔭) → 𝔒 → Ø 𝔭
  m ⟨ 𝔓 ⟩→ n = Extension 𝔓 m n

π̂ : ∀ {𝔵} ℓ (𝔛 : Ø 𝔵) → Ø 𝔵 ∙̂ ↑̂ ℓ
π̂ ℓ 𝔛 = 𝔛 → Ø ℓ

infixl 21 _←̂_
_←̂_ = π̂

π̇ : ∀ {𝔞 𝔟} (𝔄 : Ø 𝔞) (𝔅 : 𝔄 → Ø 𝔟) → Ø 𝔞 ∙̂ 𝔟
π̇ 𝔄 𝔅 = (𝓐 : 𝔄) → 𝔅 𝓐

infixl 20 π̇
syntax π̇ 𝔄 (λ 𝓐 → 𝔅𝓐) = 𝔅𝓐 ← 𝓐 ≔ 𝔄

π̇-hidden-quantifier-syntax = π̇
infixl 20 π̇-hidden-quantifier-syntax
syntax π̇-hidden-quantifier-syntax 𝔄 (λ _ → 𝔅𝓐) = 𝔅𝓐 ← 𝔄

π̂² : ∀ {𝔞} ℓ → Ø 𝔞 → Ø 𝔞 ∙̂ ↑̂ ℓ
π̂² ℓ 𝔄 = ℓ ←̂ 𝔄 ← 𝔄

_→̂²_ : ∀ {𝔞} → Ø 𝔞 → ∀ ℓ → Ø 𝔞 ∙̂ ↑̂ ℓ
_→̂²_ 𝔒 ℓ = π̂² ℓ 𝔒

record Lift {a ℓ} (A : Set a) : Set (a ∙̂ ℓ) where
  instance constructor lift
  field lower : A

open Lift public

record Wrap {𝔵} (𝔛 : Ø 𝔵) : Ø 𝔵 where
  constructor ∁
  field
    π₀ : 𝔛

open Wrap public

∀̇ : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔞}
  → (∀ ℓ (𝔄 : Ø 𝔞) → Ø 𝔞 ∙̂ ↑̂ ℓ)
  → ∀ ℓ → (𝔛 → Ø 𝔞) → Ø 𝔵 ∙̂ 𝔞 ∙̂ ↑̂ ℓ
∀̇ Q ℓ 𝔄 = ∀ {x} → Q ℓ (𝔄 x)

Ṙelation : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔞} ℓ → (𝔞 ←̂ 𝔛) → Ø 𝔵 ∙̂ 𝔞 ∙̂ ↑̂ ℓ
Ṙelation ℓ P = Wrap (∀̇ π̂² ℓ P)

Pointwise : ∀ {𝔞} {𝔄 : Ø 𝔞} {𝔟} {𝔅 : Ø 𝔟} {ℓ} → 𝔅 →̂² ℓ → (𝔅 ← 𝔄) → (𝔄 → 𝔅) → Ø 𝔞 ∙̂ ℓ
Pointwise _≈_ = λ f g → ∀ x → f x ≈ g x

Ṗroperty : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔬} ℓ → (𝔵 ∙̂ 𝔬 ∙̂ ↑̂ ℓ) ←̂ (𝔬 ←̂ 𝔛)
Ṗroperty ℓ P = Wrap (∀̇ π̂ ℓ P)

LeftṖroperty : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔶} {𝔜 : 𝔛 → Ø 𝔶} {𝔯} → ∀ ℓ → ((x : 𝔛) → 𝔜 x → Ø 𝔯) → 𝔛 → Ø 𝔶 ∙̂ 𝔯 ∙̂ ↑̂ ℓ
LeftṖroperty ℓ _↦_ = Ṗroperty ℓ ∘ _↦_

ArrowṖroperty : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔭₁ 𝔭₂} → ∀ ℓ → (𝔛 → Ø 𝔭₁) → (𝔛 → Ø 𝔭₂) → 𝔛 → Ø 𝔵 ∙̂ 𝔭₁ ∙̂ 𝔭₂ ∙̂ ↑̂ ℓ
ArrowṖroperty ℓ 𝔒₁ 𝔒₂ = LeftṖroperty ℓ (Arrow 𝔒₁ 𝔒₂)

module _ where

  infixr 5 _,_
  record Σ {𝔬} (𝔒 : Ø 𝔬) {𝔭} (𝔓 : 𝔒 → Ø 𝔭) : Ø 𝔬 ∙̂ 𝔭 where
    instance constructor _,_
    field
      π₀ : 𝔒
      π₁ : 𝔓 π₀

  open Σ public

  infixr 5 _,,_
  record Σ′ {𝔬} (𝔒 : Ø 𝔬) {𝔭} (𝔓 : Ø 𝔭) : Ø 𝔬 ∙̂ 𝔭 where
    instance constructor _,,_
    field
      π₀ : 𝔒
      π₁ : 𝔓

  open Σ′ public

  _×_ : ∀ {𝔬₁ 𝔬₂} (𝔒₁ : Ø 𝔬₁) (𝔒₂ : Ø 𝔬₂) → Ø 𝔬₁ ∙̂ 𝔬₂
  _×_ O₁ O₂ = Σ O₁ (λ _ → O₂)

  ∃_ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) → Ø 𝔬 ∙̂ 𝔭
  ∃_ = Σ _

  uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} →
              (∀ x (y : B x) → C x y) → (p : Σ A B) → C (π₀ p) (π₁ p)
  uncurry f (x , y) = f x y

  uncurry′ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c} →
              (∀ x → B x → C) → Σ A B → C
  uncurry′ f (x , y) = f x y

  curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
            (∀ p → C p) → ∀ x (y : B x) → C (x , y)
  curry f x y = f (x , y)

ExtensionṖroperty : ∀ {𝔵} {𝔛 : Ø 𝔵} {𝔬} {ℓ̇}
  ℓ (𝔒 : 𝔛 → Ø 𝔬) (_↦_ : ∀̇ π̂² ℓ̇ 𝔒)
  → Ø 𝔵 ∙̂ 𝔬 ∙̂ ↑̂ ℓ ∙̂ ℓ̇
ExtensionṖroperty ℓ 𝔒 _↦_ = Σ (Ṗroperty ℓ 𝔒) (λ P → ∀ {x} {f g : 𝔒 x} → f ↦ g → Extension (π₀ P) f g)

LeftExtensionṖroperty : ∀ {𝔶} {𝔜 : Ø 𝔶} {𝔵} {𝔛 : 𝔜 → Ø 𝔵} {𝔬} {ℓ̇}
  ℓ (𝔒 : (y : 𝔜) → 𝔛 y → Ø 𝔬) (_↦_ : ∀ {y} → ∀̇ π̂² ℓ̇ (𝔒 y))
  → 𝔜
  → Ø 𝔵 ∙̂ 𝔬 ∙̂ ↑̂ ℓ ∙̂ ℓ̇
LeftExtensionṖroperty ℓ 𝔒 _↦_ y = ExtensionṖroperty ℓ (𝔒 y) _↦_

ArrowExtensionṖroperty : ∀
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔬₁} ℓ (𝔒₁ : 𝔛 → Ø 𝔬₁)
  {𝔬₂} (𝔒₂ : 𝔛 → Ø 𝔬₂)
  → ∀ {ℓ̇} (_↦_ : ∀̇ π̂² ℓ̇ 𝔒₂)
  → 𝔛
  → Ø 𝔵 ∙̂ 𝔬₁ ∙̂ 𝔬₂ ∙̂ ↑̂ ℓ ∙̂ ℓ̇
ArrowExtensionṖroperty ℓ 𝔒₁ 𝔒₂ _↦_ = LeftExtensionṖroperty ℓ (Arrow 𝔒₁ 𝔒₂) (Pointwise _↦_)

record Instance {a} (A : Set a) : Set a where
  constructor ∁
  field {{x}} : A

mkInstance : ∀ {a} {A : Set a} → A → Instance A
mkInstance x = ∁ {{x}}

ext: agda


text:
{-# OPTIONS --cubical --postfix-projections --safe #-}

open import Relation.Binary
open import Prelude hiding (tt)

module Data.List.Sort.InsertionSort {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open import Relation.Binary.Construct.LowerBound totalOrder
open import Data.List.Sort.Sorted totalOrder

open TotalOrder totalOrder renaming (refl to refl-≤)
open TotalOrder lb-ord renaming (≤-trans to ⌊trans⌋) using ()

open import Data.List
open import Data.Unit.UniversePolymorphic as Poly using (tt)
open import Data.List.Relation.Binary.Permutation
open import Function.Isomorphism
open import Data.Fin
open import Data.List.Membership

private variable lb : ⌊∙⌋

insert : E → List E → List E
insert x [] = x ∷ []
insert x (y ∷ xs) with x ≤ᵇ y
... | true  = x ∷ y ∷ xs
... | false = y ∷ insert x xs

insert-sort : List E → List E
insert-sort = foldr insert []

insert-sorts : ∀ x xs → lb ⌊≤⌋ ⌊ x ⌋ → SortedFrom lb xs → SortedFrom lb (insert x xs)
insert-sorts x [] lb≤x Pxs = lb≤x , tt
insert-sorts x (y ∷ xs) lb≤x (lb≤y , Sxs) with x ≤? y
... | yes x≤y = lb≤x , x≤y , Sxs
... | no  x≰y = lb≤y , insert-sorts x xs (<⇒≤ (≰⇒> x≰y)) Sxs

sort-sorts : ∀ xs → Sorted (insert-sort xs)
sort-sorts [] = tt
sort-sorts (x ∷ xs) = insert-sorts x (insert-sort xs) tt (sort-sorts xs)

insert-perm : ∀ x xs → insert x xs ↭ x ∷ xs
insert-perm x [] = reflₚ
insert-perm x (y ∷ xs) with x ≤ᵇ y
... | true  = consₚ x reflₚ
... | false = consₚ y (insert-perm x xs) ⟨ transₚ ⟩ swapₚ y x xs

sort-perm : ∀ xs → insert-sort xs ↭ xs
sort-perm [] = reflₚ {xs = []}
sort-perm (x ∷ xs) = insert-perm x (insert-sort xs) ⟨ transₚ {xs = insert x (insert-sort xs)} ⟩ consₚ x (sort-perm xs)

perm-invar : ∀ xs ys → xs ↭ ys → insert-sort xs ≡ insert-sort ys
perm-invar xs ys xs⇔ys =
  perm-same
    (insert-sort xs)
    (insert-sort ys)
    (sort-sorts xs)
    (sort-sorts ys)
    (λ k → sort-perm xs k ⟨ trans-⇔ ⟩ xs⇔ys k ⟨ trans-⇔ ⟩ sym-⇔ (sort-perm ys k))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- We only translate definition with one clause
------------------------------------------------------------------------------

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

module OnlyOneClause where

infixl 9 _+_
infix  7 _≡_

data ℕ : Set where
  zero :     ℕ
  succ : ℕ → ℕ

data _≡_ (n : ℕ) : ℕ → Set where
  refl : n ≡ n

_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)
{-# ATP definition _+_ #-}

postulate +-comm : ∀ m n → m + n ≡ n + m
{-# ATP prove +-comm #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module 015-logic where

-- Simple propositional logic.

open import 010-false-true

-- Logical and. We represent a proof of A and B as a pair of proofs,
-- namely, a proof of A and a proof of B.

data Pair (A B : Set) : Set where
  _,_ : A -> B -> Pair A B

_∧_ : (A B : Set) -> Set
A ∧ B = Pair A B

-- Get back proof of any of the components.

a∧b->a : {A B : Set} -> A ∧ B -> A
a∧b->a (a , b) = a

a∧b->b : {A B : Set} -> A ∧ B -> B
a∧b->b (a , b) = b

-- Logical or. We represent a proof of A or B as a proof of A or a
-- proof of B.

data Either (A B : Set) : Set where
  left : A -> Either A B
  right : B -> Either A B

_∨_ : (A B : Set) -> Set
A ∨ B = Either A B

-- Negation.

¬_ : (A : Set) -> Set
¬ A = A -> False

-- Now some properties.

-- Commutativity.

a∧b->b∧a : ∀ {A B} -> A ∧ B -> B ∧ A
a∧b->b∧a ( a , b ) = ( b , a )

a∨b->b∨a : ∀ {A B} -> A ∨ B -> B ∨ A
a∨b->b∨a (left a) = right a
a∨b->b∨a (right b) = left b

-- Distributivity.

a∧[b∨c]->[a∧b]∨[a∧c] : ∀ {A B C} -> A ∧ (B ∨ C) -> (A ∧ B) ∨ (A ∧ C)
a∧[b∨c]->[a∧b]∨[a∧c] (a , left b) = left (a , b)
a∧[b∨c]->[a∧b]∨[a∧c] (a , right c) = right (a , c)

[a∧b]∨[a∧c]->a∧[b∨c] : ∀ {A B C} -> (A ∧ B) ∨ (A ∧ C) -> A ∧ (B ∨ C)
[a∧b]∨[a∧c]->a∧[b∨c] (left (a , b)) = (a , left b)
[a∧b]∨[a∧c]->a∧[b∨c] (right (a , c)) = (a , right c)

a∨[b∧c]->[a∨b]∧[a∨c] : ∀ {A B C} -> A ∨ (B ∧ C) -> (A ∨ B) ∧ (A ∨ C)
a∨[b∧c]->[a∨b]∧[a∨c] (left a) = (left a , left a)
a∨[b∧c]->[a∨b]∧[a∨c] (right (b , c)) = (right b , right c)

[a∨b]∧[a∨c]->a∨[b∧c] : ∀ {A B C} -> (A ∨ B) ∧ (A ∨ C) -> A ∨ (B ∧ C)
[a∨b]∧[a∨c]->a∨[b∧c] ( left a , _ ) = left a
[a∨b]∧[a∨c]->a∨[b∧c] ( _ , left a ) = left a
[a∨b]∧[a∨c]->a∨[b∧c] ( right b , right c ) = right (b , c)

-- Contraposition.

[a->b]->[¬b->¬a] : ∀ {A B} -> (A -> B) -> (¬ B -> ¬ A)
[a->b]->[¬b->¬a] a->b ¬b a = ¬b (a->b a)

-- Contradiction.

¬[a∧¬a] : ∀ {A} -> ¬ (A ∧ (¬ A))
¬[a∧¬a] ( a , ¬a ) = ¬a a

-- De Morgan.

¬[a∨b]->¬a∧¬b : ∀ {A B} -> ¬ (A ∨ B) -> (¬ A) ∧ (¬ B)
¬[a∨b]->¬a∧¬b ¬[a∨b] = (\a -> ¬[a∨b] (left a)) , (\b -> ¬[a∨b] (right b))

¬a∧¬b->¬[a∨b] : ∀ {A B} -> (¬ A) ∧ (¬ B) -> ¬ (A ∨ B)
¬a∧¬b->¬[a∨b] ( ¬a , ¬b ) (left a) =  ¬a a
¬a∧¬b->¬[a∨b] ( ¬a , ¬b ) (right b) =  ¬b b

¬a∨¬b->¬[a∧b] : ∀ {A B} -> (¬ A) ∨ (¬ B) -> ¬ (A ∧ B)
¬a∨¬b->¬[a∧b] (left ¬a) ( a , b ) = ¬a a
¬a∨¬b->¬[a∧b] (right ¬b) ( a , b ) = ¬b b

-- not provable, see https://math.stackexchange.com/questions/120187/does-de-morgans-laws-hold-in-propositional-intuitionistic-logic
-- ¬[a∧b]->¬a∨¬b : ∀ {A B} -> ¬ (A ∧ B) -> (¬ A) ∨ (¬ B)
-- ¬[a∧b]->¬a∨¬b ¬[a∧b] = {!!}

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax QIO

type
  T : 0-ary
  P : 0-ary

term
  new      : P.T  ->  T
  measure  : P  T  T  ->  T
  applyX   : P  P.T  ->  T
  applyI2  : P  P.T  ->  T
  applyDuv : P  P  (P,P).T  ->  T
  applyDu  : P  P.T  ->  T
  applyDv  : P  P.T  ->  T

theory
  (A) a:P   t u:T         |> applyX (a, b.measure(b, t, u)) = measure(a, u, t)
  (B) a:P   b:P  t u:P.T  |> measure(a, applyDu(b, b.t[b]), applyDv(b, b.u[b])) = applyDuv(a, b, a b.measure(a, t[b], u[b]))
  (D) t u:T               |> new(a.measure(a, t, u)) = t
  (E) b:P  t:(P, P).T     |> new(a.applyDuv(a, b, a b. t[a,b])) = applyDu(b, b.new(a.t[a,b]))
-}

module QIO.Signature where

open import SOAS.Context

-- Type declaration
data QIOT : Set where
  T : QIOT
  P : QIOT

open import SOAS.Syntax.Signature QIOT public
open import SOAS.Syntax.Build QIOT public

-- Operator symbols
data QIOₒ : Set where
  newₒ measureₒ applyXₒ applyI2ₒ applyDuvₒ applyDuₒ applyDvₒ : QIOₒ

-- Term signature
QIO:Sig : Signature QIOₒ
QIO:Sig = sig λ
  {  newₒ       → (P ⊢₁ T) ⟼₁ T
  ;  measureₒ   → (⊢₀ P) , (⊢₀ T) , (⊢₀ T) ⟼₃ T
  ;  applyXₒ    → (⊢₀ P) , (P ⊢₁ T) ⟼₂ T
  ;  applyI2ₒ   → (⊢₀ P) , (P ⊢₁ T) ⟼₂ T
  ;  applyDuvₒ  → (⊢₀ P) , (⊢₀ P) , (P , P ⊢₂ T) ⟼₃ T
  ;  applyDuₒ   → (⊢₀ P) , (P ⊢₁ T) ⟼₂ T
  ;  applyDvₒ   → (⊢₀ P) , (P ⊢₁ T) ⟼₂ T
  }

open Signature QIO:Sig public


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Dagger.Instance.Rels where

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Level

open import Categories.Category.Dagger
open import Categories.Category.Instance.Rels

RelsHasDagger : ∀ {o ℓ} → HasDagger (Rels o ℓ)
RelsHasDagger = record
  { _† = flip
  ; †-identity = (lift ∘ sym ∘ lower) , (lift ∘ sym ∘ lower)
  ; †-homomorphism = (map₂ swap) , (map₂ swap)
  ; †-resp-≈ = λ p → (proj₁ p) , (proj₂ p) -- it's the implicits that need flipped
  ; †-involutive = λ _ → id , id
  }

RelsDagger : ∀ o ℓ → DaggerCategory (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ)
RelsDagger o ℓ = record
  { C = Rels o ℓ
  ; hasDagger = RelsHasDagger
  }

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:
{-# OPTIONS --universe-polymorphism #-}
{-# OPTIONS --universe-polymorphism #-}
open import Level
open import Categories.Category
open import Categories.Product

-- Parameterize over the categories in whose product we are working
module Categories.Product.Properties
    {o ℓ e o′ ℓ′ e′}
    (C : Category o ℓ e)
    (D : Category o′ ℓ′ e′)
    where

C×D : Category _ _ _
C×D = Product C D
module C×D = Category C×D

import Categories.Product.Projections
open Categories.Product.Projections C D

open import Categories.Functor

open import Relation.Binary using (module IsEquivalence)
open import Relation.Binary.PropositionalEquality as PropEq
    using ()
    renaming (_≡_ to _≣_)

∏₁※∏₂≣id : (∏₁ ※ ∏₂) ≣ id
∏₁※∏₂≣id = PropEq.refl

∏₁※∏₂-identity : (∏₁ ※ ∏₂) ≡ id
∏₁※∏₂-identity h = refl
    where open Heterogeneous C×D

※-distrib' :
    ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
    → {A : Category o₁ ℓ₁ e₁}
    → {B : Category o₂ ℓ₂ e₂}
    → {F : Functor B C}
    → {G : Functor B D}
    → {H : Functor A B}
    → ((F ∘ H) ※ (G ∘ H)) ≣ ((F ※ G) ∘ H)
※-distrib' = PropEq.refl

※-distrib :
    ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
    → {A : Category o₁ ℓ₁ e₁}
    → {B : Category o₂ ℓ₂ e₂}
    → (F : Functor B C)
    → (G : Functor B D)
    → (H : Functor A B)
    → ((F ∘ H) ※ (G ∘ H)) ≡ ((F ※ G) ∘ H)
※-distrib F G H h = refl
    where open Heterogeneous C×D

∏₁※∏₂-distrib :
    ∀ {o₁ ℓ₁ e₁}{A : Category o₁ ℓ₁ e₁}
    → (F : Functor A C×D)
    → ((∏₁ ∘ F) ※ (∏₂ ∘ F)) ≡ F
∏₁※∏₂-distrib F h = refl
    where open Heterogeneous C×D

module Lemmas where
    open Heterogeneous C×D
    open import Data.Product

    lem₁ : {x₁ y₁ x₂ y₂ : Category.Obj C}
        → {x₃ y₃ : Category.Obj D}
        → (f₁ : C [ x₁ , y₁ ])
        → (f₂ : C [ x₂ , y₂ ])
        → (g : D [ x₃ , y₃ ])
        → C   [ f₁ ∼ f₂ ]
        → C×D [ (f₁ , g) ∼ (f₂ , g) ]
    lem₁ f₁ f₂ g (≡⇒∼ f₁≡f₂) = ≡⇒∼ (f₁≡f₂ , Category.Equiv.refl D)

    lem₂ : {x₁ y₁ x₂ y₂ : Category.Obj D}
        → {x₃ y₃ : Category.Obj C}
        → (f : C [ x₃ , y₃ ])
        → (g₁ : D [ x₁ , y₁ ])
        → (g₂ : D [ x₂ , y₂ ])
        → D   [ g₁ ∼ g₂ ]
        → C×D [ (f , g₁) ∼ (f , g₂) ]
    lem₂ f g₁ g₂ (≡⇒∼ g₁≡g₂) = ≡⇒∼ (Category.Equiv.refl C , g₁≡g₂)
open Lemmas

※-preserves-≡ˡ :
    ∀ {o₁ ℓ₁ e₁}
    → {A : Category o₁ ℓ₁ e₁}
    → (F₁ : Functor A C)
    → (F₂ : Functor A C)
    → (G  : Functor A D)
    → (F₁ ≡ F₂) → ((F₁ ※ G) ≡ (F₂ ※ G))
※-preserves-≡ˡ F₁ F₂ G F₁≡F₂ h =
    lem₁ (Functor.F₁ F₁ h) (Functor.F₁ F₂ h) (Functor.F₁ G  h) (F₁≡F₂ h)

※-preserves-≡ʳ :
    ∀ {o₁ ℓ₁ e₁}
    → {A : Category o₁ ℓ₁ e₁}
    → (F  : Functor A C)
    → (G₁ : Functor A D)
    → (G₂ : Functor A D)
    → (G₁ ≡ G₂) → ((F ※ G₁) ≡ (F ※ G₂))
※-preserves-≡ʳ F G₁ G₂ G₁≡G₂ h =
    lem₂ (Functor.F₁ F h) (Functor.F₁ G₁ h) (Functor.F₁ G₂ h) (G₁≡G₂ h)
    where open Heterogeneous C×D

.※-preserves-≡ :
    ∀ {o₁ ℓ₁ e₁}
    → {A : Category o₁ ℓ₁ e₁}
    → (F : Functor A C)
    → (G : Functor A C)
    → (H : Functor A D)
    → (I : Functor A D)
    → (F ≡ G) → (H ≡ I) → ((F ※ H) ≡ (G ※ I))
※-preserves-≡ {A = A} F G H I F≡G H≡I
    = trans {i = F ※ H}{j = G ※ H}{k = G ※ I}
        (※-preserves-≡ˡ F G H F≡G)
        (※-preserves-≡ʳ G H I H≡I)
    where open IsEquivalence (equiv {C = A}{D = C×D})

.※-universal :
    ∀ {o₁ ℓ₁ e₁}{A : Category o₁ ℓ₁ e₁}
    → {F : Functor A C}
    → {G : Functor A D}
    → {I : Functor A C×D}
    → (∏₁ ∘ I ≡ F)
    → (∏₂ ∘ I ≡ G)
    → ((F ※ G) ≡ I)
※-universal {_}{_}{_}{A}{F}{G}{I} p₁ p₂ =
    trans {i = F ※ G}{j = (∏₁ ∘ I) ※ (∏₂ ∘ I)}{k = I}
        (sym {i = (∏₁ ∘ I) ※ (∏₂ ∘ I)}{j = F ※ G}
            (※-preserves-≡ (∏₁ ∘ I) F (∏₂ ∘ I) G p₁ p₂))
        (∏₁※∏₂-distrib I)
    where open IsEquivalence (equiv {C = A}{D = C×D})

※-commute₁ :
    ∀ {o₁ ℓ₁ e₁}{A : Category o₁ ℓ₁ e₁}
    → {F : Functor A C}
    → {G : Functor A D}
    → (∏₁ ∘ (F ※ G) ≡ F)
※-commute₁ h = refl
    where open Heterogeneous C

※-commute₂ :
    ∀ {o₁ ℓ₁ e₁}{A : Category o₁ ℓ₁ e₁}
    → {F : Functor A C}
    → {G : Functor A D}
    → (∏₂ ∘ (F ※ G) ≡ G)
※-commute₂ h = refl
    where open Heterogeneous D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Dave.Logic.Basics where
    open import Dave.Functions
    open import Dave.Equality
    open import Dave.Isomorphism
    open import Dave.Structures.Monoid

    {- True -}
    data ⊤ : Set where
        tt : ⊤

    η-⊤ : ∀ (w : ⊤) → tt ≡ w
    η-⊤ tt = refl

    {- False -}
    data ⊥ : Set where
        -- no clauses!

    ⊥-elim : ∀ {A : Set} → ⊥ → A
    ⊥-elim ()

    uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
    uniq-⊥ h ()

    {- Product (Conjunction) -}
    data _×_ (A B : Set) : Set where
        ⟨_,_⟩ : A → B → A × B

    infixr 2 _×_

    proj₁ : {A B : Set} → A × B → A
    proj₁ ⟨ a , b ⟩ = a

    proj₂ : {A B : Set} → A × B → B
    proj₂ ⟨ a , b ⟩ = b

    ×-comm :  {A B : Set} → (A × B) ≃ (B × A)
    ×-comm = record
        {
            to = λ{ ⟨ a , b ⟩ → ⟨ b , a ⟩ };
            from = λ {⟨ b , a ⟩ → ⟨ a , b ⟩};
            from∘to = λ { ⟨ a , b ⟩ → refl };
            to∘from = λ { ⟨ b , a ⟩ → refl }
        }

    ×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
    ×-assoc = record
        {
            to = λ {⟨ ⟨ a , b ⟩ , c ⟩ → ⟨ a , ⟨ b , c ⟩ ⟩};
            from = λ {⟨ a , ⟨ b , c ⟩ ⟩ → ⟨ ⟨ a , b ⟩ , c ⟩};
            from∘to = λ {⟨ ⟨ a , b ⟩ , c ⟩ → refl};
            to∘from = λ {⟨ a , ⟨ b , c ⟩ ⟩ → refl}
        }

    η-× : ∀ {A B : Set} (w : A × B) →  ⟨ proj₁ w , proj₂ w ⟩ ≡ w
    η-× ⟨ x , y ⟩ = refl

    ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
    ⊤-identityˡ = record
        {
            to      = λ{ ⟨ tt , x ⟩ → x };
            from    = λ{ x → ⟨ tt , x ⟩ };
            from∘to = λ{ ⟨ tt , x ⟩ → refl };
            to∘from = λ{ x → refl }
        }

    ⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
    ⊤-identityʳ {A} = ≃-begin
        (A × ⊤) ≃⟨ ×-comm ⟩
        (⊤ × A) ≃⟨ ⊤-identityˡ ⟩
        A ≃-∎

    {- Sum (Disjunction) -}
    data _⊎_ (A B : Set) : Set where
        inj₁ : A → A ⊎ B
        inj₂ : B → A ⊎ B

    infixr 1 _⊎_

    case-⊎ : ∀ {A B C : Set}
        → (A → C)
        → (B → C)
        → A ⊎ B
        -----------
        → C
    case-⊎ f g (inj₁ x) = f x
    case-⊎ f g (inj₂ y) = g y

    uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
        case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
    uniq-⊎ h (inj₁ x) = refl
    uniq-⊎ h (inj₂ y) = refl

    η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
    η-⊎ (inj₁ x) = refl
    η-⊎ (inj₂ y) = refl

    ⊥-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
    ⊥-identityˡ = record
        {
            to = λ {(inj₂ a) → a};
            from = λ a → inj₂ a;
            from∘to = λ {(inj₂ a) → refl};
            to∘from = λ a → refl
        }

    ⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
    ⊎-comm = record
        {
            to = λ {(inj₁ A) → inj₂ A
                  ; (inj₂ B) → inj₁ B};
            from = λ {(inj₁ B) → inj₂ B
                    ; (inj₂ A) → inj₁ A};
            from∘to = λ {(inj₁ x) → refl
                       ; (inj₂ x) → refl};
            to∘from = λ {(inj₁ x) → refl
                       ; (inj₂ x) → refl}
        }

    ⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
    ⊎-assoc = record
        {
            to = λ {(inj₁ (inj₁ a)) → inj₁ a
                  ; (inj₁ (inj₂ b)) → inj₂ (inj₁ b)
                  ; (inj₂ c) → inj₂ (inj₂ c)};
            from = λ {(inj₁ a) → inj₁ (inj₁ a)
                    ; (inj₂ (inj₁ b)) → inj₁ (inj₂ b)
                    ; (inj₂ (inj₂ c)) → inj₂ c};
            from∘to = λ {(inj₁ (inj₁ x)) → refl
                       ; (inj₁ (inj₂ x)) → refl
                       ; (inj₂ x) → refl};
            to∘from = λ {(inj₁ x) → refl
                       ; (inj₂ (inj₁ x)) → refl
                       ; (inj₂ (inj₂ x)) → refl}
        }

    ⊥-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
    ⊥-identityʳ {A} = ≃-begin
        (A ⊎ ⊥) ≃⟨ ⊎-comm ⟩
        (⊥ ⊎ A) ≃⟨ ⊥-identityˡ ⟩
        A ≃-∎

    {- Equality -}
    record _⇔_ (A B : Set) : Set where
        field
            to   : A → B
            from : B → A

    open _⇔_

    ⇔-ref : ∀ {A : Set} → A ⇔ A
    ⇔-ref = record
        {
            to = λ a → a;
            from = λ a → a
        }

    ⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
    ⇔-sym A⇔B = record
        {
            to = from A⇔B;
            from = to A⇔B
        }

    ⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
    ⇔-trans A⇔B B⇔C = record
        {
            to = λ a → to B⇔C (to A⇔B a);
            from = λ c → from A⇔B (from B⇔C c)
        }

    ⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
    ⇔≃× = record
        {
            to = λ {A⇔B → ⟨ to A⇔B , from A⇔B ⟩};
            from = λ {x → record { to = proj₁ x; from = proj₂ x } };
            from∘to = λ A⇔B → refl;
            to∘from = λ {⟨ A→B , B→A ⟩ → refl}
        }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.Vec.Recursive.Properties
-- instead.
------------------------------------------------------------------------

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

module Data.Product.N-ary.Properties where

{-# WARNING_ON_IMPORT
"Data.Product.N-ary.Properties was deprecated in v1.1.
Use Data.Vec.Recursive.Properties instead."
#-}

open import Data.Vec.Recursive.Properties public


text:
module Data.List.Instance where

open import Class.Equality
open import Class.Monad
open import Class.Monoid
open import Class.Show
open import Class.Traversable
open import Data.Bool using (Bool; _∧_; true; false)
open import Data.List hiding (concat)
open import Data.List.Properties
open import Data.String using (String)
open import Data.String.Instance
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

instance
  List-Eq : ∀ {A} {{_ : Eq A}} -> Eq (List A)
  List-Eq {A} = record { _≟_ = ≡-dec _≟_ }

  List-EqB : ∀ {A} {{_ : EqB A}} -> EqB (List A)
  List-EqB {A} = record { _≣_ = helper }
    where
      helper : (l l' : List A) -> Bool
      helper [] [] = true
      helper [] (x ∷ l') = false
      helper (x ∷ l) [] = false
      helper (x ∷ l) (x₁ ∷ l') = x ≣ x₁ ∧ helper l l'

  List-Monoid : ∀ {a} {A : Set a} -> Monoid (List A)
  List-Monoid = record { mzero = [] ; _+_ = _++_ }

  List-Traversable : ∀ {a} -> Traversable {a} (List {a})
  List-Traversable = record { sequence = helper }
    where
      helper : ∀ {a} {M : Set a → Set a} ⦃ _ : Monad M ⦄ {A : Set a} → List (M A) → M (List A)
      helper [] = return []
      helper (x ∷ xs) = do
        x' <- x
        xs' <- helper xs
        return (x' ∷ xs')

  List-Show : ∀ {a} {A : Set a} {{_ : Show A}} -> Show (List A)
  List-Show = record { show = showList show }
    where
      showList : ∀ {a} {A : Set a} -> (A -> String) -> List A -> String
      showList showA l = "[" + concat (intersperse "," (map showA l)) + "]"

  List-Monad : ∀ {a} -> Monad {a} List
  List-Monad = record { _>>=_ = λ l f -> concat (map f l) ; return = λ a -> Data.List.[ a ] }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module _ where

open import Relation.Binary.PropositionalEquality using (refl)

_ : 2 + 1 ≡ 3
_ = refl

max_stars_repo_path: testData/parse/agda/dummy name.agda

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_path: testData/parse/agda/dummy name.agda

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_path: testData/parse/agda/dummy name.agda

max_forks_repo_name: dubinsky/intellij-dtlc


text:
{-# OPTIONS --prop --allow-unsolved-metas #-}

data ⊤ : Prop where
  tt : ⊤

data A : ⊤ → Set where
  a : (x : ⊤) → A x

f : A tt → ⊤
f (a x) = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2011-10-02
-- {-# OPTIONS -v tc.meta:20 #-}
module Issue483 where

data _≡_ (a : Set) : Set → Set where
  refl : a ≡ a

test : (P : .Set → Set) →
  let X : .Set → Set
      X = _
  in  (x : Set) → X x ≡ P (P x)
test P x = refl
-- expected behavior: solving X = P

{-  THE FOLLOWING COULD BE SOLVED IN THE SPECIFIC CASE, BUT NOT IN GENERAL
postulate
  A : Set
  a : A
  f : .A → A

test2 : let X : .A → A
            X = _
        in (x : A) → X a ≡ f x
test2 x = refl
-- should solve as X = f
-- it was treated as X _ = f _ before with solution X = \ x -> f _
-- which eta-contracts to X = f
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Algebra.Monoid where
  open import Basics

  open import lib.types.Paths

  record ∞-monoid i : Type (lsucc i) where
    field -- data
      el : Type i
      μ  : el → End el

    μ' : el → End el
    μ' b a = μ a b

    field -- properties
      unit-l : hfiber μ  (idf el) is-contractible
      unit-r : hfiber μ' (idf el) is-contractible
      mult   : ∀ a b → hfiber μ ((μ a) ∘ (μ b)) is-contractible

    1l : el
    1l = fst $ contr-center unit-l

    1l-def : μ 1l == idf el
    1l-def = snd $ contr-center unit-l

    1r : el
    1r = fst $ contr-center unit-r

    1r-def : μ' 1r == idf el
    1r-def = snd $ contr-center unit-r

    infix 50 _·_
    _·_ : el → el → el
    a · b = fst $ contr-center (mult a b)

    ·-def : ∀ a b → μ (a · b) == (μ a) ∘ (μ b)
    ·-def a b =  snd $ contr-center (mult a b)
    -- --------------------------------------------

    1l=1r : 1l == 1r
    1l=1r = 1l
          =⟨ ! (1r-def at 1l) ⟩
             μ 1l 1r
          =⟨ 1l-def at 1r ⟩
             1r
          =∎

    μ=· : ∀ a b → (μ a b) == (a · b)
    μ=· a b = μ a b
            =⟨ ! $ ap (μ a) (1r-def at b) ⟩
              μ a (μ b 1r)
            =⟨ ! $ (·-def a b) at 1r ⟩
              μ (a · b) 1r
            =⟨ 1r-def at (a · b) ⟩
              a · b
            =∎

    m-assoc : ∀ a b c → (a · b) · c == a · (b · c)
    m-assoc a b c = ap fst (! (contr-path (mult a (b · c)) in-fib))
      where
        lem : μ((a · b) · c) == (μ a) ∘ μ(b · c)
        lem = μ((a · b) · c)
            =⟨ ·-def (a · b) c ⟩
              μ(a · b) ∘ (μ c)
            =⟨ ap (λ f → f ∘ (μ c)) (·-def a b) ⟩
              (μ a) ∘ (μ b) ∘ (μ c)
            =⟨ ! $ ap (λ f → (μ a) ∘ f) (·-def b c) ⟩
              (μ a) ∘ μ(b · c)
            =∎

        in-fib : hfiber μ ((μ a) ∘ μ(b · c))
        in-fib = ((a · b) · c) , lem

    penta : ∀ a b c d →
            (m-assoc (a · b) c d) ∙ (m-assoc a b (c · d))
              ==
            (ap (λ x → x · d) (m-assoc a b c)) ∙ (m-assoc a (b · c) d) ∙ (ap (λ x → a · x) (m-assoc b c d))
    penta a b c d = {!!}

  End-l : ∀ {i} (X : Type i) → ∞-monoid i
  End-l X = record { el = End X
                   ; μ = λ f → λ g → f ∘ g
                   ; unit-l = has-level-in $ (idf X , refl) , proof-unit-l
                   ; unit-r = has-level-in $ (idf X , refl) , proof-unit-r
                   ; mult = λ a b → has-level-in $ (a ∘ b , refl) , proof-mult a b}
    where
      proof-unit-l : ∀ y → (idf X , refl) == y
      proof-unit-l (f , p) = pair= (! p at idf X) $ ↓-app=cst-in $
                   idp
                   =⟨ ! (!-inv-l p) ⟩
                    (! p) ∙ p
                   =⟨ ap (λ α → α ∙ p) helper ⟩
                    (ap (λ z g → z ∘ g) (! p at idf X)) ∙ p
                   =∎
        where
          lemma : (k : End X → End X) (q : (idf (End X)) == k) (f : End X)
                  (η : (k f) ∘_ == k ∘ (f ∘_))
                → (ap (λ u g → (u f) ∘ g) q) ∙' η == (ap (λ u g → u (f ∘ g)) q)
          lemma _ idp _ idp = idp

          helper : ! p == (ap (λ z g → z ∘ g) (! p at idf X))
          helper = ! p
                 =⟨ other-lemma (! p) ⟩
                   ap (λ u g → u g) (! p)
                 =⟨ ! $ lemma (f ∘_) (! p) (idf X) refl  ⟩
                   ap (λ u g → (u (idf X)) ∘ g) (! p)
                 =⟨ ap-∘ (λ z x x₁ → z (x x₁)) (λ z → z (λ x → x)) (! p) ⟩
                  (ap (λ z g → z ∘ g) (! p at idf X))
                 =∎
            where
              other-lemma : ∀ {i j} {X : Type i} {Y : Type j} {f g : X → Y}
                            (p : f == g) → p == (ap (λ u g → u g) p)
              other-lemma refl = refl

      proof-unit-r : ∀ y → (idf X , refl) == y
      proof-unit-r (f , p) = pair= (! p at idf X) $ ↓-app=cst-in $
                   idp
                   =⟨ ! (!-inv-l p) ⟩
                    (! p) ∙ p
                   =⟨ ap (λ α → α ∙ p) helper ⟩
                    (ap (λ z g → g ∘ z) (! p at idf X)) ∙ p
                   =∎
        where
          lemma : (k : End X → End X) (q : (idf (End X)) == k) (f : End X)
                  (η : _∘ (k f) == k ∘ (_∘ f))
                → (ap (λ u g → g ∘ (u f)) q) ∙' η == (ap (λ u g → u (g ∘ f)) q)
          lemma _ refl _ refl = refl

          helper : ! p  == (ap (λ z g → g ∘ z) (! p at idf X))
          helper = ! p
                 =⟨ other-lemma (! p) ⟩
                   ap (λ u g → u g) (! p)
                 =⟨ ! $ lemma (_∘ f) (! p) (idf X) refl ⟩
                   ap (λ u g → g ∘ (u (idf X))) (! p)
                 =⟨ ap-∘ (λ z x x₁ → x (z x₁)) (λ z → z (λ x → x)) (! p) ⟩
                   ap (λ z g → g ∘ z) (! p at idf X)
                 =∎
           where
              other-lemma : ∀ {i j} {X : Type i} {Y : Type j} {f g : X → Y}
                            (p : f == g) → p == (ap (λ u g → u g) p)
              other-lemma refl = refl

      proof-mult : ∀ a b y → (a ∘ b , refl) == y
      proof-mult a b (f , p) = pair= (! p at idf X) $ ↓-app=cst-in $
                 refl
                 =⟨ ! (!-inv-l p) ⟩
                  ! p ∙ p
                 =⟨ ap (λ α → α ∙ p) helper ⟩
                  (ap (λ z g → z ∘ g) (! p at idf X)) ∙ p
                 =∎
        where
          lemma : (k : End X → End X) (q : (a ∘ b) ∘_ == k) (f : End X)
                  (η : (k f) ∘_ == k ∘ (f ∘_))
                → (ap (λ u g → (u f) ∘ g) q) ∙' η == (ap (λ u g → u (f ∘ g)) q)
          lemma _ idp _ idp = idp

          helper : ! p == (ap (λ z g → z ∘ g) (! p at idf X))
          helper = ! p
                 =⟨ other-lemma (! p) ⟩
                   ap (λ u g → u g) (! p)
                 =⟨ ! $ lemma (f ∘_) (! p) (idf X) refl  ⟩
                   ap (λ u g → (u (idf X)) ∘ g) (! p)
                 =⟨ ap-∘ (λ z x x₁ → z (x x₁)) (λ z → z (λ x → x)) (! p) ⟩
                  (ap (λ z g → z ∘ g) (! p at idf X))
                 =∎
            where
              other-lemma : ∀ {i j} {X : Type i} {Y : Type j} {f g : X → Y}
                            (p : f == g) → p == (ap (λ u g → u g) p)
              other-lemma refl = refl

  Aut-l : ∀ {i} {X : Type i} (x : X) → ∞-monoid i
  Aut-l {X = X} x = record { el = x == x
                           ; μ = λ p → λ q → p ∙ q
                           ; unit-l = has-level-in $ (refl , refl) , unit-l-proof
                           ; unit-r = has-level-in $ (refl , (λ= ∙-unit-r)) , unit-r-proof
                           ; mult = λ a b → has-level-in $ (a ∙ b , λ= (∙-assoc a b)) , mult-proof a b }
    where
      unit-l-proof : ∀ y → (refl , refl) == y
      unit-l-proof (p , α) = pair= (! (α at refl) ∙ (∙-unit-r p)) $ ↓-app=cst-in $
                    idp
                   =⟨ ! (!-inv-l α) ⟩
                    ! α ∙ α
                   =⟨ {!!} ⟩
                    ap (λ z q → z ∙ q) (! (α at refl) ∙ (∙-unit-r p)) ∙ α
                   =∎

      unit-r-proof : ∀ y → (refl , (λ= ∙-unit-r)) == y
      unit-r-proof (p , α) = {!!}

      mult-proof : ∀ a b y → (a ∙ b , λ= (∙-assoc a b)) == y
      mult-proof a b y = {!!}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
{- Denotational semantics of the terms in the category of temporal types. -}
module Semantics.Terms where

open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Types

open import Semantics.Types
open import Semantics.Context

open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Linear
open import TemporalOps.Box
open import TemporalOps.Diamond
open import TemporalOps.OtherOps
open import TemporalOps.Linear
open import TemporalOps.StrongMonad

open import CategoryTheory.Functor
open import CategoryTheory.NatTrans renaming (_⟹_ to ⟹)
import CategoryTheory.Monad as M
import CategoryTheory.Comonad as W

open import Data.Product
open import Data.Sum hiding ([_,_])
import Data.Nat as N

open W.Comonad W-□
open M.Monad M-◇
private module F-◇ = Functor F-◇
private module F-□ = Functor F-□
-- open Linear ℝeactive-linear

mutual
    -- Denotation of pure terms as morphisms from contexts to types.
    ⟦_⟧ₘ : ∀{Γ A} -> Γ ⊢ A -> (⟦ Γ ⟧ₓ ⇴ ⟦ A ⟧ⱼ)
    ⟦ var top       ⟧ₘ = π₂
    ⟦ var (pop x)   ⟧ₘ = ⟦ var x ⟧ₘ ∘ π₁
    ⟦ lam M         ⟧ₘ = Λ ⟦ M ⟧ₘ
    ⟦ F $ M         ⟧ₘ = eval ∘ ⟨ ⟦ F ⟧ₘ , ⟦ M ⟧ₘ ⟩
    ⟦ unit          ⟧ₘ = !
    ⟦ [ M ,, N ]    ⟧ₘ = ⟨ ⟦ M ⟧ₘ , ⟦ N ⟧ₘ ⟩
    ⟦ fst M         ⟧ₘ = π₁ ∘ ⟦ M ⟧ₘ
    ⟦ snd M         ⟧ₘ = π₂ ∘ ⟦ M ⟧ₘ
    ⟦ inl M         ⟧ₘ = ι₁ ∘ ⟦ M ⟧ₘ
    ⟦ inr M         ⟧ₘ = ι₂ ∘ ⟦ M ⟧ₘ
    ⟦ case M inl↦ B₁ ||inr↦ B₂ ⟧ₘ = [ ⟦ B₁ ⟧ₘ ⁏ ⟦ B₂ ⟧ₘ ] ∘ dist ∘ ⟨ id , ⟦ M ⟧ₘ ⟩
    ⟦ sample {A} S  ⟧ₘ = ε.at ⟦ A ⟧ₜ ∘ ⟦ S ⟧ₘ
    ⟦ stable {Γ} S  ⟧ₘ = F-□.fmap ⟦ S ⟧ₘ ∘ ⟦ Γ ˢ⟧□
    ⟦ sig S         ⟧ₘ = ⟦ S ⟧ₘ
    ⟦ letSig S In B ⟧ₘ = ⟦ B ⟧ₘ ∘ ⟨ id , ⟦ S ⟧ₘ ⟩
    ⟦ event E       ⟧ₘ = ⟦ E ⟧ᵐ

    -- Helper function for interpreting bound events
    bindEvent : ∀ Γ {⟦A⟧ ⟦B⟧} -> (⟦E⟧ : ⟦ Γ ⟧ₓ ⇴ ◇ ⟦A⟧) (⟦C⟧ : ⟦ Γ ˢ ⟧ₓ ⊗ ⟦A⟧ ⇴ ◇ ⟦B⟧)
                  -> (⟦ Γ ⟧ₓ ⇴ ◇ ⟦B⟧)
    bindEvent Γ {⟦A⟧}{⟦B⟧} ⟦E⟧ ⟦C⟧ =
        μ.at ⟦B⟧ ∘ F-◇.fmap (⟦C⟧ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) ∘ st ⟦ Γ ˢ ⟧ₓ ⟦A⟧ ∘ ⟨ ⟦ Γ ˢ⟧□ , ⟦E⟧ ⟩

    -- Denotation of computational terms as Kleisli morphisms from contexts to types.
    ⟦_⟧ᵐ : ∀{Γ A} -> Γ ⊨ A -> (⟦ Γ ⟧ₓ ⇴ ◇ ⟦ A ⟧ⱼ)
    ⟦ pure {A} M     ⟧ᵐ = η.at ⟦ A ⟧ⱼ ∘ ⟦ M ⟧ₘ
    ⟦ letSig S InC C ⟧ᵐ = ⟦ C ⟧ᵐ ∘ ⟨ id , ⟦ S ⟧ₘ ⟩
    ⟦ letEvt_In_ {Γ} E C ⟧ᵐ = bindEvent Γ ⟦ E ⟧ₘ ⟦ C ⟧ᵐ
    ⟦ select_↦_||_↦_||both↦_ {Γ} E₁ C₁ E₂ C₂ C₃ ⟧ᵐ =
        bindEvent Γ (⟪ ⟦ E₁ ⟧ₘ , ⟦ E₂ ⟧ₘ ⟫) (handle ⟦ C₁ ⟧ᵐ ⟦ C₂ ⟧ᵐ ⟦ C₃ ⟧ᵐ)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------------
-- Well-founded relation related to the McCarthy 91 function
------------------------------------------------------------------------------

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

module FOTC.Program.McCarthy91.WF-Relation where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- The relation _◁_.

◁-fn : D → D
◁-fn n = 101' ∸ n
{-# ATP definition ◁-fn #-}

_◁_ : D → D → Set
m ◁ n = ◁-fn m < ◁-fn n
{-# ATP definition _◁_ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Data.List.Base where

open import Level
open import Agda.Builtin.List using (List; _∷_; []) public
open import Data.Nat.Base
open import Function
open import Strict
open import Data.Maybe using (Maybe; just; nothing; maybe)

foldr : (A → B → B) → B → List A → B
foldr f b [] = b
foldr f b (x ∷ xs) = f x (foldr f b xs)

foldrMay : (A → A → A) → List A → Maybe A
foldrMay f = foldr (λ x → just ∘ maybe x (f x)) nothing

foldl : (B → A → B) → B → List A → B
foldl f b [] = b
foldl f b (x ∷ xs) = foldl f (f b x) xs

foldl′ : (B → A → B) → B → List A → B
foldl′ f b [] = b
foldl′ f b (x ∷ xs) = let! z =! f b x in! foldl′ f z xs

foldr′ : (A → B → B) → B → List A → B
foldr′ f b [] = b
foldr′ f b (x ∷ xs) = f x $! foldr′ f b xs

infixr 5 _++_
_++_ : List A → List A → List A
xs ++ ys = foldr _∷_ ys xs

length : List A → ℕ
length = foldr (const suc) zero

concat : List (List A) → List A
concat = foldr _++_ []

concatMap : (A → List B) → List A → List B
concatMap f = foldr (λ x ys → f x ++ ys) []

map : (A → B) → List A → List B
map f = foldr (λ x xs → f x ∷ xs) []

take : ℕ → List A → List A
take zero _ = []
take (suc n) [] = []
take (suc n) (x ∷ xs) = x ∷ take n xs

_⋯_ : ℕ → ℕ → List ℕ
_⋯_ n = go n
  where
  go″ : ℕ → ℕ → List ℕ
  go′ : ℕ → ℕ → List ℕ

  go″ n zero = []
  go″ n (suc m) = go′ (suc n) m

  go′ n m = n ∷ go″ n m

  go : ℕ → ℕ → List ℕ
  go zero = go′ n
  go (suc n) zero = []
  go (suc n) (suc m) = go n m

replicate : A → ℕ → List A
replicate {A = A} x = go
  where
  go : ℕ → List A
  go zero = []
  go (suc n) = x ∷ go n


text:
{-

Set quotients:

-}

{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.SetQuotients.Properties where

open import Cubical.HITs.SetQuotients.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.HAEquiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.SetTruncation

-- Type quotients

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    R : A → A → Type ℓ'
    B : A / R → Type ℓ''

elimEq/ : (Bprop : (x : A / R ) → isProp (B x))
          {x y : A / R}
          (eq : x ≡ y)
          (bx : B x)
          (by : B y) →
          PathP (λ i → B (eq i)) bx by
elimEq/ {B = B} Bprop {x = x} =
  J (λ y eq → ∀ bx by → PathP (λ i → B (eq i)) bx by) (λ bx by → Bprop x bx by)

elimSetQuotientsProp : ((x : A / R ) → isProp (B x)) →
                       (f : (a : A) → B ( [ a ])) →
                       (x : A / R) → B x
elimSetQuotientsProp Bprop f [ x ] = f x
elimSetQuotientsProp Bprop f (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep {n = 2} (λ x → isProp→isSet (Bprop x))
              (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
    g = elimSetQuotientsProp Bprop f
elimSetQuotientsProp Bprop f (eq/ a b r i) = elimEq/ Bprop (eq/ a b r) (f a) (f b) i

-- lemma 6.10.2 in hott book
-- TODO: defined truncated Sigma as ∃
[]surjective : (x : A / R) → ∥ Σ[ a ∈ A ] [ a ] ≡ x ∥
[]surjective = elimSetQuotientsProp (λ x → squash) (λ a → ∣ a , refl ∣)

elimSetQuotients : {B : A / R → Type ℓ} →
                   (Bset : (x : A / R) → isSet (B x)) →
                   (f : (a : A) → (B [ a ])) →
                   (feq : (a b : A) (r : R a b) →
                          PathP (λ i → B (eq/ a b r i)) (f a) (f b)) →
                   (x : A / R) → B x
elimSetQuotients Bset f feq [ a ] = f a
elimSetQuotients Bset f feq (eq/ a b r i) = feq a b r i
elimSetQuotients Bset f feq (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep {n = 2} Bset
              (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
      g = elimSetQuotients Bset f feq

setQuotUniversal : {B : Type ℓ} (Bset : isSet B) →
                   (A / R → B) ≃ (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b))
setQuotUniversal Bset = isoToEquiv (iso intro elim elimRightInv elimLeftInv)
  where
  intro = λ g →  (λ a → g [ a ]) , λ a b r i → g (eq/ a b r i)
  elim = λ h → elimSetQuotients (λ x → Bset) (fst h) (snd h)

  elimRightInv : ∀ h → intro (elim h) ≡ h
  elimRightInv h = refl

  elimLeftInv : ∀ g → elim (intro g) ≡ g
  elimLeftInv = λ g → funExt (λ x → elimPropTrunc {P = λ sur → elim (intro g) x ≡ g x}
    (λ sur → Bset (elim (intro g) x) (g x))
    (λ sur → cong (elim (intro g)) (sym (snd sur)) ∙ (cong g (snd sur))) ([]surjective x)
    )

open BinaryRelation

effective : (Rprop : isPropValued R) (Requiv : isEquivRel R) (a b : A) → [ a ] ≡ [ b ] → R a b
effective {A = A} {R = R} Rprop (EquivRel R/refl R/sym R/trans) a b p = transport aa≡ab (R/refl _)
  where
    helper : A / R → hProp
    helper = elimSetQuotients (λ _ → isSetHProp) (λ c → (R a c , Rprop a c))
                              (λ c d cd → ΣProp≡ (λ _ → isPropIsProp)
                                                 (ua (PropEquiv→Equiv (Rprop a c) (Rprop a d)
                                                                      (λ ac → R/trans _ _ _ ac cd) (λ ad → R/trans _ _ _ ad (R/sym _ _ cd)))))

    aa≡ab : R a a ≡ R a b
    aa≡ab i = fst (helper (p i))

isEquivRel→isEffective : isPropValued R → isEquivRel R → isEffective R
isEquivRel→isEffective {R = R} Rprop Req a b = isoToEquiv (iso intro elim intro-elim elim-intro)
  where
    intro : [ a ] ≡ [ b ] → R a b
    intro = effective Rprop Req a b

    elim : R a b → [ a ] ≡ [ b ]
    elim = eq/ a b

    intro-elim : ∀ x → intro (elim x) ≡ x
    intro-elim ab = Rprop a b _ _

    elim-intro : ∀ x → elim (intro x) ≡ x
    elim-intro eq = squash/ _ _ _ _

discreteSetQuotients : Discrete A → isPropValued R → isEquivRel R → (∀ a₀ a₁ → Dec (R a₀ a₁)) → Discrete (A / R)
discreteSetQuotients {A = A} {R = R} Adis Rprop Req Rdec =
 elimSetQuotients ((λ a₀ → isSetPi (λ a₁ → isProp→isSet (isPropDec (squash/ a₀ a₁)))))
                  discreteSetQuotients' discreteSetQuotients'-eq
  where
    discreteSetQuotients' : (a : A) (y : A / R) → Dec ([ a ] ≡ y)
    discreteSetQuotients' a₀ = elimSetQuotients ((λ a₁ → isProp→isSet (isPropDec (squash/ [ a₀ ] a₁)))) dis dis-eq
      where
        dis : (a₁ : A) → Dec ([ a₀ ] ≡ [ a₁ ])
        dis a₁ with Rdec a₀ a₁
        ... | (yes p) = yes (eq/ a₀ a₁ p)
        ... | (no ¬p) = no λ eq → ¬p (effective Rprop Req a₀ a₁ eq )

        dis-eq : (a b : A) (r : R a b) →
          PathP (λ i → Dec ([ a₀ ] ≡ eq/ a b r i)) (dis a) (dis b)
        dis-eq a b ab = J (λ b ab → ∀ k → PathP (λ i → Dec ([ a₀ ] ≡ ab i)) (dis a) k)
                          (λ k → isPropDec (squash/ _ _) _  _) (eq/ a b ab) (dis b)

    discreteSetQuotients'-eq : (a b : A) (r : R a b) →
      PathP (λ i → (y : A / R) → Dec (eq/ a b r i ≡ y))
            (discreteSetQuotients' a) (discreteSetQuotients' b)
    discreteSetQuotients'-eq a b ab =
      J (λ b ab → ∀ k → PathP (λ i → (y : A / R) → Dec (ab i ≡ y))
                              (discreteSetQuotients' a) k)
        (λ k → funExt (λ x → isPropDec (squash/ _ _) _ _)) (eq/ a b ab) (discreteSetQuotients' b)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Basic.Axiomatic.TotalImpliesPartial where

open import Basic.AST
open import Basic.BigStep
open import Basic.Axiomatic.Total as T
  renaming (〈_〉_〈_〉 to total〈_〉_〈_〉)
open import Basic.Axiomatic.Partial as P
  renaming (〈_〉_〈_〉 to partial〈_〉_〈_〉) hiding (_==>_; _∧_)

open import Function
open import Data.Product

{-
The proof that total correctness implies partial correctness (exercise 6.33)
is fortunately really simple.

We already proved soundness and completeness for both systems, so instead of
trying to construct the partial proof directly from the total proof, we can
just take a detour and prove the analoguous implication about the *validity*
of triples.
-}

{-
The total validity of Hoare triples implies partial validity, if the language semantics is
deterministic.
-}
P==>wp→P==>wlp : ∀{n S}{P Q : State n → Set} → (P ==> wp S Q) → (P ==> wlp S Q)
P==>wp→P==>wlp pwp ps runS with pwp ps
... | _ , runS' , qs' rewrite deterministic runS runS' = qs'

{- And now we just do an excursion to semantics-land and then back -}
total→partial : ∀ {n S}{P Q : State n → Set} → total〈 P 〉 S 〈 Q 〉 → partial〈 P 〉 S 〈 Q 〉
total→partial = P.complete _ ∘ P==>wp→P==>wlp ∘ T.sound

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
{-# OPTIONS --sized-types #-}
module SList.Concatenation (A : Set) where

open import Data.List
open import List.Permutation.Base A
open import Size
open import SList

lemma-⊕-/ : {xs ys : List A}{x y : A} → xs / x ⟶ ys → unsize A (_⊕_ A (size A xs) (y ∙ snil)) / x ⟶ unsize A (_⊕_ A (size A ys) (y ∙ snil))
lemma-⊕-/ /head = /head
lemma-⊕-/ (/tail xs/x⟶xs') = /tail (lemma-⊕-/ xs/x⟶xs')

lemma-⊕∼ : {xs ys : List A}(x : A) → xs ∼ ys → (x ∷ xs) ∼ unsize A (_⊕_ A (size A ys) (x ∙ snil))
lemma-⊕∼ x ∼[] = ∼x /head /head ∼[]
lemma-⊕∼ x (∼x xs/x⟶xs' ys/x⟶ys' xs'∼ys') = ∼x (/tail xs/x⟶xs') (lemma-⊕-/ ys/x⟶ys') (lemma-⊕∼ x xs'∼ys')

lemma-size-unsize : {ι : Size}(x : A) → (xs : SList A {ι}) → (unsize A (_⊕_ A (size A (unsize A xs)) (x ∙ snil))) ∼ unsize A (_⊕_ A xs (x ∙ snil))
lemma-size-unsize x snil = ∼x /head /head ∼[]
lemma-size-unsize x (y ∙ ys) = ∼x /head  /head (lemma-size-unsize x ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module main where

open import Not-named-according-to-the-Haskell-lexical-syntax

main = return Not-named-according-to-the-Haskell-lexical-syntax.unit

-- The following code once triggered an MAlonzo bug resulting in the
-- error message "Panic: ... no such name main.M.d".

module M where
  data D : Set where
    d : D

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- This file has been extracted from https://alhassy.github.io/PathCat/
-- Type checks with Agda version 2.6.0.

module PathCat where

open import Level using (Level) renaming (zero to ℓ₀ ; suc to ℓsuc ; _⊔_ to _⊍_)

-- Numbers
open import Data.Fin
  using (Fin ; toℕ ; fromℕ ; fromℕ≤ ; reduce≥ ; inject≤)
  renaming (_<_ to _f<_ ; zero to fzero ; suc to fsuc)
open import Data.Nat
open import Relation.Binary using (module DecTotalOrder)
open import Data.Nat.Properties using(≤-decTotalOrder ; ≤-refl)
open DecTotalOrder Data.Nat.Properties.≤-decTotalOrder

-- Z-notation for sums
open import Data.Product using (Σ ; proj₁ ; proj₂ ; _×_ ; _,_)
Σ∶• : {a b : Level} (A : Set a) (B : A → Set b) → Set (a ⊍ b)
Σ∶• = Σ
infix -666 Σ∶•
syntax Σ∶• A (λ x → B) = Σ x ∶ A • B

-- Equalities
open import Relation.Binary.PropositionalEquality using (_≗_ ; _≡_)
  renaming (sym to ≡-sym ; refl to ≡-refl ; trans to _⟨≡≡⟩_
           ; cong to ≡-cong ; cong₂ to ≡-cong₂
           ; subst to ≡-subst ; subst₂ to ≡-subst₂ ; setoid to ≡-setoid)

module _ {i} {S : Set i} where
    open import Relation.Binary.EqReasoning (≡-setoid S) public

open import Agda.Builtin.String

defn-chasing : ∀ {i} {A : Set i} (x : A) → String → A → A
defn-chasing x reason supposedly-x-again = supposedly-x-again

syntax defn-chasing x reason xish = x ≡⟨ reason ⟩′ xish

infixl 3 defn-chasing

_even-under_ : ∀ {a b} {A : Set a} {B : Set b} {x y} → x ≡ y → (f : A → B) → f x ≡ f y
_even-under_ = λ eq f → ≡-cong f eq

record Graph₀ : Set₁ where
  field
    V   : Set
    E   : Set
    src : E → V
    tgt : E → V

record _𝒢⟶₀_ (G H : Graph₀) : Set₁ where
  open Graph₀
  field
    vertex : V(G) → V(H)
    edge   : E(G) → E(H)
    src-preservation : ∀ e → src(H) (edge e) ≡  vertex (src(G) e)
    tgt-preservation : ∀ e → tgt(H) (edge e) ≡  vertex (tgt(G) e)

-- ‘small graphs’ , since we are not using levels
record Graph : Set₁ where
  field
    V    : Set
    _⟶_ : V → V → Set

-- i.e., Graph ≈ Σ V ∶ Set • (V → V)
-- Graphs are a dependent type!

record GraphMap (G H : Graph) : Set₁ where
    private
      open Graph using (V)
      _⟶g_ = Graph._⟶_ G
      _⟶h_ = Graph._⟶_ H
    field
      ver  : V(G) → V(H)                                   -- vertex morphism
      edge : {x y : V(G)} → (x ⟶g y) → (ver x ⟶h ver y) -- arrow preservation

open GraphMap

-- embedding: j < n ⇒ j < suc n
`_ : ∀{n} → Fin n → Fin (suc n)
` j = inject≤ j (≤-step ≤-refl) where open import Data.Nat.Properties using (≤-step)

[_]₀ : ℕ → Graph₀
[ n ]₀ = record
    { V = Fin (suc n)                  -- ≈ {0, 1, ..., n - 1, n}
    ; E = Fin n                        -- ≈ {0, 1, ..., n - 1}
    ; src = λ j → ` j
    ; tgt = λ j → fsuc j
    }

[_] : ℕ → Graph
[ n ] = record {V = Fin (suc n) ; _⟶_ = λ x y → fsuc x ≡ ` y }

open import Data.Vec
  using (Vec)
  renaming (_∷_ to _,,_ ; [] to nil) -- , already in use for products :/

-- one sorted
record Signature : Set where
    field
     𝒩 : ℕ        -- How many function symbols there are
     ar : Vec ℕ 𝒩 -- Their arities: lookup i ar == arity of i-th function symbol

open Signature ⦃...⦄ -- 𝒩 now refers to the number of function symbols in a signature

MonSig : Signature
MonSig = record { 𝒩 = 2 ; ar = 0 ,, 2 ,, nil }
-- unit u : X⁰ → X and multiplication m : X² → X

module _ where -- An anyonomous module for categorial definitions

 record Category {i j : Level} : Set (ℓsuc (i ⊍ j)) where
  infixr 10 _⨾_
  field
    Obj      : Set i
    _⟶_     : Obj → Obj → Set j
    _⨾_      : ∀ {A B C : Obj} → A ⟶ B → B ⟶ C → A ⟶ C
    assoc    : ∀ {A B C D} {f : A ⟶ B}{g : B ⟶ C} {h : C ⟶ D} → (f ⨾ g) ⨾ h ≡ f ⨾ (g ⨾ h)
    Id       : ∀ {A : Obj} → A ⟶ A
    leftId   : ∀ {A B : Obj} {f : A ⟶ B} → Id ⨾ f ≡ f
    rightId  : ∀ {A B : Obj} {f : A ⟶ B} → f ⨾ Id ≡ f

 open Category using (Obj)
 open Category ⦃...⦄ hiding (Obj)

 -- Some sugar for times when we must specify the category
 -- “colons associate to the right” ;-)

 arr = Category._⟶_
 syntax arr 𝒞 x y  =  x ⟶ y ∶ 𝒞    -- “ghost colon”

 cmp = Category._⨾_
 syntax cmp 𝒞 f g  =  f ⨾ g ∶ 𝒞    -- “ghost colon”

 open Category using (Obj) public

 record Iso {i} {j} (𝒞 : Category {i} {j}) (A B : Obj 𝒞) : Set j where
   private instance 𝒞′ : Category ; 𝒞′ = 𝒞
   field
     to   : A ⟶ B
     from : B ⟶ A
     lid  : to ⨾ from ≡ Id
     rid  : from ⨾ to ≡ Id

 syntax Iso 𝒞 A B = A ≅ B within 𝒞

 instance
  𝒮e𝓉 : ∀ {i} → Category {ℓsuc i} {i} -- this is a ‘big’ category
  𝒮e𝓉 {i} = record {
      Obj = Set i
    ; _⟶_ = λ A B → (A → B)
    ; _⨾_ = λ f g → (λ x → g (f x))
    ; assoc = ≡-refl
    ; Id = λ x → x
    ; leftId = ≡-refl
    ; rightId = ≡-refl
    }

 record Functor {i j k l} (𝒞 : Category {i} {j}) (𝒟 : Category {k} {l})
  : Set (ℓsuc (i ⊍ j ⊍ k ⊍ l)) where
  private
    instance
      𝒞′ : Category ;  𝒞′ = 𝒞
      𝒟′ : Category ;  𝒟′  = 𝒟
  field
    -- Usual graph homomorphism structure: An object map, with morphism preservation
    obj   : Obj 𝒞 → Obj 𝒟
    mor   : ∀{x y : Obj 𝒞} → x ⟶ y → obj x ⟶ obj y
    -- Interaction with new algebraic structure: Preservation of identities & composition
    id    : ∀{x   : Obj 𝒞} → mor (Id {A = x}) ≡ Id       -- identities preservation
    comp  : ∀{x y z} {f : x ⟶ y} {g : y ⟶ z} → mor (f ⨾ g) ≡ mor f ⨾ mor g

  -- Aliases for readability
  functor_preserves-composition = comp
  functor_preserves-identities  = id

 open Functor public hiding (id ; comp)

 NatTrans : ∀ {i j i’ j’}  ⦃ 𝒞 : Category {i} {j} ⦄ ⦃ 𝒟 : Category {i’} {j’} ⦄
            (F G : Functor 𝒞 𝒟) → Set (j’ ⊍ i ⊍ j)
 NatTrans ⦃ 𝒞 = 𝒞 ⦄ ⦃ 𝒟 ⦄ F G =
   Σ η ∶ (∀ {X : Obj 𝒞} → (obj F X) ⟶ (obj G X))
       • (∀ {A B} {f : A ⟶ B} → mor F f ⨾ η {B} ≡ η {A} ⨾ mor G f)

 -- function extensionality
 postulate extensionality : ∀ {i j} {A : Set i} {B : A → Set j}
                              {f g : (a : A) → B a}
                          → (∀ {a} → f a ≡ g a) → f ≡ g

 -- functor extensionality
 postulate funcext : ∀ {i j k l} ⦃ 𝒞 : Category {i} {j} ⦄ ⦃ 𝒟 : Category {k} {l} ⦄
                       {F G : Functor 𝒞 𝒟}
                     → (oeq : ∀ {o} → obj F o ≡ obj G o)
                     → (∀ {X Y} {f : X ⟶ Y}
                        → mor G f  ≡  ≡-subst₂ (Category._⟶_ 𝒟) oeq oeq (mor F f))
                     → F ≡ G

 -- graph map extensionality
 postulate graphmapext : {G H : Graph } {f g : GraphMap G H}
                       → (veq : ∀ {v} → ver f v ≡ ver g v)
                       → (∀ {x y} {e : Graph._⟶_ G x y}
                          → edge g e ≡ ≡-subst₂ (Graph._⟶_ H) veq veq (edge f e))
                       → f ≡ g

 -- natural transformation extensionality
 postulate nattransext : ∀ {i j i’ j’} {𝒞 : Category {i} {j} } {𝒟 : Category {i’} {j’} }
                         {F G : Functor 𝒞 𝒟} (η γ : NatTrans F G)
                       → (∀ {X} → proj₁ η {X} ≡ proj₁ γ {X})
                       → η ≡ γ

 instance
  𝒞𝒶𝓉 : ∀ {i j} → Category {ℓsuc (i ⊍ j)} {ℓsuc (i ⊍ j)}
  𝒞𝒶𝓉 {i} {j} = record {
      Obj = Category {i} {j}
    ; _⟶_ = Functor
    ; _⨾_ = λ {𝒞} {𝒟} {ℰ} F G →
        let instance
                   𝒞′ : Category ; 𝒞′ = 𝒞
                   𝒟′ : Category ; 𝒟′ = 𝒟
                   ℰ′ : Category ; ℰ′ = ℰ
        in record
        { obj  =  obj F ⨾ obj G -- this compositon lives in 𝒮e𝓉
        ; mor  =  mor F ⨾ mor G
        ; id   =  λ {x} → begin
              (mor F ⨾ mor G) (Id ⦃ 𝒞 ⦄ {A = x})
            ≡⟨ "definition of function composition" ⟩′
              mor G (mor F Id)
            ≡⟨ functor F preserves-identities even-under (mor G) ⟩
              mor G Id
            ≡⟨ functor G preserves-identities ⟩
              Id
            ∎
        ; comp = λ {x y z f g} →
             begin
               (mor F ⨾ mor G) (f ⨾ g)
            ≡⟨ "definition of function composition" ⟩′
               mor G (mor F (f ⨾ g))
             ≡⟨ functor F preserves-composition even-under mor G ⟩
               mor G (mor F f ⨾ mor F g)
             ≡⟨ functor G preserves-composition ⟩
               (mor F ⨾ mor G) f ⨾ (mor F ⨾ mor G) g
             ∎
        }
    ; assoc    =  λ {a b c d f g h} → funcext ≡-refl ≡-refl
    ; Id       =  record { obj = Id ; mor = Id ; id = ≡-refl ; comp = ≡-refl }
    ; leftId   =  funcext ≡-refl ≡-refl
    ; rightId  =  funcext ≡-refl ≡-refl
    }

  𝒢𝓇𝒶𝓅𝒽 : Category
  𝒢𝓇𝒶𝓅𝒽 =
   record
    { Obj   = Graph ; _⟶_ = GraphMap
    ; _⨾_   = λ f g → record { ver = ver f ⨾ ver g ; edge = edge f ⨾ edge g } -- using ~𝒮et~
    ; assoc = ≡-refl  -- function composition is associtive, by definition
    ; Id    = record { ver = Id ; edge = Id } ; leftId = ≡-refl ; rightId = ≡-refl
    -- functional identity is no-op, by definition
    }
    where open GraphMap

 𝒰₀ : Category → Graph
 𝒰₀ 𝒞 = record { V = Obj 𝒞 ; _⟶_ = Category._⟶_ 𝒞 }

 𝒰₁ : {𝒞 𝒟 : Category} → 𝒞 ⟶ 𝒟 → 𝒰₀ 𝒞 ⟶ 𝒰₀ 𝒟
 𝒰₁ F = record { ver = obj F ; edge = mor F }

-- Underlying/forgetful functor: Every category is a graph
 𝒰 : Functor 𝒞𝒶𝓉 𝒢𝓇𝒶𝓅𝒽
 𝒰 = record { obj = 𝒰₀ ; mor = 𝒰₁ ; id = ≡-refl ; comp = ≡-refl }

 instance
  Func : ∀ {i j i’ j’} (𝒞 : Category {i} {j}) (𝒟 : Category {i’} {j’}) → Category {ℓsuc (i ⊍ j ⊍ i’ ⊍ j’)} {j’ ⊍ i ⊍ j}
  Func {i} {j} {i’} {j’} 𝒞 𝒟 = record {
      Obj = Functor 𝒞 𝒟
    ; _⟶_ = NatTrans
    ; _⨾_ = λ {A B C} η γ → comp {A} {B} {C} η γ
    ; assoc = λ {F G H K η γ ω} → nattransext {i} {j} {i’} {j’} {𝒞} {𝒟} {F} {K} (comp {F} {H} {K} (comp {F} {G} {H} η γ) ω) (comp {F} {G} {K} η (comp {G} {H} {K} γ ω)) assoc
    ; Id = λ {F} → iden F
    ; leftId = λ {F G η} → nattransext {i} {j} {i’} {j’} {𝒞} {𝒟} {F} {G} (comp {F} {F} {G} (iden F) η) η leftId
    ; rightId = λ {F G η} → nattransext {i} {j} {i’} {j’} {𝒞} {𝒟} {F} {G} (comp {F} {G} {G} η (iden G)) η rightId
    }
    where
      instance
        𝒟′ : Category
        𝒟′ = 𝒟

      iden : (A : Functor 𝒞 𝒟) → NatTrans A A
      iden A = Id , (rightId ⟨≡≡⟩ ≡-sym leftId)

      -- To avoid long wait times, we avoid instance resolution by
      -- making an alias.
      _⨾′_ = Category._⨾_ 𝒟
      infixr 6 _⨾′_

      comp : {A B C : Functor 𝒞 𝒟} → NatTrans A B → NatTrans B C → NatTrans A C
      comp {F} {G} {H} (η , nat) (γ , nat′) = (λ {X} → η {X} ⨾′ γ {X}) , (λ {A B f} → begin
           mor F f ⨾′ η {B} ⨾′ γ {B}
          ≡⟨ ≡-sym assoc ⟨≡≡⟩ (≡-cong₂ _⨾′_ nat ≡-refl ⟨≡≡⟩ assoc) ⟩
            η {A} ⨾′ mor G f ⨾′ γ {B}
          ≡⟨ ≡-cong₂ _⨾′_ ≡-refl nat′ ⟨≡≡⟩ ≡-sym assoc ⟩
            (η {A} ⨾′ γ {A}) ⨾′ mor H f
          ∎)

 module graphs-as-functors where

  -- formal objects
  data 𝒢₀ : Set where E V : 𝒢₀

  -- formal arrows
  data 𝒢₁ : 𝒢₀ → 𝒢₀ → Set where
     s t : 𝒢₁ E V
     id  : ∀ {o} → 𝒢₁ o o

  -- (forward) composition
  fcmp : ∀ {a b c} → 𝒢₁ a b → 𝒢₁ b c → 𝒢₁ a c
  fcmp f id = f
  fcmp id f = f

  instance
   𝒢 : Category
   𝒢 = record
        { Obj     = 𝒢₀
        ; _⟶_     = 𝒢₁
        ; _⨾_     = fcmp
        ; assoc   = λ {a b c d f g h} → fcmp-assoc f g h
        ; Id      = id
        ; leftId  = left-id
        ; rightId = right-id
        }
    where
       -- exercises: prove associativity, left and right unit laws

       -- proofs are just C-c C-a after some casing

       fcmp-assoc : ∀ {a b c d} (f : 𝒢₁ a b) (g : 𝒢₁ b c) (h : 𝒢₁ c d) → fcmp (fcmp f g) h ≡ fcmp f (fcmp g h)
       fcmp-assoc s id id = ≡-refl
       fcmp-assoc t id id = ≡-refl
       fcmp-assoc id s id = ≡-refl
       fcmp-assoc id t id = ≡-refl
       fcmp-assoc id id s = ≡-refl
       fcmp-assoc id id t = ≡-refl
       fcmp-assoc id id id = ≡-refl

       right-id : ∀ {a b} {f : 𝒢₁ a b} → fcmp f id ≡ f
       right-id {f = s} = ≡-refl
       right-id {f = t} = ≡-refl
       right-id {f = id} = ≡-refl

       left-id : ∀ {a b} {f : 𝒢₁ a b} → fcmp id f ≡ f
       left-id {f = s} = ≡-refl
       left-id {f = t} = ≡-refl
       left-id {f = id} = ≡-refl

  toFunc : Graph → Functor 𝒢 𝒮e𝓉
  toFunc G = record
    { obj  = ⟦_⟧₀
    ; mor  = ⟦_⟧₁
    ; id   = ≡-refl
    ; comp = λ {x y z f g} → fcmp-⨾ {x} {y} {z} {f} {g}
    }
    where
      ⟦_⟧₀ : Obj 𝒢 → Obj 𝒮e𝓉
      ⟦ 𝒢₀.V ⟧₀ = Graph.V G
      ⟦ 𝒢₀.E ⟧₀ = Σ x ∶ Graph.V G • Σ y ∶ Graph.V G • Graph._⟶_ G x y

      ⟦_⟧₁ : ∀ {x y : Obj 𝒢} → x ⟶ y → (⟦ x ⟧₀ → ⟦ y ⟧₀)
      ⟦ s ⟧₁ (src , tgt , edg) = src
      ⟦ t ⟧₁ (src , tgt , edg) = tgt
      ⟦ id ⟧₁ x = x

      -- Exercise: fcmp is realised as functional composition
      fcmp-⨾ : ∀{x y z} {f : 𝒢₁ x y} {g : 𝒢₁ y z} → ⟦ fcmp f g ⟧₁ ≡ ⟦ f ⟧₁ ⨾ ⟦ g ⟧₁

      fcmp-⨾ {f = s} {id} = ≡-refl
      fcmp-⨾ {f = t} {id} = ≡-refl
      fcmp-⨾ {f = id} {s} = ≡-refl
      fcmp-⨾ {f = id} {t} = ≡-refl
      fcmp-⨾ {f = id} {id} = ≡-refl

  fromFunc : Functor 𝒢 𝒮e𝓉 → Graph
  fromFunc F = record {
      V      = obj F 𝒢₀.V
    ; _⟶_    = λ x y → Σ e ∶ obj F 𝒢₀.E • src e ≡ x × tgt e ≡ y
             -- the type of edges whose source is x and target is y
    }
    where tgt src : obj F 𝒢₀.E → obj F 𝒢₀.V
          src = mor F 𝒢₁.s
          tgt = mor F 𝒢₁.t

 _ᵒᵖ : ∀ {i j} → Category {i} {j} → Category {i} {j}
 𝒞 ᵒᵖ         = record {
      Obj     = Obj 𝒞
    ; _⟶_     = λ A B → (B ⟶ A)
    ; _⨾_     = λ f g → (g ⨾ f)
    ; assoc   = ≡-sym assoc
    ; Id      = Id
    ; leftId  = rightId
    ; rightId = leftId
    }
    where instance 𝒞′ : Category ; 𝒞′ = 𝒞

 infix 10 _∘_
 _∘_ : ∀ {i j } ⦃ 𝒞 : Category {i} {j}⦄ {A B C : Obj 𝒞} → B ⟶ C →  A ⟶ B → A ⟶ C
 f ∘ g = g ⨾ f

 -- this only changes type
 opify : ∀ {i j i’ j’} {𝒞 : Category {i} {j}} {𝒟 : Category {i’} {j’}}
      → Functor 𝒞 𝒟 → Functor (𝒞 ᵒᵖ) (𝒟 ᵒᵖ)
 opify F = record { obj   =  obj F
                  ; mor   =  mor F
                  ; id    =  Functor.id F
                  ; comp  =  Functor.comp F
                  }

 ∂ : ∀ {i j} → Functor (𝒞𝒶𝓉 {i} {j}) 𝒞𝒶𝓉
 ∂ = record { obj = _ᵒᵖ ; mor = opify ; id = ≡-refl ; comp = ≡-refl }

 ah-yeah : ∀ {i j} (let Cat = Obj (𝒞𝒶𝓉 {i} {j}))
     -- identity on objects cofunctor, sometimes denoted _˘
     → (dual : ∀ (𝒞 : Cat) {x y : Obj 𝒞}  →  x ⟶ y ∶ 𝒞  →  y ⟶ x ∶ 𝒞)
     → (Id˘ : ∀ ⦃ 𝒞 : Cat ⦄ {x : Obj 𝒞} → dual 𝒞 Id  ≡  Id {A = x})
     → (⨾-˘ : ∀ ⦃ 𝒞 : Cat ⦄ {x y z : Obj 𝒞} {f : x ⟶ y} {g : y ⟶ z}
            → dual 𝒞 (f ⨾ g ∶ 𝒞)  ≡  (dual 𝒞 g) ⨾ (dual 𝒞 f) ∶ 𝒞)
     -- which is involutionary
     → (˘˘ : ∀ ⦃ 𝒞 : Cat ⦄ {x y : Obj 𝒞} {f : x ⟶ y} → dual 𝒞 (dual 𝒞 f) ≡ f)
     -- which is respected by other functors
     → (respect : ⦃ 𝒞 𝒟 : Cat ⦄ {F : 𝒞 ⟶ 𝒟} {x y : Obj 𝒞} {f : x ⟶ y}
                → mor F (dual 𝒞 f) ≡ dual 𝒟 (mor F f))
     -- then
     → ∂ ≅ Id within Func (𝒞𝒶𝓉 {i} {j}) 𝒞𝒶𝓉

 ah-yeah {i} {j} _˘ Id˘ ⨾-˘ ˘˘ respect = record
   { to = II
   ; from = JJ
   ; lid = nattransext {𝒞 = 𝒞𝒶𝓉} {𝒞𝒶𝓉} {∂} {∂} (Category._⨾_ 𝒩𝓉 {∂} {Id} {∂} II JJ) (Category.Id 𝒩𝓉 {∂}) λ {𝒞} → funcext ≡-refl (≡-sym (˘˘ ⦃ 𝒞 ⦄ ))
   ; rid = nattransext {𝒞 = 𝒞𝒶𝓉} {𝒞𝒶𝓉} {Id} {Id} (Category._⨾_ 𝒩𝓉 {Id} {∂} {Id} JJ II) (Category.Id 𝒩𝓉 {Id}) λ {𝒞} → funcext ≡-refl (≡-sym (˘˘ ⦃ 𝒞 ⦄))
   }
   where

     𝒩𝓉 = Func (𝒞𝒶𝓉 {i} {j}) (𝒞𝒶𝓉 {i} {j}) -- the category of ~𝒩~atural transormations as morphisms

     I : ⦃ 𝒞 : Category {i} {j} ⦄ → Functor (obj ∂ 𝒞) 𝒞
     I ⦃ 𝒞 ⦄ = record { obj = Id ; mor = _˘ 𝒞 ; id = Id˘ ; comp = ⨾-˘ }

     _⨾f_ = Category._⨾_ (𝒞𝒶𝓉 {i} {j})

     Inat : ⦃ 𝒞 𝒟 : Category {i} {j} ⦄ {F : Functor 𝒞 𝒟} → mor ∂ F ⨾f I ⦃ 𝒟 ⦄  ≡  I ⦃ 𝒞 ⦄ ⨾f F
     Inat ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F} = funcext ⦃ 𝒞 = 𝒞 ᵒᵖ ⦄ ⦃ 𝒟 ⦄ { mor ∂ F ⨾f I ⦃ 𝒟 ⦄ } { I ⦃ 𝒞 ⦄ ⨾f F } ≡-refl λ {x} {y} {f} → respect ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F} {y} {x} {f}

     II : NatTrans ∂ Id
     II = I , (λ {𝒞} {𝒟} {F} → Inat ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F})

     J : ⦃ 𝒞 : Category {i} {j} ⦄ → 𝒞 ⟶ obj ∂ 𝒞
     J ⦃ 𝒞 ⦄ = record { obj = Id ; mor = _˘ 𝒞 ; id = Id˘ ; comp = ⨾-˘ }

     Jnat : ⦃ 𝒞 𝒟 : Category {i} {j} ⦄ {F : 𝒞 ⟶ 𝒟}  →  F ⨾f J ⦃ 𝒟 ⦄  ≡  J ⦃ 𝒞 ⦄ ⨾f mor ∂ F
     Jnat ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F} = funcext ⦃ 𝒞 = 𝒞 ⦄ ⦃ 𝒟 ᵒᵖ ⦄ {F ⨾f J ⦃ 𝒟 ⦄} {J ⦃ 𝒞 ⦄ ⨾f mor ∂ F} ≡-refl (λ {x y f} → respect ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F} {x} {y} {f})

     JJ : NatTrans ⦃ 𝒞𝒶𝓉 {i} {j} ⦄ ⦃ 𝒞𝒶𝓉 ⦄ Id ∂
     JJ = J , (λ {𝒞} {𝒟} {F} → Jnat ⦃ 𝒞 ⦄ ⦃ 𝒟 ⦄ {F})

 infix 5 _⊗_
 _⊗_ : ∀ {i j i’ j’} → Category {i} {j} → Category {i’} {j’} → Category {i ⊍ i’} {j ⊍ j’}
 𝒞 ⊗ 𝒟 = record
           { Obj = Obj 𝒞 × Obj 𝒟
           ; _⟶_ = λ{ (A , X) (B , Y)  →  (A ⟶ B) × (X ⟶ Y) }
           ; _⨾_ = λ{ (f , k) (g , l) → (f ⨾ g , k ⨾ l) }
           ; assoc = assoc ≡×≡ assoc
           ; Id = Id , Id
           ; leftId = leftId ≡×≡ leftId
           ; rightId = rightId ≡×≡ rightId
           }
           where
             _≡×≡_ : ∀ {i j} {A : Set i} {B : Set j} {a a’ : A} {b b’ : B} → a ≡ a’ → b ≡ b’ → (a , b) ≡ (a’ , b’)
             ≡-refl ≡×≡ ≡-refl = ≡-refl
             instance
               𝒞′ : Category
               𝒞′ = 𝒞
               𝒟′ : Category
               𝒟′ = 𝒟

 Fst : ∀ {i j i’ j’} {𝒞 : Category {i} {j}} {𝒟 : Category {i’} {j’}}
     → Functor (𝒞 ⊗ 𝒟) 𝒞
 Fst = record { obj = proj₁ ; mor = proj₁ ; id = ≡-refl ; comp = ≡-refl }

 Snd : ∀ {i j i’ j’} {𝒞 : Category {i} {j}} {𝒟 : Category {i’} {j’}}
     → Functor (𝒞 ⊗ 𝒟) 𝒟
 Snd = record { obj = proj₂ ; mor = proj₂ ; id = ≡-refl ; comp = ≡-refl }

 curry₂ : ∀ {ix jx iy jy iz jz} ⦃ 𝒳 : Category {ix} {jx} ⦄ ⦃ 𝒴 : Category {iy} {jy} ⦄ ⦃ 𝒵 : Category {iz} {jz} ⦄
         → Functor (𝒳 ⊗ 𝒴) 𝒵 → Functor 𝒴 (Func 𝒳 𝒵)
 curry₂ ⦃ 𝒳 = 𝒳 ⦄ ⦃ 𝒴 ⦄ ⦃ 𝒵 ⦄ F = record {
    obj =  funcify
  ; mor =  natify
  ; id =  λ {x} → nattransext {F = funcify x} {funcify x} (natify (Id {A = x})) (Category.Id (Func 𝒳 𝒵) {A = funcify x}) (Functor.id F)
  ; comp =  λ {x y z f g} → nattransext {F = funcify x} {funcify z} (natify (f ⨾ g)) ( Category._⨾_ (Func 𝒳 𝒵) {A = funcify x} {B = funcify y} {C = funcify z} (natify f) (natify g) ) (begin
             mor F (Id , f 𝒴.⨾ g)
           ≡⟨ ≡-cong (λ e → mor F (e , f 𝒴.⨾ g)) (≡-sym 𝒳.rightId) ⟩
             mor F (Id 𝒳.⨾ Id , f 𝒴.⨾ g)
           ≡⟨ functor F preserves-composition ⟩
             mor F (Id , f) 𝒵.⨾ mor F (Id , g)
           ∎) }
  where
        module 𝒳 = Category 𝒳
        module 𝒴 = Category 𝒴
        module 𝒵 = Category 𝒵
        funcify : (y : Obj 𝒴) → Functor 𝒳 𝒵
        funcify = λ Y → record {
            obj = λ X → obj F (X , Y)
          ; mor = λ f → mor F (f , Id ⦃ 𝒴 ⦄ {A = Y})
          ; id = Functor.id F
          ; comp = λ {x y z f g} → begin
                mor F (f 𝒳.⨾ g , Id ⦃ 𝒴 ⦄)
              ≡⟨ ≡-cong (λ x → mor F (f 𝒳.⨾ g , x)) (≡-sym 𝒴.rightId) ⟩
                mor F (f 𝒳.⨾ g , Id 𝒴.⨾ Id)
              ≡⟨ Functor.comp F ⟩
                mor F (f , Id ⦃ 𝒴 ⦄) 𝒵.⨾ mor F (g , Id ⦃ 𝒴 ⦄)
              ∎ }

        natify : {x y : Obj 𝒴} → x 𝒴.⟶ y → NatTrans (funcify x) (funcify y)
        natify {x} {y} f = (λ {z} → mor F (Id {A = z} , f)) , (λ {a b g} → begin
                mor F (g , Id) 𝒵.⨾ mor F (Id , f)
              ≡⟨ ≡-sym (functor F preserves-composition) ⟩
                 mor F (g 𝒳.⨾ Id , Id 𝒴.⨾ f)
              ≡⟨ ≡-cong₂ (λ x y → mor F (x , y)) 𝒳.rightId 𝒴.leftId ⟩
                 mor F (g , f)
              ≡⟨ ≡-sym (≡-cong₂ (λ x y → mor F (x , y)) 𝒳.leftId 𝒴.rightId) ⟩
                 mor F (Id 𝒳.⨾ g , f 𝒴.⨾ Id)
              ≡⟨ functor F preserves-composition ⟩
                mor F (Id , f) 𝒵.⨾ mor F (g , Id)
              ∎)

 pointwise : ∀ {ic jc id jd ix jx iy jy} {𝒞 : Category {ic} {jc}} {𝒟 : Category {id} {jd}}
   {𝒳 : Category {ix} {jx}} {𝒴 : Category {iy} {jy}}
   (_⊕_ : Functor (𝒳 ⊗ 𝒴) 𝒟) (F : Functor 𝒞 𝒳) (G : Functor 𝒞 𝒴) → Functor 𝒞 𝒟
 pointwise {𝒞 = 𝒞} {𝒟} {𝒳} {𝒴} Bi F G =
   let module 𝒳 = Category 𝒳
       module 𝒴 = Category 𝒴
       module 𝒞 = Category 𝒞
       module 𝒟 = Category 𝒟
   in record {
     obj = λ C → obj Bi (obj F C , obj G C)
   ; mor = λ {x y} x→y → mor Bi (mor F x→y , mor G x→y)
   ; id = λ {x} → begin
          mor Bi (mor F 𝒞.Id , mor G 𝒞.Id)
        ≡⟨ ≡-cong₂ (λ f g → mor Bi (f , g)) (Functor.id F) (Functor.id G) ⟩
          mor Bi (𝒳.Id , 𝒴.Id)
        ≡⟨ functor Bi preserves-identities ⟩
          𝒟.Id
        ∎
   ; comp = λ {x y z x⟶y y⟶z} → begin
       mor Bi (mor F (x⟶y 𝒞.⨾ y⟶z) , mor G (x⟶y 𝒞.⨾ y⟶z))
     ≡⟨ ≡-cong₂ (λ f g → mor Bi (f , g)) (Functor.comp F) (Functor.comp G) ⟩
       mor Bi (mor F x⟶y 𝒳.⨾ mor F y⟶z , mor G x⟶y 𝒴.⨾ mor G y⟶z)
     ≡⟨ functor Bi preserves-composition ⟩
      (mor Bi (mor F x⟶y , mor G x⟶y)) 𝒟.⨾ (mor Bi (mor F y⟶z , mor G y⟶z))
     ∎
     }

 exempli-gratia : ∀ {𝒞 𝒟 𝒳 𝒴 : Category {ℓ₀} {ℓ₀}} (⊕ : Functor (𝒳 ⊗ 𝒴) 𝒟)
                → let _⟨⊕⟩_ = pointwise ⊕
                   in
                      Fst ⟨⊕⟩ Snd ≡ ⊕
 exempli-gratia Bi = funcext (≡-cong (obj Bi) ≡-refl) (≡-cong (mor Bi) ≡-refl)

 Hom : ∀ {i j} {𝒞 : Category {i} {j} } → Functor (𝒞 ᵒᵖ ⊗ 𝒞) (𝒮e𝓉 {j})
   -- hence contravariant in ‘first arg’ and covaraint in ‘second arg’
 Hom {𝒞 = 𝒞} =
   let
     module 𝒞 = Category 𝒞
     instance 𝒞′ : Category ; 𝒞′ = 𝒞
     ⨾-cong₂ : ∀ {A B C : Obj 𝒞} {f : A 𝒞.⟶ B} {g g’ : B 𝒞.⟶ C}
             → g ≡ g’ → f 𝒞.⨾ g ≡ f 𝒞.⨾ g’
     ⨾-cong₂  q  =  ≡-cong₂ 𝒞._⨾_ ≡-refl q
   in record {
     obj = λ{ (A , B) →  A ⟶ B }
   ; mor = λ{ (f , g) → λ h → f ⨾ h ⨾ g }
   ; id = extensionality (λ {h} → begin
        Id 𝒞.⨾ h 𝒞.⨾ Id
      ≡⟨ leftId ⟩
        h 𝒞.⨾ Id
      ≡⟨ rightId ⟩
        h
      ∎)
   ; comp =  λ {x y z fg fg’} →
       let (f , g) = fg ; (f’ , g’) = fg’ in extensionality (λ {h} → begin
            (f’ 𝒞.⨾ f) 𝒞.⨾ h 𝒞.⨾ (g 𝒞.⨾ g’)
          ≡⟨ assoc ⟩
            f’ 𝒞.⨾ (f 𝒞.⨾ (h 𝒞.⨾ (g 𝒞.⨾ g’)))
          ≡⟨ ⨾-cong₂ (≡-sym assoc) ⟩
            f’ 𝒞.⨾ ((f 𝒞.⨾ h) 𝒞.⨾ (g 𝒞.⨾ g’))
          ≡⟨ ⨾-cong₂ (≡-sym assoc) ⟩
            f’ 𝒞.⨾ ((f 𝒞.⨾ h) 𝒞.⨾ g) 𝒞.⨾ g’
          ≡⟨ ⨾-cong₂ (≡-cong₂ 𝒞._⨾_ assoc ≡-refl) ⟩
            f’ 𝒞.⨾ (f 𝒞.⨾ h 𝒞.⨾ g) 𝒞.⨾ g’
          ∎)
     }

 _⊣₀_ : ∀ {i j} {𝒞 𝒟 : Category {i} {j}} → Functor 𝒞 𝒟 → Functor 𝒟 𝒞 → Set (i ⊍ j)
 _⊣₀_ {𝒞 = 𝒞} {𝒟} F G
    =
      (F ′ ∘ X  ⟶ₙₐₜ Y)  ≅  (X ⟶ₙₐₜ G ∘ Y)  within  Func (𝒞 ᵒᵖ ⊗ 𝒟) 𝒮e𝓉
   where
     X = Fst ; Y = Snd ; _′ = opify -- only changes types

     infix 5 _⟶ₙₐₜ_
     _⟶ₙₐₜ_ : ∀ {i j} {𝒜 : Category {i} {j}} →
            Functor (𝒞 ᵒᵖ ⊗ 𝒟) (𝒜 ᵒᵖ) → Functor (𝒞 ᵒᵖ ⊗ 𝒟) 𝒜 → Functor (𝒞 ᵒᵖ ⊗ 𝒟) 𝒮e𝓉
     _⟶ₙₐₜ_ {i} {j} {𝒜} = pointwise (Hom {i} {j} {𝒜})

 record _⊣_ {i j i’ j’} {𝒞 : Category {i} {j}} {𝒟 : Category {i’} {j’}}
        (F : Functor 𝒞 𝒟) (G : Functor 𝒟 𝒞)
        : Set (j’ ⊍ i’ ⊍ j ⊍ i) where

   open Category 𝒟 renaming (_⨾_ to _⨾₂_)
   open Category 𝒞 renaming (_⨾_ to _⨾₁_)
   field
     -- ‘left-adjunct’  L ≈ ⌊  and  ‘right-adjunct’  r ≈ ⌈
     ⌊_⌋ : ∀ {X Y} →   obj F X ⟶ Y ∶ 𝒟   →   X ⟶ obj G Y ∶ 𝒞
     ⌈_⌉ : ∀ {X Y} →   X ⟶ obj G Y ∶ 𝒞   →   obj F X ⟶ Y ∶ 𝒟

     -- Adjuncts are inverse operations
     lid : ∀ {X Y} {d : obj F X ⟶ Y ∶ 𝒟} → ⌈ ⌊ d ⌋ ⌉ ≡ d
     rid : ∀ {X Y} {c : X ⟶ obj G Y ∶ 𝒞} → ⌊ ⌈ c ⌉ ⌋ ≡ c

     -- That for a fixed argument, are natural transformations between Hom functors
     lfusion : ∀ {A B C D} {f : A ⟶ B ∶ 𝒞} {ψ : obj F B ⟶ C ∶ 𝒟} {g : C ⟶ D ∶ 𝒟}
             →  ⌊ mor F f ⨾₂ ψ ⨾₂ g ⌋  ≡  f ⨾₁ ⌊ ψ ⌋ ⨾₁ mor G g
     rfusion : ∀ {A B C D} {f : A ⟶ B ∶ 𝒞} {ψ : B ⟶ obj G C ∶ 𝒞} {g : C ⟶ D ∶ 𝒟}
             →  ⌈ f ⨾₁ ψ ⨾₁ mor G g ⌉  ≡  mor F f ⨾₂ ⌈ ψ ⌉ ⨾₂ g

Path₀ : ℕ → Graph₀ → Set (ℓsuc ℓ₀)
Path₀ n G = [ n ]₀ 𝒢⟶₀ G

open import Data.Vec using (Vec ; lookup)

record Path₁ (n : ℕ) (G : Graph₀) : Set (ℓsuc ℓ₀) where
  open Graph₀
  field
    edges     : Vec (E G) (suc n)
    coherency : {i : Fin n} → tgt G (lookup (` i) edges) ≡ src G (lookup (fsuc i) edges)

module Path-definition-2 (G : Graph₀) where
  open Graph₀ G

  mutual
    data Path₂ : Set where
      _!   : V → Path₂
      cons : (v : V) (e : E) (ps : Path₂) (s : v ≡ src e) (t : tgt e ≡ head₂ ps) → Path₂

    head₂ : Path₂ → V
    head₂ (v !) = v
    head₂ (cons v e p s t) = v

module Path-definition-3 (G : Graph) where

  open Graph G

  -- handy dandy syntax
  infixr 5 cons
  syntax cons v ps e = v ⟶[ e ]⟶ ps -- v goes, by e, onto path ps

  -- we want well-formed paths
  mutual
    data Path₃ : Set where
      _!   : (v : V) → Path₃
      cons : (v : V) (ps : Path₃) (e : v ⟶ head₃ ps) → Path₃

    head₃ : Path₃ → V
    head₃ (v !) = v
    head₃ (v ⟶[ e ]⟶ ps) = v

  -- motivation for the syntax declaration above
  example : (v₁ v₂ v₃ : V) (e₁ : v₁ ⟶ v₂) (e₂ : v₂ ⟶ v₃) → Path₃
  example v₁ v₂ v₃ e₁ e₂ = v₁ ⟶[ e₁ ]⟶ v₂ ⟶[ e₂ ]⟶ v₃ !

  end₃ : Path₃ → V
  end₃ (v !) = v
  end₃ (v ⟶[ e ]⟶ ps) = end₃ ps

  -- typed paths; squigarrowright
  record _⇝_ (x y : V) : Set where
    field
      path   : Path₃
      start  : head₃ path ≡ x
      finish : end₃ path  ≡ y

module TypedPaths (G : Graph) where

  open Graph G hiding(V)
  open Graph   using (V)

  data _⇝_ : V G → V G → Set where
    _!      : ∀ x → x ⇝ x
    _⟶[_]⟶_ : ∀ x {y ω} (e : x ⟶ y) (ps : y ⇝ ω) → x ⇝ ω

  -- Preprend preserves path equality
  ⟶-≡ : ∀{x y ω} {e : x ⟶ y} {ps qs : y ⇝ ω}
      → ps ≡ qs → (x ⟶[ e ]⟶ ps) ≡ (x ⟶[ e ]⟶ qs)
  ⟶-≡ {x} {y} {ω} {e} {ps} {qs} eq = ≡-cong (λ r → x ⟶[ e ]⟶ r) eq

  open import Data.List using (List ; [] ; _∷_)
  edges : ∀ {x ω} (p : x ⇝ ω) → List (Σ s ∶ V G • Σ t ∶ V G • s ⟶ t)
  edges {x} (.x !) = []
  edges {x} (.x ⟶[ e ]⟶ ps) = (x , _ , e) ∷ edges ps

  path-eq : ∀ {x y} {p q : x ⇝ y} → edges p ≡ edges q → p ≡ q
  path-eq {x} {p = .x !} {q = .x !} pf = ≡-refl
  path-eq {x} {p = .x !} {q = .x ⟶[ e ]⟶ q} ()
  path-eq {x} {p = .x ⟶[ e ]⟶ p} {q = .x !} ()
  path-eq {x} {p = .x ⟶[ e ]⟶ p} {q = .x ⟶[ e₁ ]⟶ q} pf with edges p | pf
  path-eq {x} {p = .x ⟶[ e ]⟶ p} {q = .x ⟶[ .e ]⟶ q} pf | .(edges q) | ≡-refl = ⟶-≡ (path-eq (uncons pf))
    where uncons : ∀{A : Set} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
          uncons {A} {x} {.x} {xs} {.xs} ≡-refl = ≡-refl

  infixr 5 _++_

  _++_ : ∀{x y z} → x ⇝ y → y ⇝ z → x ⇝ z
  x ! ++ q           = q                         -- left unit
  (x ⟶[ e ]⟶ p) ++ q = x ⟶[ e ]⟶ (p ++ q)     -- mutual-associativity

  leftId : ∀ {x y} {p : x ⇝ y} → x ! ++ p ≡ p
  leftId = ≡-refl

  rightId : ∀ {x y} {p : x ⇝ y} → p ++ y ! ≡ p
  rightId {x} {.x} {.x !} = ≡-refl
  rightId {x} {y } {.x ⟶[ e ]⟶ ps} = ≡-cong (λ q → x ⟶[ e ]⟶ q) rightId

  assoc : ∀{x y z ω} {p : x ⇝ y} {q : y ⇝ z} {r : z ⇝ ω}
        → (p ++ q) ++ r ≡ p ++ (q ++ r)
  assoc {x} {p = .x !} = ≡-refl
  assoc {x} {p = .x ⟶[ e ]⟶ ps} {q} {r} = ≡-cong (λ s → x ⟶[ e ]⟶ s) (assoc {p = ps})

𝒫₀ : Graph → Category
𝒫₀ G = let open TypedPaths G in
    record
      { Obj     = Graph.V G
      ; _⟶_     = _⇝_
      ; _⨾_     = _++_
      ; assoc   = λ {x y z ω p q r} → assoc {p = p}
      ; Id      = λ {x} → x !
      ; leftId  = leftId
      ; rightId = rightId
      }

𝒫₁ : ∀ {G H} → GraphMap G H → Functor (𝒫₀ G) (𝒫₀ H)
𝒫₁ {G} {H} f = record
    { obj  = ver f
    ; mor  = amore
    ; id   = ≡-refl
    ; comp = λ {x} {y} {z} {p} → comp {p = p}
    }
    where
      open TypedPaths ⦃...⦄ public
      instance G' : Graph ; G' = G
               H' : Graph ; H' = H

      amore : {x y : Graph.V G} →  x ⇝ y → (ver f x) ⇝ (ver f y)
      amore (x !) = ver f x !
      amore (x ⟶[ e ]⟶ p) = ver f x ⟶[ edge f e ]⟶ amore p

      comp : {x y z : Graph.V G} {p : x ⇝ y} {q : y ⇝ z}
          →  amore (p ++ q)  ≡  amore p ++ amore q
      comp {x} {p = .x !} = ≡-refl    -- since ! is left unit of ++
      comp {x} {p = .x ⟶[ e ]⟶ ps} = ⟶-≡ (comp {p = ps})

𝒫 : Functor 𝒢𝓇𝒶𝓅𝒽 𝒞𝒶𝓉
𝒫 = record { obj   = 𝒫₀
            ; mor  = 𝒫₁
            ; id   = λ {G} → funcext ≡-refl (id ⦃ G ⦄)
            ; comp = funcext ≡-refl comp
            }
    where
      open TypedPaths ⦃...⦄
      open Category   ⦃...⦄

      module 𝒞𝒶𝓉   = Category 𝒞𝒶𝓉
      module 𝒢𝓇𝒶𝓅𝒽 = Category 𝒢𝓇𝒶𝓅𝒽

      id : ∀ ⦃ G ⦄ {x y} {p : x ⇝ y}
        →   mor (𝒞𝒶𝓉.Id {𝒫₀ G}) p  ≡  mor (𝒫₁ (𝒢𝓇𝒶𝓅𝒽.Id)) p
      id {p = x !} = ≡-refl
      id {p = x ⟶[ e ]⟶ ps} = ⟶-≡ (id {p = ps})

      comp : {G H K : Graph} {f : GraphMap G H} {g : GraphMap H K}
           → {x y : Graph.V G} {p : TypedPaths._⇝_ G x y}
           →  mor (𝒫₁ f 𝒞𝒶𝓉.⨾ 𝒫₁ g) p  ≡  mor (𝒫₁ (f 𝒢𝓇𝒶𝓅𝒽.⨾ g)) p
      comp {p = x !} = ≡-refl
      comp {p = x ⟶[ e ]⟶ ps} = ⟶-≡ (comp {p = ps})

module freedom (G : Obj 𝒢𝓇𝒶𝓅𝒽) {𝒞 : Category {ℓ₀} {ℓ₀} } where

  open TypedPaths G using (_! ; _⟶[_]⟶_ ;  _⇝_ ; _++_)
  open Category ⦃...⦄

  module 𝒢𝓇𝒶𝓅𝒽 = Category 𝒢𝓇𝒶𝓅𝒽
  module 𝒮ℯ𝓉 = Category (𝒮e𝓉 {ℓ₀})
  module 𝒞 = Category 𝒞
  instance 𝒞′ : Category ; 𝒞′ = 𝒞

  ι : G ⟶ 𝒰₀ (𝒫₀ G)
  ι = record { ver = Id ; edge = λ {x} {y} e  →  x ⟶[ e ]⟶ (y !) }

  lift : G ⟶ 𝒰₀ 𝒞  →  𝒫₀ G ⟶ 𝒞
  lift f = record
     { obj  = λ v → ver f v -- Only way to obtain an object of 𝒞; hope it works!
     ; mor  = fmap
     ; id   = ≡-refl
     ; comp = λ {x y z p q} → proof {x} {y} {z} {p} {q}
     }
     where
          fmap : ∀ {x y} → x ⇝ y → ver f x 𝒞.⟶ ver f y
          fmap (y !) = 𝒞.Id
          fmap (x ⟶[ e ]⟶ p) = edge f e 𝒞.⨾ fmap p

          -- homomorphism property
          proof : ∀{x y z} {p : x ⇝ y} {q : y ⇝ z} → fmap (p ++ q) ≡ fmap p 𝒞.⨾ fmap q
          proof {p = ._ !} = ≡-sym 𝒞.leftId
          proof {p = ._ ⟶[ e ]⟶ ps} =  ≡-cong (λ m → edge f e 𝒞.⨾ m) (proof {p = ps})
                                     ⟨≡≡⟩ ≡-sym assoc
                                     -- Exercise: Rewrite this calculationally!

  property : ∀{f : G ⟶ 𝒰₀ 𝒞}  →  f  ≡  (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ (lift f))
  property {f} = graphmapext
    -- Proving: ∀ {v} → ver f v ≡ ver (ι 𝒞.⨾ 𝒰₁ (lift f)) v
    -- by starting at the complicated side and simplifying
    (λ {v} → ≡-sym (begin
              ver (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ (lift f)) v
            ≡⟨" definition of ver on composition "⟩′
              (ver ι 𝒮ℯ𝓉.⨾ ver (𝒰₁ (lift f))) v
            ≡⟨" definition of 𝒰₁ says: ver (𝒰₁ F) = obj F "⟩′
              (ver ι 𝒮ℯ𝓉.⨾ obj (lift f)) v
            ≡⟨" definition of lift says: obj (lift f) = ver f "⟩′
              (ver ι 𝒮ℯ𝓉.⨾ ver f) v
            ≡⟨" definition of ι on vertices is identity "⟩′
              ver f v
            ∎))

    -- Proving: edge (ι ⨾g 𝒰₁ (lift f)) e ≡ edge f e
    (λ {x} {y} {e} → begin
               edge (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ (lift f)) e
             ≡⟨" definition of edge on composition "⟩′
               (edge ι 𝒮ℯ𝓉.⨾ edge (𝒰₁ (lift f))) e
             ≡⟨" definition of 𝒰 says: edge (𝒰₁ F) = mor F "⟩′
               (edge ι 𝒮ℯ𝓉.⨾ mor (lift f)) e
             ≡⟨" definition chasing gives: mor (lift f) (edge ι e) = edge f e ⨾ Id "⟩′
               edge f e 𝒞.⨾ Id
             ≡⟨ 𝒞.rightId ⟩
               edge f e
             ∎)

  uniqueness : ∀{f : G ⟶ 𝒰₀ 𝒞} {F : 𝒫₀ G ⟶ 𝒞} → f ≡ (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F) → lift f ≡ F
  uniqueness {.(ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)} {F} ≡-refl = funcext ≡-refl (≡-sym pf)
    where
      pf : ∀{x y} {p : x ⇝ y} →  mor (lift (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) p  ≡  mor F p
      pf {x} {.x} {p = .x !} = ≡-sym (Functor.id F)
      pf {x} {y} {p = .x ⟶[ e ]⟶ ps} = begin
         mor (lift (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) (x ⟶[ e ]⟶ ps)
       ≡⟨" definition of mor on lift, the inductive clause "⟩′
         edge (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F) e 𝒞.⨾ mor (lift (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) ps
       ≡⟨ ≡-cong₂ 𝒞._⨾_ ≡-refl (pf {p = ps}) ⟩ -- inductive step
         edge (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F) e 𝒞.⨾ mor F ps
       ≡⟨" definition of edge says it preserves composition "⟩′
         (edge ι 𝒮ℯ𝓉.⨾ edge (𝒰₁ F)) e 𝒞.⨾ mor F ps
       ≡⟨" definition of 𝒰 gives: edge (𝒰₁ F) = mor F "⟩′
         (edge ι 𝒮ℯ𝓉.⨾ mor F) e 𝒞.⨾ mor F ps
       ≡⟨" definition of functional composition 𝒮ℯ𝓉 "⟩′
          mor F (edge ι e) 𝒞.⨾ mor F ps
       ≡⟨ ≡-sym (Functor.comp F) {- i.e., functors preserve composition -} ⟩
          mor F (edge ι e ++ ps)
       ≡⟨" definition of embedding and concatenation "⟩′
         mor F (x ⟶[ e ]⟶ ps)
       ∎

  _≈g_ : ∀{G H : Graph} (f g : G ⟶ H) → Set
  _≈g_ {G} {H} f g = Σ veq ∶ (∀ {v} → ver f v ≡ ver g v) •
    (∀ {x y e} → edge g {x} {y} e ≡ ≡-subst₂ (λ a b → Graph._⟶_ H a b) veq veq (edge f {x} {y} e))

  _≋_ : ∀{𝒞 𝒟 : Category} (f g : 𝒞 ⟶ 𝒟) → Set
  F ≋ G = 𝒰₁ F ≈g 𝒰₁ G   -- proofs (x , y) now replaced with: funcext x y

-- Since equality of functors makes use of ~subst~s all over the place, we will need
-- a lemma about how ~subst~ factors/distributes over an operator composition.
  subst-dist : ∀ {S : Set} {v v’ : S → Category.Obj 𝒞} (veq : ∀ {z} → v z ≡ v’ z)
         → ∀ x t y {ec : v x 𝒞.⟶ v t} {psc : v t 𝒞.⟶ v y}
         →
           ≡-subst₂ 𝒞._⟶_ veq veq ec 𝒞.⨾ ≡-subst₂ 𝒞._⟶_ veq veq psc
         ≡ ≡-subst₂ 𝒞._⟶_ veq veq (ec 𝒞.⨾ psc)
  subst-dist veq x t y rewrite veq {x} | veq {t} | veq {y} = ≡-refl

  uniquenessOld : ∀{f : G ⟶ 𝒰₀ 𝒞} {F : 𝒫₀ G ⟶ 𝒞} → f ≈g (ι ⨾ 𝒰₁ F) → lift f ≡ F
  uniquenessOld {f} {F} (veq , eeq) = funcext veq pf
    where

      𝒮 : ∀{x y} → ver f x 𝒞.⟶ ver f y → obj F x 𝒞.⟶ obj F y
      𝒮 m = ≡-subst₂ 𝒞._⟶_ veq veq m

      pf : ∀{x y} {p : x ⇝ y} → mor F p ≡ 𝒮( mor (lift f) p )
      pf {x} {.x} {.x !} rewrite (veq {x})= Functor.id F
      pf {x} {y}  {.x ⟶[ e ]⟶ ps} rewrite (eeq {e = e}) =  begin
          mor F (x ⟶[ e ]⟶ ps)
       ≡⟨" definition of embedding and concatenation "⟩′
          mor F (edge ι e ++ ps)
       ≡⟨ functor F preserves-composition ⟩
          mor F (edge ι e) 𝒞.⨾ mor F ps
       ≡⟨ ≡-cong₂ 𝒞._⨾_ eeq (pf {p = ps}) ⟩ -- inductive step
          𝒮(edge f e) 𝒞.⨾ 𝒮(mor (lift f) ps)
       ≡⟨ subst-dist veq x _ y ⟩
          𝒮( edge f e 𝒞.⨾ mor (lift f) ps )
       ≡⟨" definition of “mor” on “lift”, the inductive clause "⟩′
          𝒮( mor (lift f) (x ⟶[ e ]⟶ ps) )
       ∎

  lift˘ : Functor (𝒫₀ G) 𝒞 → GraphMap G (𝒰₀ 𝒞)
  lift˘ F =  ι ⨾ 𝒰₁ F  -- ≡ record {ver = obj F , edge = mor F ∘ edge ι}

  rid₀ : ∀ {f : GraphMap G (𝒰₀ 𝒞)} → ver (lift˘ (lift f)) ≡ ver f
  rid₀ {f} = begin
      ver (lift˘ (lift f))
    ≡⟨" ver of lift˘ ; defn of lift˘ "⟩′
      obj (lift f)
    ≡⟨" defn of lift.obj "⟩′
      ver f
    ∎
-- note that ≡-refl would have suffcied, but we show all the steps for clarity, for human consumption!

  open Graph G renaming (_⟶_ to _⟶g_)
  rid₁ : ∀{f : GraphMap G (𝒰₀ 𝒞)} → ∀{x y} {e : x ⟶g y} → edge (lift˘ (lift f)) e ≡ edge f e
  rid₁ {f} {x} {y} {e} = begin
      edge (lift˘ (lift f)) e
    ≡⟨ "lift˘.edge definition" ⟩′
      mor (lift f) (edge ι e)
    ≡⟨ "lift.mor~ on an edge; i.e., the inductive case of fmap" ⟩′
      edge f e 𝒞.⨾ Id
    ≡⟨ 𝒞.rightId ⟩
      edge f e
    ∎

  rid : ∀{f : GraphMap G (𝒰₀ 𝒞)} → lift˘ (lift f) ≡ f
  rid {f} = graphmapext ≡-refl (≡-sym (rid₁ {f}))

  lid₀ : ∀{F : Functor (𝒫₀ G) 𝒞} → obj (lift (lift˘ F)) ≡ obj F
  lid₀ {F} =  begin
      obj (lift (lift˘ F))
    ≡⟨ "obj of lift" ⟩′
      ver (lift˘ F)
    ≡⟨ "ver of lift˘" ⟩′
       obj F
    ∎

  lid₁ : ∀{F : Functor (𝒫₀ G) 𝒞} → ∀ {x y} {p : x ⇝ y} → mor (lift (lift˘ F)) p ≡ mor F p
  lid₁ {F} {x} {.x} {p = (.x) !} = begin
      mor (lift (lift˘ F)) (x !)
    ≡⟨ "mor of lift on !" ⟩′
      𝒞.Id
    ≡⟨ ≡-sym (Functor.id F) ⟩ -- ! is identity path in ~𝒫G~ and functor preserve identites
       mor F (x !)
    ∎
  lid₁ {F} {x} {y} {p = .x ⟶[ e ]⟶ ps} = begin
      mor (lift (lift˘ F)) (x ⟶[ e ]⟶ ps)
    ≡⟨⟩ -- mor on lift on inductive case
      edge (lift˘ F) e 𝒞.⨾ mor (lift (lift˘ F)) ps
    ≡⟨  ≡-cong (λ w → edge (lift˘ F) e 𝒞.⨾ w) (lid₁ {F}) ⟩
      edge (lift˘ F) e 𝒞.⨾ mor F ps
    ≡⟨ "edge on lift˘" ⟩′
      mor F (edge ι e) 𝒞.⨾ mor F ps
    ≡⟨ ≡-sym (Functor.comp F) ⟩ -- factor out Functor.mor
      mor F (edge ι e ++ ps)
    ≡⟨ "defn of ++" ⟩′
      mor F (x ⟶[ e ]⟶ ps)
    ∎

  lid : ∀ {F : Functor (𝒫₀ G) 𝒞} → lift (lift˘ F) ≡ F
  lid  {F} = funcext ≡-refl (≡-sym (lid₁ {F}))

  -- old version
  lift-≈ : ∀{f f’ : GraphMap G (𝒰₀ 𝒞)} → f ≈g f’ → lift f ≋ lift f’
  lift-≈  {f} {f’} (veq , eeq) = veq , (λ {x} {y} {p} → pf {x} {y} {p})
    where
      pf : {x y : V} {p : x ⇝ y} → mor (lift f’) p ≡ ≡-subst₂ 𝒞._⟶_ veq veq (mor (lift f) p)
      pf {x} {.x} {p = .x !} rewrite (veq {x}) = ≡-refl
      pf {x} {y} {p = .x ⟶[ e ]⟶ ps} = begin
           mor (lift f’) (x ⟶[ e ]⟶ ps)
         ≡⟨⟩
           edge f’ e 𝒞.⨾ mor (lift f’) ps
         ≡⟨ ≡-cong₂ 𝒞._⨾_ eeq (pf {p = ps}) ⟩
           ≡-subst₂ 𝒞._⟶_ veq veq (edge f e) 𝒞.⨾ ≡-subst₂ 𝒞._⟶_ veq veq (mor (lift f) ps)
         ≡⟨ subst-dist veq x _ y ⟩
            ≡-subst₂ 𝒞._⟶_ veq veq (mor (lift f) (x ⟶[ e ]⟶ ps))
         ∎

  uniqueness’  :  ∀{f h}   →    f  ≡  (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ h)   →   lift f  ≡  h
  uniqueness’ {f} {h} f≈ι⨾𝒰₁h = begin
      lift f
    ≡⟨ ≡-cong lift f≈ι⨾𝒰₁h ⟩
      lift (ι 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ h)
    ≡⟨" definition of lift˘ "⟩′
      lift (lift˘ h)
    ≡⟨ lid ⟩
      h
    ∎

module _ {G H : Graph} {𝒞 𝒟 : Category {ℓ₀} {ℓ₀}}
          (g : GraphMap G H) (F : Functor 𝒞 𝒟) where

  private
    lift˘ = λ {A} {C} B → freedom.lift˘ A {C} B
    lift = λ {A} {C} B → freedom.lift A {C} B
  open Category ⦃...⦄

  module 𝒞     = Category 𝒞
  module 𝒟     = Category 𝒟
  module 𝒢𝓇𝒶𝓅𝒽 = Category 𝒢𝓇𝒶𝓅𝒽
  module 𝒞𝒶𝓉   = Category (𝒞𝒶𝓉 {ℓ₀} {ℓ₀})
  module 𝒮ℯ𝓉   = Category (𝒮e𝓉 {ℓ₀})

  naturality˘ : ∀ {K : Functor (𝒫₀ H) 𝒞}
              →  lift˘ (𝒫₁ g 𝒞𝒶𝓉.⨾ K 𝒞𝒶𝓉.⨾ F)  ≡  (g 𝒢𝓇𝒶𝓅𝒽.⨾ lift˘ K 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)
  naturality˘ = graphmapext ≡-refl ≡-refl

  naturality : ∀ {k : GraphMap H (𝒰₀ 𝒞)} →     lift (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)
                                              ≡  (𝒫₁ g 𝒞𝒶𝓉.⨾ lift k 𝒞𝒶𝓉.⨾ F)
  naturality {k} = funcext ≡-refl (λ {x y p} → proof {x} {y} {p})
    where
      open TypedPaths ⦃...⦄
      instance G′ : Graph ; G′ = G
               H′ : Graph ; H′ = H
      proof : ∀ {x y : Graph.V G} {p : x ⇝ y}
            →    mor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) p
               ≡  mor (lift {G} {𝒟} (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) p
      proof {p = _ !} = functor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) preserves-identities
      proof {p = x ⟶[ e ]⟶ ps} = begin
            mor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) (x ⟶[ e ]⟶ ps)
         ≡⟨" By definition, “mor” distributes over composition "⟩′
            (mor (𝒫₁ g) 𝒮ℯ𝓉.⨾ mor (lift {H} {𝒞} k) 𝒮ℯ𝓉.⨾ mor F) (x ⟶[ e ]⟶ ps)
         ≡⟨" Definitions of function composition and “𝒫₁ ⨾ mor” "⟩′
            mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) (x ⟶[ e ]⟶ ps)))
                                                  -- This explicit path is in G
         ≡⟨" Lifting graph-map “g” onto a path "⟩′
            mor F (mor (lift {H} {𝒞} k) (ver g x ⟶[ edge g e ]⟶ mor (𝒫₁ g) ps))
                                                  -- This explicit path is in H
         ≡⟨" Definition of “lift ⨾ mor” on inductive case for paths "⟩′
            mor F (edge k (edge g e) 𝒞.⨾ mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
         ≡⟨ functor F preserves-composition ⟩
                mor F (edge k (edge g e))
           𝒟.⨾  mor F (mor (lift {H} {𝒞} k) (mor (𝒫₁ g) ps))
         ≡⟨" Definition of function composition, for top part "⟩′
               (edge g 𝒮ℯ𝓉.⨾ edge k 𝒮ℯ𝓉.⨾ mor F) e  -- ≈ mor F ∘ edge k ∘ edge g
           𝒟.⨾ (mor (𝒫₁ g) 𝒮ℯ𝓉.⨾ mor (lift {H} {𝒞} k) 𝒮ℯ𝓉.⨾ mor F) ps
         ≡⟨" “𝒰₁ ⨾ edge = mor” and “edge” and “mor” are functorial by definition "⟩′
                edge (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F) e
           𝒟.⨾  mor (𝒫₁ g 𝒞𝒶𝓉.⨾ lift {H} {𝒞} k 𝒞𝒶𝓉.⨾ F) ps
         ≡⟨ {- Inductive Hypothesis: -} ≡-cong₂ 𝒟._⨾_ ≡-refl (proof {p = ps}) ⟩
                edge (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F) e
           𝒟.⨾  mor (lift {G} {𝒟} (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) ps
         ≡⟨" Definition of “lift ⨾ mor” on inductive case for paths "⟩′
            mor (lift {G} {𝒟} (g 𝒢𝓇𝒶𝓅𝒽.⨾ k 𝒢𝓇𝒶𝓅𝒽.⨾ 𝒰₁ F)) (x ⟶[ e ]⟶ ps)
         ∎

𝒫⊣𝒰 : 𝒫 ⊣ 𝒰
𝒫⊣𝒰 = record{
    ⌊_⌋ = lift˘
  ; ⌈_⌉ = lift
  ; lid = lid
  ; rid = λ {G 𝒞 c} → rid {G} {𝒞} {c}
  ; lfusion = λ {G H 𝒞 𝒟 f F K} → naturality˘ {G} {H} {𝒞} {𝒟} f K {F}
  ; rfusion = λ {G H 𝒞 𝒟 f k F} → naturality {G} {H} {𝒞} {𝒟} f F {k} }
  where
    module _ {G : Graph} {𝒞 : Category} where open freedom G {𝒞} public

module folding (G : Graph) where
  open TypedPaths G
  open Graph G
                                              -- Given:
  fold : {X : Set} (v : V → X)               -- realise G's vertices as X elements
         (f : ∀ x {y} (e : x ⟶ y) → X → X) -- realise paths as X elements
       → (∀ {a b} → a ⇝ b → X)            -- Then: Any path is an X value
  fold v f (b !) = v b
  fold v f (x ⟶[ e ]⟶ ps) = f x e (fold v f ps)

  length : ∀{x y} → x ⇝ y → ℕ
  length = fold (λ _ → 0)          -- single walks are length 0.
                (λ _ _ n → 1 + n)  -- edges are one more than the
                                    -- length of the remaining walk

  length-! : ∀{x} → length (x !) ≡ 0
  length-! = ≡-refl
  -- True by definition of “length”: The first argument to the “fold”

  length-ind : ∀ {x y ω} {e : x ⟶ y} {ps : y ⇝ ω}
            →  length (x ⟶[ e ]⟶ ps)  ≡  1 + length ps
  length-ind = ≡-refl
  -- True by definition of “length”: The second-argument to the “fold”

  path-cost : (c : ∀{x y}(e : x ⟶ y) → ℕ) → ∀{x y}(ps : x ⇝ y) → ℕ
  path-cost c = fold (λ _ → 0)           -- No cost on an empty path.
                     (λ x e n → c e + n) -- Cost of current edge plus
                                          -- cost of remainder of path.

  fold-++ :  ∀{X : Set} {v : V → X} {g : ∀ x {y} (e : x ⟶ y) → X}
          → (_⊕_ : X → X → X)
          → ∀{x y z : V} {p : x ⇝ y} {q : y ⇝ z}
          → (unitl : ∀{x y} → y ≡ v x ⊕ y)        -- Image of ‘v’ is left unit of ⊕
          → (assoc : ∀ {x y z} → x ⊕ (y ⊕ z) ≡ (x ⊕ y) ⊕ z )  -- ⊕ is associative
          → let f : ∀ x {y} (e : x ⟶ y) → X → X
                f = λ x e ps → g x e ⊕ ps
             in
               fold v f (p ++ q) ≡ fold v f p ⊕ fold v f q
  fold-++ {g = g} _⊕_ {x = x} {p = .x !} unitl assoc =  unitl
  fold-++ {g = g} _⊕_ {x = x} {p = .x ⟶[ e ]⟶ ps} unitl assoc =
    ≡-cong (λ exp → g x e ⊕ exp) (fold-++ _⊕_ {p = ps} unitl assoc) ⟨≡≡⟩ assoc

module lists (A : Set) where

  open import Data.Unit

  listGraph : Graph
  listGraph = record { V = A ; _⟶_ = λ a a’ → ⊤ }

  open TypedPaths listGraph
  open folding listGraph

  -- Every non-empty list [x₀, …, xₖ] of A’s corresonds to a path x₀ ⇝ xₖ.
  toPath : ∀{n} (list : Fin (suc n) → A) →  list fzero ⇝ list (fromℕ n)
  toPath {zero} list = list fzero !
  toPath {suc n} list = list fzero ⟶[ tt ]⟶ toPath {n} (λ i → list(fsuc i))
    -- Note that in the inductive case, “list : Fin (suc (suc n)) → A”
    -- whereas “suc ⨾ list : Fin (suc n) → A”.
    --
    -- For example, if “list ≈ [x , y , z]” yields
    --          “fsuc ⨾ list ≈ [y , z ]” and
    --   “fsuc ⨾ fsuc ⨾ list ≈ [z]”.

  -- List type former
  List = λ (X : Set) → Σ n ∶ ℕ • (Fin n → X)

  -- Usual list folding, but it's in terms of path folding.
  foldr : ∀{B : Set} (f : A → B → B) (e : B) → List A → B
  foldr f e (zero , l) = e
  foldr f e (suc n , l) = fold (λ a → f a e) (λ a _ rem → f a rem) (toPath l)

  -- example
  listLength : List A → ℕ -- result should clearly be “proj₁” of the list, anyhow:
  listLength = foldr
    (λ a rem → 1 + rem) -- Non-empty list has length 1 more than the remainder.
    0                    -- Empty list has length 0.

  -- Empty list
  [] : ∀{X : Set} → List X
  [] = 0 , λ ()

  -- Cons for lists
  _∷_ : ∀{X : Set} → X → List X → List X
  _∷_ {X} x (n , l) = 1 + n , cons x l
    where
      -- “cons a l  ≈  λ i : Fin (1 + n) → if i ≈ 0 then a else l i”
      cons : ∀{n} → X → (Fin n → X) → (Fin (suc n) → X)
      cons x l fzero = x
      cons x l (fsuc i) = l i

  map : ∀ {B} (f : A → B) → List A → List B
  map f =  foldr (λ a rem → f a ∷ rem) []  -- looks like the usual map don’t it ;)

  -- list concatenation
  _++ℓ_ : List A → List A → List A
  l ++ℓ r = foldr _∷_ r l -- fold over ‘l’ by consing its elements infront of ‘r’

  -- Exercise: Write path catenation as a path-fold.


text:
-- Andreas, 2016-12-20, issue #2347, reported by m0davis
-- Case splitting in extended lambda with instance argument
-- was printed wrongly

-- {-# OPTIONS -v interaction.case:100 #-}
-- {-# OPTIONS -v reify:100 #-}
-- {-# OPTIONS -v reify.clause:100 #-}
-- {-# OPTIONS -v extendedlambda:100 #-}
-- {-# OPTIONS -v tc.term.extlam:100 #-}

data ⊥ : Set where

works : ⊥ → Set
works = λ {x → {!x!}}

works1 : { _ : Set } → ⊥ → Set
works1 = λ {x → {!x!}}

test : ⦃ _ : Set ⦄ → ⊥ → Set
test = λ {x → {!x!}}

-- Case splitting on x should succeed in each case


text:
module Cats.Util.SetoidMorphism where

open import Data.Product using (∃-syntax ; _,_ ; proj₁ ; proj₂)
open import Level using (_⊔_ ; suc)
open import Relation.Binary using (Rel ; Setoid ; IsEquivalence ; _Preserves_⟶_)
open import Relation.Binary.SetoidReasoning

open import Cats.Util.Function using () renaming (_∘_ to _⊚_)

open Setoid renaming (_≈_ to eq)

infixr 9 _∘_

record _⇒_ {l l≈} (A : Setoid l l≈) {l′ l≈′} (B : Setoid l′ l≈′)
  : Set (l ⊔ l′ ⊔ l≈ ⊔ l≈′)
  where
  field
    arr : Carrier A → Carrier B
    resp : arr Preserves eq A ⟶ eq B

open _⇒_ public using (arr ; resp)

module _ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′} where

  infixr 4 _≈_

  record _≈_ (f g : A ⇒ B) : Set (l ⊔ l≈ ⊔ l≈′) where
    constructor ≈-intro
    field
       ≈-elim : ∀ {x y} → eq A x y → eq B (arr f x) (arr g y)

    ≈-elim′ : ∀ {x} → eq B (arr f x) (arr g x)
    ≈-elim′ = ≈-elim (refl A)

  open _≈_ public

  equiv : IsEquivalence _≈_
  equiv = record
      { refl = λ {f} → ≈-intro (resp f)
      ; sym = λ eq → ≈-intro λ x≈y → sym B (≈-elim eq (sym A x≈y))
      ; trans = λ eq₁ eq₂ → ≈-intro (λ x≈y → trans B (≈-elim eq₁ x≈y) (≈-elim′ eq₂))
      }

  setoid : Setoid (l ⊔ l≈ ⊔ l′ ⊔ l≈′) (l ⊔ l≈ ⊔ l≈′)
  setoid = record
      { Carrier = A ⇒ B
      ; _≈_ = _≈_
      ; isEquivalence = equiv
      }

id : ∀ {l l≈} {A : Setoid l l≈} → A ⇒ A
id = record { arr = λ x → x ; resp = λ x → x }

_∘_ : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → ∀ {l″ l≈″} {C : Setoid l″ l≈″}
  → B ⇒ C → A ⇒ B → A ⇒ C
_∘_ f g = record
    { arr = arr f ⊚ arr g
    ; resp = resp f ⊚ resp g
    }

∘-resp : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → ∀ {l″ l≈″} {C : Setoid l″ l≈″}
  → {f f′ : B ⇒ C} {g g′ : A ⇒ B}
  → f ≈ f′ → g ≈ g′ → f ∘ g ≈ f′ ∘ g′
∘-resp f≈f′ g≈g′ = ≈-intro (≈-elim f≈f′ ⊚ ≈-elim g≈g′)

id-l : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
   → {f : A ⇒ B}
   → id ∘ f ≈ f
id-l {f = f} = ≈-intro (resp f)

id-r : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → {f : A ⇒ B}
  → f ∘ id ≈ f
id-r {f = f} = ≈-intro (resp f)

assoc : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → ∀ {l″ l≈″} {C : Setoid l″ l≈″} {l‴ l≈‴} {D : Setoid l‴ l≈‴}
  → {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
  → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
assoc {f = f} {g} {h} = ≈-intro (resp f ⊚ resp g ⊚ resp h)

module _ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′} where

  IsInjective : A ⇒ B → Set (l ⊔ l≈ ⊔ l≈′)
  IsInjective f = ∀ {a b} → eq B (arr f a) (arr f b) → eq A a b

  IsSurjective : A ⇒ B → Set (l ⊔ l′ ⊔ l≈′)
  IsSurjective f = ∀ b → ∃[ a ] (eq B b (arr f a))

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:
-- Andreas, 2016-03-28, Issue 1920
-- Improve error message when user puts where clause in hole.

infix 3 _∎

postulate
  A : Set
  begin : A
  _∎ : A → A

works : A
works = begin
  ∎
  where b = begin

test : A
test = {!begin
  ∎
  where b = begin
!}


text:
module functor where

open import level

record Functor {ℓ : Level} (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where
  constructor mkFunc
  field
    fmap : ∀{A B : Set ℓ} → (A → B) → F A → F B

open Functor public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL