text:
{-

This file contains:
  - The equivalence "James X ≃ Ω Σ X" for any connected pointed type X.
    (KANG Rongji, Feb. 2022)

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.LoopSuspEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed

open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.HITs.Pushout
open import Cubical.HITs.Pushout.Flattening
open import Cubical.HITs.Susp
open import Cubical.HITs.James.Base
  renaming (James to JamesContruction ; James∙ to JamesContruction∙)
open import Cubical.HITs.Truncation

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace

private
  variable
    ℓ : Level

module _
  ((X , x₀) : Pointed ℓ) where

  private
    James  =  JamesContruction  (X , x₀)
    James∙ =  JamesContruction∙ (X , x₀)

  Total : Type ℓ
  Total = Pushout {A = X × James} snd (λ (x , xs) → x ∷ xs)

  private
    flipSquare : (xs : James)(i j : I) → James
    flipSquare xs i j =
      hcomp (λ k → λ
        { (i = i0) → unit xs (j ∨ k)
        ; (i = i1) → unit (x₀ ∷ xs) j
        ; (j = i0) → unit xs (i ∨ k)
        ; (j = i1) → x₀ ∷ (unit xs i) })
      (unit (unit xs i) j)

    square1 : (x : X)(xs : James)(i j : I) → Total
    square1 x xs i j =
      hfill (λ j → λ
        { (i = i0) → push (x , xs) (~ j)
        ; (i = i1) → push (x₀ , x ∷ xs) (~ j) })
      (inS (inr (unit (x ∷ xs) i))) j

    square2 : (xs : James)(i j : I) → Total
    square2 xs i j =
      hcomp (λ k → λ
        { (i = i0) → push (x₀ , xs) (~ k)
        ; (i = i1) → square1 x₀ xs j k
        ; (j = i0) → push (x₀ , xs) (~ k)
        ; (j = i1) → push (x₀ , unit xs i) (~ k) })
      (inr (flipSquare xs i j))

    center : Total
    center = inl []

    pathL : (xs : James) → center ≡ inl xs
    pathL [] = refl
    pathL (x ∷ xs) = pathL xs ∙ (λ i → square1 x xs i i1)
    pathL (unit xs i) j =
      hcomp (λ k → λ
        { (i = i0) → pathL xs j
        ; (i = i1) → compPath-filler (pathL xs) (λ i → square1 x₀ xs i i1) k j
        ; (j = i0) → inl []
        ; (j = i1) → square2 xs i k })
      (pathL xs j)

  isContrTotal : isContr Total
  isContrTotal .fst = center
  isContrTotal .snd (inl xs) = pathL xs
  isContrTotal .snd (inr xs) = pathL xs ∙∙ push (x₀ , xs) ∙∙ (λ i → inr (unit xs (~ i)))
  isContrTotal .snd (push (x , xs) i) j =
    hcomp (λ k → λ
      { (i = i0) → compPath-filler' (pathL xs) (λ i → square1 x xs i i1) (~ j) (~ k)
      ; (i = i1) → doubleCompPath-filler (pathL (x ∷ xs)) (push (x₀ , x ∷ xs)) (λ i → inr (unit (x ∷ xs) (~ i))) k j
      ; (j = i0) → pathL (x ∷ xs) (~ k)
      ; (j = i1) → square1 x xs (~ k) (~ i) })
    (push (x₀ , x ∷ xs) (i ∧ j))

  module _
    (conn : isConnected 2 X) where

    private
      isEquivx₀∷ : isEquiv {A = James} (x₀ ∷_)
      isEquivx₀∷ = subst isEquiv (λ i xs → unit xs i) (idIsEquiv _)

      ∣isEquiv∣ : hLevelTrunc 2 X → Type ℓ
      ∣isEquiv∣ x = rec isSetHProp (λ x → isEquiv {A = James} (x ∷_) , isPropIsEquiv _) x .fst

    isEquiv∷ : (x : X) → isEquiv {A = James} (x ∷_)
    isEquiv∷ x = subst ∣isEquiv∣ (sym (conn .snd ∣ x₀ ∣) ∙ (conn .snd ∣ x ∣)) isEquivx₀∷

    Code : Susp X → Type ℓ
    Code north = James
    Code south = James
    Code (merid x i) = ua (_ , isEquiv∷ x) i

    private
      open FlatteningLemma (λ _ → tt) (λ _ → tt) (λ tt → James) (λ tt → James) (λ x → _ , isEquiv∷ x)

      Total≃ : Pushout Σf Σg ≃ Total
      Total≃ = pushoutEquiv _ _ _ _ (idEquiv _) (ΣUnit _) (ΣUnit _) refl refl

      PushoutSuspCode : (x : PushoutSusp X) → E x ≃ Code (PushoutSusp→Susp x)
      PushoutSuspCode (inl tt) = idEquiv _
      PushoutSuspCode (inr tt) = idEquiv _
      PushoutSuspCode (push x i) = idEquiv _

      ΣCode≃' : _ ≃ Σ _ Code
      ΣCode≃' = Σ-cong-equiv PushoutSusp≃Susp PushoutSuspCode

    ΣCode≃ : Total ≃ Σ _ Code
    ΣCode≃ = compEquiv (invEquiv Total≃) (compEquiv (invEquiv flatten) ΣCode≃')

    isContrΣCode : isContr (Σ _ Code)
    isContrΣCode = isOfHLevelRespectEquiv _ ΣCode≃ isContrTotal

    ΩΣ≃J : Ω (Susp∙ X) .fst ≃ James
    ΩΣ≃J = recognizeId Code [] isContrΣCode _

    ΩΣ≃∙J : Ω (Susp∙ X) ≃∙ James∙
    ΩΣ≃∙J = ΩΣ≃J , refl

    J≃ΩΣ : James ≃ Ω (Susp∙ X) .fst
    J≃ΩΣ = invEquiv ΩΣ≃J

    J≃∙ΩΣ : James∙ ≃∙ Ω (Susp∙ X)
    J≃∙ΩΣ = invEquiv∙ ΩΣ≃∙J

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ (P : Set) where

data ⊤ : Set where tt : ⊤

foo : ⊤ → Set
foo tt = ⊤

bar : {{_ : ⊤}} → ⊤
bar {{tt}} = tt

error : foo bar → ⊤
error tt = tt

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module SizedNat where

open import Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

-- subtraction is non size increasing
sub : {size : Size} -> Nat {size} -> Nat {∞} -> Nat {size}
sub zero n = zero
sub (suc m) zero = suc m
sub (suc m) (suc n) = sub m n

-- div' m n  computes  ceiling(m/(n+1))
div' : {size : Size} -> Nat {size} -> Nat -> Nat {size}
div' zero    n = zero
div' (suc m) n = suc (div' (sub m n) n)

-- one can use sized types as if they were not sized
-- sizes default to ∞

add : Nat -> Nat -> Nat
add (zero ) n = n
add (suc m) n = suc (add m n)

nisse : {i : Size} -> Nat {i} -> Nat {i}
nisse zero = zero
nisse (suc zero) = suc zero
nisse (suc (suc n)) = suc zero

{- Agda complains about duplicate binding

NatInfty = Nat {∞}

{-# BUILTIN NATURAL  NatInfty  #-}
{-# BUILTIN PLUS     add       #-}

-}

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module _ where

open import Common.Prelude
open import Common.Equality

primitive
  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x

force = primForce
forceLemma = primForceLemma

seq : ∀ {a b} {A : Set a} {B : Set b} → A → B → B
seq x y = force x λ _ → y

foo : (a b : Nat) → seq a b ≡ b
foo zero    _ = refl
foo (suc n) _ = refl

seqLit : (n : Nat) → seq "literal" n ≡ n
seqLit n = refl

seqType : (n : Nat) → seq Nat n ≡ n
seqType n = refl

seqPi : {A B : Set} {n : Nat} → seq (A → B) n ≡ n
seqPi = refl

seqLam : {n : Nat} → seq (λ (x : Nat) → x) n ≡ n
seqLam = refl

seqLemma : (a b : Nat) → seq a b ≡ b
seqLemma a b = forceLemma a _

evalLemma : (n : Nat) → seqLemma (suc n) n ≡ refl
evalLemma n = refl

infixr 0 _$!_
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $! x = force x f

-- Without seq, this would be exponential --

pow2 : Nat → Nat → Nat
pow2 zero    acc = acc
pow2 (suc n) acc = pow2 n $! acc + acc

lem : pow2 32 1 ≡ 4294967296
lem = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Semigroup.Construct.Right {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Semigroup

import Cubical.Algebra.Magma.Construct.Right Aˢ as RMagma
open RMagma public hiding (Right-isMagma; RightMagma)

private
  A = ⟨ Aˢ ⟩
  isSetA = Aˢ .snd

▸-assoc : Associative _▸_
▸-assoc _ _ _ = refl

Right-isSemigroup : IsSemigroup A _▸_
Right-isSemigroup = record
  { isMagma = RMagma.Right-isMagma
  ; assoc   = ▸-assoc
  }

RightSemigroup : Semigroup ℓ
RightSemigroup = record { isSemigroup = Right-isSemigroup }


text:
module _ where

abstract
  data Nat : Set where
    Zero : Nat
    Succ : Nat → Nat

  countDown : Nat → Nat
  countDown x with x
  ... | Zero   = Zero
  ... | Succ n = countDown n

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Group
open import lib.types.CommutingSquare
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.CommutingSquare where

-- A new type to keep the parameters.
record CommSquareᴳ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  (φ₀ : G₀ →ᴳ H₀) (φ₁ : G₁ →ᴳ H₁) (ξG : G₀ →ᴳ G₁) (ξH : H₀ →ᴳ H₁)
  : Type (lmax (lmax i₀ i₁) (lmax j₀ j₁)) where
  constructor comm-sqrᴳ
  field
    commutesᴳ : ∀ g₀ → GroupHom.f (ξH ∘ᴳ φ₀) g₀ == GroupHom.f (φ₁ ∘ᴳ ξG) g₀

infixr 0 _□$ᴳ_
_□$ᴳ_ = CommSquareᴳ.commutesᴳ

is-csᴳ-equiv : ∀ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  {φ₀ : G₀ →ᴳ H₀} {φ₁ : G₁ →ᴳ H₁} {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  → CommSquareᴳ φ₀ φ₁ ξG ξH → Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
is-csᴳ-equiv {ξG = ξG} {ξH} _ = is-equiv (GroupHom.f ξG) × is-equiv (GroupHom.f ξH)

CommSquareEquivᴳ : ∀ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  (φ₀ : G₀ →ᴳ H₀) (φ₁ : G₁ →ᴳ H₁) (ξG : G₀ →ᴳ G₁) (ξH : H₀ →ᴳ H₁)
  → Type (lmax (lmax i₀ i₁) (lmax j₀ j₁))
CommSquareEquivᴳ φ₀ φ₁ ξG ξH = Σ (CommSquareᴳ φ₀ φ₁ ξG ξH) is-csᴳ-equiv

abstract
  CommSquareᴳ-∘v : ∀ {i₀ i₁ i₂ j₀ j₁ j₂}
    {G₀ : Group i₀} {G₁ : Group i₁} {G₂ : Group i₂}
    {H₀ : Group j₀} {H₁ : Group j₁} {H₂ : Group j₂}
    {φ : G₀ →ᴳ H₀} {ψ : G₁ →ᴳ H₁} {χ : G₂ →ᴳ H₂}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    {μA : G₁ →ᴳ G₂} {μB : H₁ →ᴳ H₂}
    → CommSquareᴳ ψ χ μA μB
    → CommSquareᴳ φ ψ ξG ξH
    → CommSquareᴳ φ χ (μA ∘ᴳ ξG) (μB ∘ᴳ ξH)
  CommSquareᴳ-∘v {ξG = ξG} {μB = μB} (comm-sqrᴳ □₁₂) (comm-sqrᴳ □₀₁) =
    comm-sqrᴳ λ g₀ → ap (GroupHom.f μB) (□₀₁ g₀) ∙ □₁₂ (GroupHom.f ξG g₀)

CommSquareEquivᴳ-inverse-v : ∀ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  {φ₀ : G₀ →ᴳ H₀} {φ₁ : G₁ →ᴳ H₁} {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  → (cse : CommSquareEquivᴳ φ₀ φ₁ ξG ξH)
  → CommSquareEquivᴳ φ₁ φ₀ (GroupIso.g-hom (ξG , fst (snd cse))) (GroupIso.g-hom (ξH , snd (snd cse)))
CommSquareEquivᴳ-inverse-v (comm-sqrᴳ cs , ise)
  with CommSquareEquiv-inverse-v (comm-sqr cs , ise)
... | (comm-sqr cs' , ise') = cs'' , ise' where abstract cs'' = comm-sqrᴳ cs'

CommSquareᴳ-inverse-v : ∀ {i₀ i₁ j₀ j₁}
  {G₀ : Group i₀} {G₁ : Group i₁} {H₀ : Group j₀} {H₁ : Group j₁}
  {φ₀ : G₀ →ᴳ H₀} {φ₁ : G₁ →ᴳ H₁} {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
  → CommSquareᴳ φ₀ φ₁ ξG ξH
  → (ξG-ise : is-equiv (GroupHom.f ξG)) (ξH-ise : is-equiv (GroupHom.f ξH))
  → CommSquareᴳ φ₁ φ₀ (GroupIso.g-hom (ξG , ξG-ise)) (GroupIso.g-hom (ξH , ξH-ise))
CommSquareᴳ-inverse-v cs ξG-ise ξH-ise = fst (CommSquareEquivᴳ-inverse-v (cs , ξG-ise , ξH-ise))

-- basic facts nicely represented in commuting squares

inv-hom-natural-comm-sqr : ∀ {i j} (G : AbGroup i) (H : AbGroup j)
  (φ : AbGroup.grp G →ᴳ AbGroup.grp H)
  → CommSquareᴳ φ φ (inv-hom G) (inv-hom H)
inv-hom-natural-comm-sqr _ _ φ = comm-sqrᴳ λ g →  ! (GroupHom.pres-inv φ g)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- this is effectively a CM make file. it just includes all the files that
-- exist in the directory in the right order so that one can check that
-- everything compiles cleanly and has no unfilled holes

-- data structures
open import List
open import Nat
open import Prelude

-- basic stuff: core definitions, etc
open import core
open import checks
open import judgemental-erase
open import judgemental-inconsistency
open import moveerase
open import examples
open import structural

-- first wave theorems
open import sensibility
open import aasubsume-min
open import determinism

-- second wave theorems (checksums)
open import reachability
open import constructability


text:
module consoleExamples.passwordCheckSimple where

open import ConsoleLib
open import Data.Bool.Base
open import Data.Bool
open import Data.String renaming (_==_ to _==str_)
open import SizedIO.Base

main : ConsoleProg
main = run (GetLine >>= λ s →
            if  s ==str "passwd"
            then  WriteString "Success"
            else  WriteString "Error")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Universe where

open import Cubical.Data.Universe.Base public

open import Cubical.Data.Universe.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Categories.Bicategory using (Bicategory)

-- A Pseudofunctor is a homomorphism of Bicategories
-- Follow Bénabou's definition, which is basically that of a Functor

-- Note that what is in nLab is an "exploded" version of the simpler version below
module Categories.Pseudofunctor where

open import Level
open import Data.Product using (_,_)

import Categories.Category as Category
open Category.Category using (Obj; module Commutation)
open Category using (Category; _[_,_])
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Category.Product using (_⁂_)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_)
open import Categories.Category.Instance.One using (shift)
open NaturalIsomorphism using (F⇒G; F⇐G)

record Pseudofunctor {o ℓ e t o′ ℓ′ e′ t′  : Level} (C : Bicategory o ℓ e t) (D : Bicategory o′ ℓ′ e′ t′)
    : Set (o ⊔ ℓ ⊔ e ⊔ t ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ t′) where
  private
    module C = Bicategory C
    module D = Bicategory D

  field
    P₀ : C.Obj → D.Obj
    P₁ : {x y : C.Obj} → Functor (C.hom x y) (D.hom (P₀ x) (P₀ y))
    -- For maximal generality, shift the levels of One. P preserves id
    P-identity : {A : C.Obj} →  D.id {P₀ A} ∘F shift o′ ℓ′ e′ ≃ P₁ ∘F (C.id {A})
    -- P preserves composition
    P-homomorphism : {x y z : C.Obj} → D.⊚ ∘F (P₁ ⁂ P₁) ≃ P₁ ∘F C.⊚ {x} {y} {z}
    -- P preserves ≃

  module unitˡ {A} = NaturalTransformation (F⇒G (P-identity {A}))
  module unitʳ {A} = NaturalTransformation (F⇐G (P-identity {A}))
  module Hom {x} {y} {z} = NaturalTransformation (F⇒G (P-homomorphism {x} {y} {z}))

  -- For notational convenience, shorten some functor applications
  private
    F₀ = λ {x y} X → Functor.F₀ (P₁ {x} {y}) X

  field
    unitaryˡ : {x y : C.Obj} →
               let open Commutation (D.hom (P₀ x) (P₀ y)) in
               {f : Obj (C.hom x y)} →
               [ D.id₁ D.⊚₀ (F₀ f)            ⇒ F₀ f ]⟨
                 unitˡ.η _ D.⊚₁ D.id₂         ⇒⟨ F₀ C.id₁ D.⊚₀ F₀ f ⟩
                 Hom.η ( C.id₁ , f)           ⇒⟨ F₀ (C.id₁ C.⊚₀ f) ⟩
                 Functor.F₁ P₁ C.unitorˡ.from
               ≈ D.unitorˡ.from
               ⟩
    unitaryʳ : {x y : C.Obj} →
               let open Commutation (D.hom (P₀ x) (P₀ y)) in
               {f : Obj (C.hom x y)} →
               [ (F₀ f) D.⊚₀ D.id₁             ⇒ F₀ f ]⟨
                 D.id₂ D.⊚₁ unitˡ.η _          ⇒⟨ F₀ f D.⊚₀ F₀ C.id₁ ⟩
                 Hom.η ( f , C.id₁ )            ⇒⟨ F₀ (f C.⊚₀ C.id₁) ⟩
                 Functor.F₁ P₁ (C.unitorʳ.from)
               ≈ D.unitorʳ.from
               ⟩

    assoc : {x y z w : C.Obj} →
            let open Commutation (D.hom (P₀ x) (P₀ w)) in
            {f : Obj (C.hom x y)} {g : Obj (C.hom y z)} {h : Obj (C.hom z w)} →
            [ (F₀ h D.⊚₀ F₀ g) D.⊚₀ F₀ f     ⇒ F₀ (h C.⊚₀ (g C.⊚₀ f)) ]⟨
              Hom.η (h , g) D.⊚₁ D.id₂       ⇒⟨ F₀ (h C.⊚₀ g) D.⊚₀ F₀ f ⟩
              Hom.η (_ , f)                   ⇒⟨ F₀ ((h C.⊚₀ g) C.⊚₀ f) ⟩
              Functor.F₁ P₁ C.associator.from
            ≈ D.associator.from               ⇒⟨ F₀ h D.⊚₀ (F₀ g D.⊚₀ F₀ f) ⟩
              D.id₂ D.⊚₁ Hom.η (g , f)       ⇒⟨ F₀ h D.⊚₀ F₀ (g C.⊚₀ f) ⟩
              Hom.η (h , _)
            ⟩

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module Tactic.Reflection.Replace where
  open import Prelude

  open import Container.Traversable

  open import Tactic.Reflection
  open import Tactic.Reflection.Equality

  {-# TERMINATING #-}
  _r[_/_] : Term → Term → Term → Term
  p r[ r / l ] =
    ifYes p == l
      then r
      else case p of λ
        { (var x args) → var x $ args r₂[ r / l ]
        ; (con c args) → con c $ args r₂[ r / l ]
        ; (def f args) → def f $ args r₂[ r / l ]
        ; (lam v t) → lam v $ t r₁[ weaken 1 r / weaken 1 l ] -- lam v <$> t r₁[ weaken 1 r / weaken 1 l ]
        ; (pat-lam cs args) →
            let w = length args in
            pat-lam (replaceClause (weaken w l) (weaken w r) <$> cs) $ args r₂[ r / l ]
        ; (pi a b) → pi (a r₁[ r / l ]) (b r₁[ weaken 1 r / weaken 1 l ])
        ; (agda-sort s) → agda-sort $ replaceSort l r s
        ; (lit l) → lit l
        ; (meta x args) → meta x $ args r₂[ r / l ]
        ; unknown → unknown
        }
      where

      replaceClause : Term → Term → Clause → Clause
      replaceClause l r (clause pats x) = clause pats $ x r[ r / l ]
      replaceClause l r (absurd-clause pats) = absurd-clause pats

      replaceSort : Term → Term → Sort → Sort
      replaceSort l r (set t) = set $ t r[ r / l ]
      replaceSort l r (lit n) = lit n
      replaceSort l r unknown = unknown

      _r₁[_/_] : {T₀ : Set → Set} {{_ : Traversable T₀}} → T₀ Term → Term → Term → T₀ Term
      p r₁[ r / l ] = _r[ r / l ] <$> p

      _r₂[_/_] : {T₀ T₁ : Set → Set} {{_ : Traversable T₀}} {{_ : Traversable T₁}} →
                 T₁ (T₀ Term) → Term → Term → T₁ (T₀ Term)
      p r₂[ r / l ] = fmap _r[ r / l ] <$> p

  _R[_/_] : List (Arg Type) → Type → Type → List (Arg Type)
  Γ R[ L / R ] = go Γ (strengthen 1 L) (strengthen 1 R) where
    go : List (Arg Type) → Maybe Term → Maybe Term → List (Arg Type)
    go (γ ∷ Γ) (just L) (just R) = (caseF γ of _r[ L / R ]) ∷ go Γ (strengthen 1 L) (strengthen 1 R)
    go Γ _ _ = Γ

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Numeral.Natural.Relation.Order.Decidable where

open import Functional
open import Logic.IntroInstances
open import Logic.Propositional.Theorems
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Type.Properties.Decidable

instance
  [≡]-decider : Decider(2)(_≡_)(_≡?_)
  [≡]-decider {𝟎}  {𝟎}   = true [≡]-intro
  [≡]-decider {𝟎}  {𝐒 y} = false \()
  [≡]-decider {𝐒 x}{𝟎}   = false \()
  [≡]-decider {𝐒 x}{𝐒 y} = step{f = id} (true ∘ [≡]-with(𝐒)) (false ∘ contrapositiveᵣ (injective(𝐒))) ([≡]-decider {x}{y})

instance
  [≤]-decider : Decider(2)(_≤_)(_≤?_)
  [≤]-decider {𝟎} {𝟎} = true [≤]-minimum
  [≤]-decider {𝟎} {𝐒 y} = true [≤]-minimum
  [≤]-decider {𝐒 x} {𝟎} = false \()
  [≤]-decider {𝐒 x} {𝐒 y} = step{f = id} (true ∘ \p → [≤]-with-[𝐒] ⦃ p ⦄) (false ∘ contrapositiveᵣ [≤]-without-[𝐒]) ([≤]-decider {x}{y})

[<]-decider : Decider(2)(_<_)(_<?_)
[<]-decider {𝟎} {𝟎} = false (λ ())
[<]-decider {𝟎} {𝐒 y} = true (succ min)
[<]-decider {𝐒 x} {𝟎} = false (λ ())
[<]-decider {𝐒 x} {𝐒 y} = step{f = id} (true ∘ succ) (false ∘ contrapositiveᵣ [≤]-without-[𝐒]) ([<]-decider {x} {y})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.WellFounded
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Integers.Definition
open import Numbers.Integers.Integers
open import Numbers.Integers.Order
open import Groups.Groups
open import Groups.Definition
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Fields.Fields
open import Numbers.Primes.PrimeNumbers
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Numbers.Rationals.Definition
open import Semirings.Definition
open import Orders.Total.Definition
open import Orders.WellFounded.Induction
open import Setoids.Orders.Total.Definition

module Numbers.Rationals.Lemmas where

open import Semirings.Lemmas ℕSemiring

open PartiallyOrderedRing ℤPOrderedRing
open import Rings.Orders.Total.Lemmas ℤOrderedRing
open import Rings.Orders.Total.AbsoluteValue ℤOrderedRing
open SetoidTotalOrder (totalOrderToSetoidTotalOrder ℤOrder)

evenOrOdd : (a : ℕ) → (Sg ℕ (λ i → i *N 2 ≡ a)) || (Sg ℕ (λ i → succ (i *N 2) ≡ a))
evenOrOdd zero = inl (zero , refl)
evenOrOdd (succ zero) = inr (zero , refl)
evenOrOdd (succ (succ a)) with evenOrOdd a
evenOrOdd (succ (succ a)) | inl (a/2 , even) = inl (succ a/2 , applyEquality (λ i → succ (succ i)) even)
evenOrOdd (succ (succ a)) | inr (a/2-1 , odd) = inr (succ a/2-1 , applyEquality (λ i → succ (succ i)) odd)

parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
parity zero (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) = bad pr
  where
    bad : (1 ≡ succ (succ ((b +N 0) +N b))) → False
    bad ()
parity (succ a) (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | Semiring.commutative ℕSemiring (b +N 0) b = parity a b (succInjective (succInjective pr))

sqrt0 : (p : ℕ) → p *N p ≡ 0 → p ≡ 0
sqrt0 zero pr = refl
sqrt0 (succ p) ()

-- So as to give us something easy to induct down, introduce a silly extra variable
evil' : (k : ℕ) → ((a b : ℕ) → (0 <N a) → (pr : k ≡ a +N b) → a *N a ≡ (b *N b) *N 2 → False)
evil' = rec <NWellfounded (λ z → (x x₁ : ℕ) (pr' : 0 <N x) (x₂ : z ≡ x +N x₁) (x₃ : x *N x ≡ (x₁ *N x₁) *N 2) → False) go
  where
    go : (k : ℕ) (indHyp : (k' : ℕ) (k'<k : k' <N k) (r s : ℕ) (0<r : 0 <N r) (r+s : k' ≡ r +N s) (x₇ : r *N r ≡ (s *N s) *N 2) → False) (a b : ℕ) (0<a : 0 <N a) (a+b : k ≡ a +N b) (pr : a *N a ≡ (b *N b) *N 2) → False
    go k indHyp a b 0<a a+b pr = contr
      where
        open import Semirings.Solver ℕSemiring multiplicationNIsCommutative
        aEven : Sg ℕ (λ i → i *N 2 ≡ a)
        aEven with evenOrOdd a
        aEven | inl x = x
        aEven | inr (a/2-1 , odd) rewrite equalityCommutative odd =
          -- Derive a pretty mechanical contradiction using the automatic solver.
          -- This line looks hellish, but it was almost completely mechanical.
          exFalso (parity (a/2-1 +N (a/2-1 *N succ (a/2-1 *N 2))) (b *N b) (transitivity (
            -- truly mechanical bit starts here
            from (succ (plus (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero)))))) (plus (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero)))))) (times zero (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero))))))))))
            to succ (plus (times (const a/2-1) (succ (succ zero))) (times (times (const a/2-1) (succ (succ zero))) (succ (times (const a/2-1) (succ (succ zero))))))
            -- truly mechanical bit ends here
            by applyEquality (λ i → succ (a/2-1 +N i)) (
              -- Grinding out some manipulations
              transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (Semiring.commutative ℕSemiring (a/2-1 *N (a/2-1 +N a/2-1)) _) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (equalityCommutative (Semiring.+DistributesOver* ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 *N_) (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _))))))))))
            )) (transitivity pr (multiplicationNIsCommutative (b *N b) 2))))

        next : (underlying aEven *N 2) *N (underlying aEven *N 2) ≡ (b *N b) *N 2
        next with aEven
        ... | a/2 , even rewrite even = pr

        next2 : (underlying aEven *N 2) *N underlying aEven ≡ b *N b
        next2 = productCancelsRight 2 _ _ (le 1 refl) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (underlying aEven *N 2) _ _)) next)

        next3 : b *N b ≡ (underlying aEven *N underlying aEven) *N 2
        next3 = equalityCommutative (transitivity (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (underlying aEven) _ _)) (multiplicationNIsCommutative (underlying aEven) _)) next2)

        halveDecreased : underlying aEven <N a
        halveDecreased with aEven
        halveDecreased | zero , even rewrite equalityCommutative even = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
        halveDecreased | succ a/2 , even = le a/2 (transitivity (applyEquality succ (transitivity (Semiring.commutative ℕSemiring a/2 _) (applyEquality succ (transitivity (doubleIsAddTwo a/2) (multiplicationNIsCommutative 2 a/2))))) even)

        reduced : b +N underlying aEven <N k
        reduced with lessRespectsAddition b halveDecreased
        ... | bl rewrite a+b = identityOfIndiscernablesLeft _<N_ bl (Semiring.commutative ℕSemiring _ b)

        0<b : 0 <N b
        0<b with TotalOrder.totality ℕTotalOrder 0 b
        0<b | inl (inl 0<b) = 0<b
        0<b | inl (inr ())
        0<b | inr 0=b rewrite equalityCommutative 0=b = exFalso (TotalOrder.irreflexive ℕTotalOrder {0} (identityOfIndiscernablesRight _<N_ 0<a (sqrt0 a pr)))

        contr : False
        contr = indHyp (b +N underlying aEven) reduced b (underlying aEven) 0<b refl next3

evil : (a b : ℕ) → (0 <N a) → a *N a ≡ (b *N b) *N 2 → False
evil a b 0<a = evil' (a +N b) a b 0<a refl

absNonneg : (x : ℕ) → abs (nonneg x) ≡ nonneg x
absNonneg x with totality (nonneg 0) (nonneg x)
absNonneg x | inl (inl 0<x) = refl
absNonneg x | inr 0=x = refl

absNegsucc : (x : ℕ) → abs (negSucc x) ≡ nonneg (succ x)
absNegsucc x with totality (nonneg 0) (negSucc x)
absNegsucc x | inl (inr _) = refl

toNats : (numerator denominator : ℤ) → .(denominator ≡ nonneg 0 → False) → (abs numerator) *Z (abs numerator) ≡ ((abs denominator) *Z (abs denominator)) *Z nonneg 2 → Sg (ℕ && ℕ) (λ nats → ((_&&_.fst nats *N _&&_.fst nats) ≡ (_&&_.snd nats *N _&&_.snd nats) *N 2) && (_&&_.snd nats ≡ 0 → False))
toNats (nonneg num) (nonneg 0) pr _ = exFalso (pr refl)
toNats (nonneg num) (nonneg (succ denom)) _ pr = (num ,, (succ denom)) , (nonnegInjective (transitivity (transitivity (equalityCommutative (absNonneg (num *N num))) (absRespectsTimes (nonneg num) (nonneg num))) pr) ,, λ ())
toNats (nonneg num) (negSucc denom) _ pr = (num ,, succ denom) , (nonnegInjective (transitivity (transitivity (equalityCommutative (absNonneg (num *N num))) (absRespectsTimes (nonneg num) (nonneg num))) pr) ,, λ ())
toNats (negSucc num) (nonneg (succ denom)) _ pr = (succ num ,, succ denom) , (nonnegInjective pr ,, λ ())
toNats (negSucc num) (negSucc denom) _ pr = (succ num ,, succ denom) , (nonnegInjective pr ,, λ ())

sqrt2Irrational : (a : ℚ) → (a *Q a) =Q (injectionQ (nonneg 2)) → False
sqrt2Irrational (record { num = numerator ; denom = denominator ; denomNonzero = denom!=0 }) pr = bad
  where
    -- We have in hand `pr`, which is the following (almost by definition):
    pr' : (numerator *Z numerator) ≡ (denominator *Z denominator) *Z nonneg 2
    pr' = transitivity (equalityCommutative (transitivity (Ring.*Commutative ℤRing) (Ring.identIsIdent ℤRing))) pr

    -- Move into the naturals so that we can do nice divisibility things.
    lemma1 : abs ((denominator *Z denominator) *Z nonneg 2) ≡ (abs denominator *Z abs denominator) *Z nonneg 2
    lemma1 = transitivity (absRespectsTimes (denominator *Z denominator) (nonneg 2)) (applyEquality (_*Z nonneg 2) (absRespectsTimes denominator denominator))
    amenableToNaturals : (abs numerator) *Z (abs numerator) ≡ ((abs denominator) *Z (abs denominator)) *Z nonneg 2
    amenableToNaturals = transitivity (equalityCommutative (absRespectsTimes numerator numerator)) (transitivity (applyEquality abs pr') lemma1)

    naturalsStatement : Sg (ℕ && ℕ) (λ nats → ((_&&_.fst nats *N _&&_.fst nats) ≡ (_&&_.snd nats *N _&&_.snd nats) *N 2) && (_&&_.snd nats ≡ 0 → False))
    naturalsStatement = toNats numerator denominator denom!=0 amenableToNaturals

    bad : False
    bad with naturalsStatement
    bad | (num ,, 0) , (pr1 ,, pr2) = exFalso (pr2 refl)
    bad | (num ,, succ denom) , (pr1 ,, pr2) = evil num (succ denom) 0<num pr1
      where
        0<num : 0 <N num
        0<num with TotalOrder.totality ℕTotalOrder 0 num
        0<num | inl (inl 0<num) = 0<num
        0<num | inr 0=num rewrite equalityCommutative 0=num = exFalso (naughtE pr1)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Equivalences.PeifferGraphS2G where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.Structures.Subtype
open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction
open import Cubical.Algebra.Group.Semidirect

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.Action
open import Cubical.DStructures.Structures.XModule
open import Cubical.DStructures.Structures.ReflGraph
open import Cubical.DStructures.Structures.VertComp
open import Cubical.DStructures.Structures.PeifferGraph
open import Cubical.DStructures.Structures.Strict2Group
open import Cubical.DStructures.Equivalences.GroupSplitEpiAction
open import Cubical.DStructures.Equivalences.PreXModReflGraph

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' ℓ≅B' : Level

open Kernel
open GroupHom -- such .fun!
open GroupLemmas
open MorphismLemmas
open ActionLemmas

module _ (ℓ ℓ' : Level) where
  ℓℓ' = ℓ-max ℓ ℓ'

  𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group : 𝒮ᴰ-♭PIso (idfun (ReflGraph ℓ ℓℓ')) (𝒮ᴰ-ReflGraph\Peiffer ℓ ℓℓ') (𝒮ᴰ-Strict2Group ℓ ℓℓ')

  RelIso.fun (𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group 𝒢) isPeifferGraph = 𝒱
    where
      open ReflGraphNotation 𝒢
      open ReflGraphLemmas 𝒢
      open VertComp
      _⊙_ = λ (g f : ⟨ G₁ ⟩) → (g -₁ (𝒾s g)) +₁ f

      𝒱 : VertComp 𝒢
      vcomp 𝒱 g f _ = g ⊙ f
      σ-∘ 𝒱 g f c = r
        where
          isg = 𝒾s g
          abstract
            r = s ((g -₁ isg) +₁ f)
                  ≡⟨ (σ .isHom (g -₁ isg) f) ⟩
                s (g -₁ isg) +₀ s f
                  ≡⟨ cong (_+₀ s f) (σ-g--isg g) ⟩
                0₀ +₀ s f
                  ≡⟨ lId₀ (s f) ⟩
                s f ∎
      τ-∘ 𝒱 g f c = r
        where
          isg = 𝒾s g
          -isg = -₁ (𝒾s g)
          abstract
            r = t ((g -₁ isg) +₁ f)
                  ≡⟨ τ .isHom (g -₁ isg) f ⟩
                t (g -₁ isg) +₀ t f
                  ≡⟨ cong (_+₀ t f)
                          (τ .isHom g (-₁ isg))  ⟩
                (t g +₀ t -isg) +₀ t f
                  ≡⟨ cong ((t g +₀ t -isg) +₀_)
                          (sym c) ⟩
                (t g +₀ t -isg) +₀ s g
                  ≡⟨ cong (λ z → (t g +₀ z) +₀ s g)
                          (mapInv τ isg) ⟩
                (t g -₀ (t isg)) +₀ s g
                  ≡⟨ cong (λ z → (t g -₀ z) +₀ s g)
                          (τι-≡-fun (s g)) ⟩
                (t g -₀ (s g)) +₀ s g
                  ≡⟨ (sym (assoc₀ (t g) (-₀ s g) (s g))) ∙ (cong (t g +₀_) (lCancel₀ (s g))) ⟩
                t g +₀ 0₀
                  ≡⟨ rId₀ (t g) ⟩
                t g ∎
      isHom-∘ 𝒱 g f c-gf g' f' _ _ = r
        where
          isg = 𝒾s g
          -isg = -₁ (𝒾s g)
          isg' = 𝒾s g'
          -isg' = -₁ (𝒾s g')
          itf = 𝒾t f
          -itf = -₁ (𝒾t f)
          abstract
            r = (g +₁ g') ⊙ (f +₁ f')
                  ≡⟨ assoc₁ ((g +₁ g') -₁ 𝒾s (g +₁ g')) f f' ⟩
                (((g +₁ g') -₁ 𝒾s (g +₁ g')) +₁ f) +₁ f'
                  ≡⟨ cong (λ z → (z +₁ f) +₁ f')
                          (sym (assoc₁ g g' (-₁ (𝒾s (g +₁ g'))))) ⟩
                ((g +₁ (g' -₁ (𝒾s (g +₁ g')))) +₁ f) +₁ f'
                  ≡⟨ cong (_+₁ f')
                          (sym (assoc₁ g (g' -₁ (𝒾s (g +₁ g'))) f)) ⟩
                (g +₁ ((g' -₁ (𝒾s (g +₁ g'))) +₁ f)) +₁ f'
                  ≡⟨ cong (λ z → (g +₁ z) +₁ f')
                          ((g' -₁ (𝒾s (g +₁ g'))) +₁ f
                            ≡⟨ cong (λ z → (g' -₁ z) +₁ f)
                                    (ι∘σ .isHom g g') ⟩
                          (g' -₁ (isg +₁ isg')) +₁ f
                            ≡⟨ cong (λ z → (g' +₁ z) +₁ f)
                                    (invDistr G₁ isg isg') ⟩
                          (g' +₁ (-isg' +₁ -isg)) +₁ f
                            ≡⟨ assoc-c--r- G₁ g' -isg' -isg f ⟩
                          g' +₁ (-isg' +₁ (-isg +₁ f))
                            ≡⟨ cong (λ z → g' +₁ (-isg' +₁ ((-₁ (𝒾 z)) +₁ f)))
                                    c-gf ⟩
                          g' +₁ (-isg' +₁ (-itf +₁ f))
                            ≡⟨ isPeifferGraph4 𝒢 isPeifferGraph f g' ⟩
                          -itf +₁ (f +₁ (g' +₁ -isg'))
                            ≡⟨ cong (λ z → (-₁ (𝒾 z)) +₁ (f +₁ (g' +₁ -isg')))
                                    (sym c-gf) ⟩
                          -isg +₁ (f +₁ (g' +₁ -isg')) ∎) ⟩
                (g +₁ (-isg +₁ (f +₁ (g' +₁ -isg')))) +₁ f'
                  ≡⟨ cong (_+₁ f')
                          (assoc₁ g -isg (f +₁ (g' -₁ isg'))) ⟩
                ((g +₁ -isg) +₁ (f +₁ (g' +₁ -isg'))) +₁ f'
                  ≡⟨ cong (_+₁ f') (assoc₁ (g -₁ isg) f (g' -₁ isg')) ⟩
                (((g -₁ isg) +₁ f) +₁ (g' -₁ isg')) +₁ f'
                  ≡⟨ sym (assoc₁ ((g -₁ isg) +₁ f) (g' -₁ isg') f') ⟩
                ((g -₁ isg) +₁ f) +₁ ((g' -₁ isg') +₁ f')
                  ≡⟨ refl ⟩
                (g ⊙ f) +₁ (g' ⊙ f') ∎
      -- behold! use of symmetry is lurking around the corner
      -- (in stark contrast to composability proofs)
      assoc-∘ 𝒱 h g f _ _ _ _ = sym r
        where
          isg = 𝒾s g
          ish = 𝒾s h
          -ish = -₁ 𝒾s h
          abstract
            r = (h ⊙ g) ⊙ f
                  ≡⟨ cong (λ z → (((h -₁ ish) +₁ g) -₁ z) +₁ f)
                          (ι∘σ .isHom (h -₁ ish) g) ⟩
                (((h -₁ ish) +₁ g) -₁ (𝒾s (h -₁ ish) +₁ 𝒾s g)) +₁ f
                  ≡⟨ cong (λ z → (((h -₁ ish) +₁ g) -₁ (z +₁ 𝒾s g)) +₁ f)
                          (ι∘σ .isHom h (-₁ ish)) ⟩
                (((h -₁ ish) +₁ g) -₁ ((𝒾s h +₁ (𝒾s -ish)) +₁ 𝒾s g)) +₁ f
                  ≡⟨ cong (λ z → (((h -₁ ish) +₁ g) -₁ ((𝒾s h +₁ z) +₁ 𝒾s g)) +₁ f)
                          (ισ-ι (s h)) ⟩
                (((h -₁ ish) +₁ g) -₁ ((ish -₁ ish) +₁ isg)) +₁ f
                  ≡⟨ cong (λ z → (((h -₁ ish) +₁ g) -₁ z) +₁ f)
                          (rCancel-lId G₁ ish isg) ⟩
                (((h -₁ ish) +₁ g) -₁ isg) +₁ f
                  ≡⟨ (cong (_+₁ f) (sym (assoc₁ (h -₁ ish) g (-₁ isg)))) ∙ (sym (assoc₁ (h -₁ ish) (g -₁ isg) f)) ⟩
                h ⊙ (g ⊙ f) ∎
      lid-∘ 𝒱 f _ = r
        where
          itf = 𝒾t f
          abstract
            r = itf ⊙ f
                  ≡⟨ cong (λ z → (itf -₁ (𝒾 z)) +₁ f) (σι-≡-fun (t f)) ⟩
                (itf -₁ itf) +₁ f
                  ≡⟨ rCancel-lId G₁ itf f ⟩
                f ∎
      rid-∘ 𝒱 g _ = r
        where
          isg = 𝒾s g
          -isg = -₁ (𝒾s g)
          abstract
            r = g ⊙ isg
                  ≡⟨ sym (assoc₁ g -isg isg) ⟩
                g +₁ (-isg +₁ isg)
                  ≡⟨ lCancel-rId G₁ g isg ⟩
                g ∎

  RelIso.inv (𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group 𝒢) 𝒞 = isPf
    where
      open ReflGraphNotation 𝒢
      open VertComp 𝒞

      abstract
        isPf : isPeifferGraph 𝒢
        isPf f g = ((isg +₁ (f -₁ itf)) +₁ (-isg +₁ g)) +₁ itf
                  ≡⟨ cong (_+₁ itf)
                          (sym (assoc₁ isg (f -₁ itf) (-isg +₁ g))) ⟩
                (isg +₁ ((f -₁ itf) +₁ (-isg +₁ g))) +₁ itf
                  ≡⟨ cong (λ z → (isg +₁ z) +₁ itf)
                          (sym (assoc₁ f -itf (-isg +₁ g))) ⟩
                (isg +₁ (f +₁ (-itf +₁ (-isg +₁ g)))) +₁ itf
                  ≡⟨ cong (λ z → (isg +₁ (f +₁ z)) +₁ itf)
                          (assoc₁ -itf -isg g) ⟩
                (isg +₁ (f +₁ ((-itf -₁ isg) +₁ g))) +₁ itf
                  ≡⟨ cong (λ z → (isg +₁ z) +₁ itf)
                          (IC5 𝒞 g f) ⟩
                (isg +₁ ((-isg +₁ g) +₁ (f -₁ itf))) +₁ itf
                  ≡⟨ cong (_+₁ itf)
                          (assoc₁ isg (-isg +₁ g) (f -₁ itf)) ⟩
                ((isg +₁ (-isg +₁ g)) +₁ (f -₁ itf)) +₁ itf
                  ≡⟨ cong (λ z → (z +₁ (f -₁ itf)) +₁ itf)
                          (assoc₁ isg -isg g ∙ rCancel-lId G₁ isg g) ⟩
                (g +₁ (f -₁ itf)) +₁ itf
                  ≡⟨ sym (assoc₁ g (f -₁ itf) itf) ⟩
                g +₁ ((f -₁ itf) +₁ itf)
                  ≡⟨ cong (g +₁_) ((sym (assoc₁ _ _ _)) ∙ (lCancel-rId G₁ f itf)) ⟩
                g +₁ f ∎
          where
            isg = 𝒾s g
            -isg = -₁ (𝒾s g)
            itf = 𝒾t f
            -itf = -it f

  RelIso.leftInv (𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group _) _ = tt
  RelIso.rightInv (𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group _) _ = tt

  Iso-PeifferGraph-Strict2Group : Iso (PeifferGraph ℓ ℓℓ') (Strict2Group ℓ ℓℓ')
  Iso-PeifferGraph-Strict2Group = 𝒮ᴰ-♭PIso-Over→TotalIso idIso (𝒮ᴰ-ReflGraph\Peiffer ℓ ℓℓ') (𝒮ᴰ-Strict2Group ℓ ℓℓ') 𝒮ᴰ-♭PIso-PeifferGraph-Strict2Group

  open import Cubical.DStructures.Equivalences.XModPeifferGraph
  Iso-XModule-Strict2Group : Iso (XModule ℓ ℓℓ') (Strict2Group ℓ ℓℓ')
  Iso-XModule-Strict2Group = compIso (Iso-XModule-PeifferGraph ℓ ℓℓ') Iso-PeifferGraph-Strict2Group

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------------
-- Arithmetic properties (added for the Collatz function example)
------------------------------------------------------------------------------

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

module FOTC.Program.Collatz.Data.Nat.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
  using ( x≤x
        ; 2*SSx≥2
        )
open import FOTC.Data.Nat.PropertiesATP
  using ( *-N
        ; *-rightZero
        ; *-rightIdentity
        ; x∸x≡0
        ; +-rightIdentity
        ; +-comm
        ; +-N
        ; xy≡0→x≡0∨y≡0
        ; Sx≢x
        ; xy≡1→x≡1
        ; 0∸x
        ; S∸S
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Program.Collatz.Data.Nat

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

^-N : ∀ {m n} → N m → N n → N (m ^ n)
^-N {m} Nm nzero = prf
  where postulate prf : N (m ^ zero)
        {-# ATP prove prf #-}
^-N {m} Nm (nsucc {n} Nn) = prf (^-N Nm Nn)
  where postulate prf : N (m ^ n) → N (m ^ succ₁ n)
        {-# ATP prove prf *-N #-}

div-2x-2≡x : ∀ {n} → N n → div (2' * n) 2' ≡ n
div-2x-2≡x nzero = prf
  where postulate prf : div (2' * zero) 2' ≡ zero
        {-# ATP prove prf *-rightZero #-}
div-2x-2≡x (nsucc nzero) = prf
  where postulate prf : div (2' * (succ₁ zero)) 2' ≡ succ₁ zero
        {-# ATP prove prf *-rightIdentity x≤x x∸x≡0 #-}
div-2x-2≡x (nsucc (nsucc {n} Nn)) = prf (div-2x-2≡x (nsucc Nn))
  where postulate prf : div (2' * succ₁ n) 2' ≡ succ₁ n →
                        div (2' * (succ₁ (succ₁ n))) 2' ≡ succ₁ (succ₁ n)
        {-# ATP prove prf 2*SSx≥2 +-rightIdentity +-comm +-N #-}

postulate div-2^[x+1]-2≡2^x : ∀ {n} → N n → div (2' ^ succ₁ n) 2' ≡ 2' ^ n
{-# ATP prove div-2^[x+1]-2≡2^x ^-N div-2x-2≡x #-}

+∸2 : ∀ {n} → N n → n ≢ zero → n ≢ 1' → n ≡ succ₁ (succ₁ (n ∸ 2'))
+∸2 nzero                  n≢0 n≢1 = ⊥-elim (n≢0 refl)
+∸2 (nsucc nzero)          n≢0 n≢1 = ⊥-elim (n≢1 refl)
+∸2 (nsucc (nsucc {n} Nn)) n≢0 n≢1 = prf
  where
  -- TODO (06 December 2012). We do not use the ATPs because we do not
  -- how to erase a term.
  --
  -- See the interactive proof.
  postulate prf : succ₁ (succ₁ n) ≡ succ₁ (succ₁ (succ₁ (succ₁ n) ∸ 2'))
  -- {-# ATP prove prf S∸S #-}

2^x≢0 : ∀ {n} → N n → 2' ^ n ≢ zero
2^x≢0 nzero          h = ⊥-elim (0≢S (trans (sym h) (^-0 2')))
2^x≢0 (nsucc {n} Nn) h = prf (2^x≢0 Nn)
  where postulate prf : 2' ^ n ≢ zero → ⊥
        {-# ATP prove prf xy≡0→x≡0∨y≡0 ^-N #-}

postulate 2^[x+1]≢1 : ∀ {n} → N n → 2' ^ succ₁ n ≢ 1'
{-# ATP prove 2^[x+1]≢1 Sx≢x xy≡1→x≡1 ^-N #-}

Sx-Even→x-Odd : ∀ {n} → N n → Even (succ₁ n) → Odd n
Sx-Even→x-Odd nzero  h = ⊥-elim prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
Sx-Even→x-Odd (nsucc {n} Nn) h = prf
  where postulate prf : odd (succ₁ n) ≡ true
        {-# ATP prove prf #-}

Sx-Odd→x-Even : ∀ {n} → N n → Odd (succ₁ n) → Even n
Sx-Odd→x-Even nzero          _ = even-0
Sx-Odd→x-Even (nsucc {n} Nn) h = trans (sym (odd-S (succ₁ n))) h

postulate 2-Even : Even 2'
{-# ATP prove 2-Even #-}

∸-Even : ∀ {m n} → N m → N n → Even m → Even n → Even (m ∸ n)
∸-Odd : ∀ {m n} → N m → N n → Odd m → Odd n → Even (m ∸ n)

∸-Even {m} Nm nzero                      h₁ _  = subst Even (sym (∸-x0 m)) h₁
∸-Even     nzero          (nsucc {n} Nn) h₁ _  = subst Even (sym (0∸x (nsucc Nn))) h₁
∸-Even     (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ = prf
  where postulate prf : Even (succ₁ m ∸ succ₁ n)
        {-# ATP prove prf ∸-Odd Sx-Even→x-Odd S∸S #-}

∸-Odd nzero          Nn             h₁ _  = ⊥-elim (t≢f (trans (sym h₁) odd-0))
∸-Odd (nsucc Nm)     nzero          _  h₂ = ⊥-elim (t≢f (trans (sym h₂) odd-0))
∸-Odd (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ = prf
  where postulate prf : Even (succ₁ m ∸ succ₁ n)
        {-# ATP prove prf ∸-Even Sx-Odd→x-Even S∸S #-}

x-Even→SSx-Even : ∀ {n} → N n → Even n → Even (succ₁ (succ₁ n))
x-Even→SSx-Even nzero h = prf
  where postulate prf : Even (succ₁ (succ₁ zero))
        {-# ATP prove prf #-}

x-Even→SSx-Even (nsucc {n} Nn) h = prf
  where postulate prf : Even (succ₁ (succ₁ (succ₁ n)))
        {-# ATP prove prf #-}

x+x-Even : ∀ {n} → N n → Even (n + n)
x+x-Even nzero  = prf
  where postulate prf : even (zero + zero) ≡ true
        {-# ATP prove prf #-}
x+x-Even (nsucc {n} Nn) = prf (x+x-Even Nn)
  where postulate prf : Even (n + n) → Even (succ₁ n + succ₁ n)
        {-# ATP prove prf x-Even→SSx-Even +-N +-comm #-}

2x-Even : ∀ {n} → N n → Even (2' * n)
2x-Even nzero = prf
  where postulate prf : Even (2' * zero)
        {-# ATP prove prf #-}
2x-Even (nsucc {n} Nn) = prf
  where
  postulate prf : Even (2' * succ₁ n)
  {-# ATP prove prf x-Even→SSx-Even x+x-Even +-N +-comm +-rightIdentity #-}

postulate 2^[x+1]-Even : ∀ {n} → N n → Even (2' ^ succ₁ n)
{-# ATP prove 2^[x+1]-Even ^-N 2x-Even #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module OlderBasicILP.Direct.Translation where

open import Common.Context public

-- import OlderBasicILP.Direct.Hilbert.Sequential as HS
import OlderBasicILP.Direct.Hilbert.Nested as HN
import OlderBasicILP.Direct.Gentzen as G

-- open HS using () renaming (_⊢×_ to HS⟨_⊢×_⟩ ; _⊢_ to HS⟨_⊢_⟩) public
open HN using () renaming (_⊢_ to HN⟨_⊢_⟩ ; _⊢⋆_ to HN⟨_⊢⋆_⟩) public
open G using  () renaming (_⊢_ to G⟨_⊢_⟩ ; _⊢⋆_ to G⟨_⊢⋆_⟩) public

-- Translation from sequential Hilbert-style to nested.

-- hs→hn : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → HN⟨ Γ ⊢ A ⟩
-- hs→hn = ?

-- Translation from nested Hilbert-style to sequential.

-- hn→hs : ∀ {A Γ} → HN⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
-- hn→hs = ?

-- Deduction theorem for sequential Hilbert-style.

-- hs-lam : ∀ {A B Γ} → HS⟨ Γ , A ⊢ B ⟩ → HS⟨ Γ ⊢ A ▻ B ⟩
-- hs-lam = hn→hs ∘ HN.lam ∘ hs→hn

-- Translation from Hilbert-style to Gentzen-style.

mutual
  hn→gᵇᵒˣ : HN.Box → G.Box
  hn→gᵇᵒˣ HN.[ t ] = {!G.[ hn→g t ]!}

  hn→gᵀ : HN.Ty → G.Ty
  hn→gᵀ (HN.α P)   = G.α P
  hn→gᵀ (A HN.▻ B) = hn→gᵀ A G.▻ hn→gᵀ B
  hn→gᵀ (T HN.⦂ A) = hn→gᵇᵒˣ T G.⦂ hn→gᵀ A
  hn→gᵀ (A HN.∧ B) = hn→gᵀ A G.∧ hn→gᵀ B
  hn→gᵀ HN.⊤      = G.⊤

  hn→gᵀ⋆ : Cx HN.Ty → Cx G.Ty
  hn→gᵀ⋆ ∅       = ∅
  hn→gᵀ⋆ (Γ , A) = hn→gᵀ⋆ Γ , hn→gᵀ A

  hn→gⁱ : ∀ {A Γ} → A ∈ Γ → hn→gᵀ A ∈ hn→gᵀ⋆ Γ
  hn→gⁱ top     = top
  hn→gⁱ (pop i) = pop (hn→gⁱ i)

  hn→g : ∀ {A Γ} → HN⟨ Γ ⊢ A ⟩ → G⟨ hn→gᵀ⋆ Γ ⊢ hn→gᵀ A ⟩
  hn→g (HN.var i)   = G.var (hn→gⁱ i)
  hn→g (HN.app t u) = G.app (hn→g t) (hn→g u)
  hn→g HN.ci        = G.ci
  hn→g HN.ck        = G.ck
  hn→g HN.cs        = G.cs
  hn→g (HN.box t)   = {!G.box (hn→g t)!}
  hn→g HN.cdist     = {!G.cdist!}
  hn→g HN.cup       = {!G.cup!}
  hn→g HN.cdown     = G.cdown
  hn→g HN.cpair     = G.cpair
  hn→g HN.cfst      = G.cfst
  hn→g HN.csnd      = G.csnd
  hn→g HN.unit      = G.unit

-- hs→g : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
-- hs→g = hn→g ∘ hs→hn

-- Translation from Gentzen-style to Hilbert-style.

mutual
  g→hnᵇᵒˣ : G.Box → HN.Box
  g→hnᵇᵒˣ G.[ t ] = {!HN.[ g→hn t ]!}

  g→hnᵀ : G.Ty → HN.Ty
  g→hnᵀ (G.α P)   = HN.α P
  g→hnᵀ (A G.▻ B) = g→hnᵀ A HN.▻ g→hnᵀ B
  g→hnᵀ (T G.⦂ A) = g→hnᵇᵒˣ T HN.⦂ g→hnᵀ A
  g→hnᵀ (A G.∧ B) = g→hnᵀ A HN.∧ g→hnᵀ B
  g→hnᵀ G.⊤      = HN.⊤

  g→hnᵀ⋆ : Cx G.Ty → Cx HN.Ty
  g→hnᵀ⋆ ∅       = ∅
  g→hnᵀ⋆ (Γ , A) = g→hnᵀ⋆ Γ , g→hnᵀ A

  g→hnⁱ : ∀ {A Γ} → A ∈ Γ → g→hnᵀ A ∈ g→hnᵀ⋆ Γ
  g→hnⁱ top     = top
  g→hnⁱ (pop i) = pop (g→hnⁱ i)

  g→hn : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HN⟨ g→hnᵀ⋆ Γ ⊢ g→hnᵀ A ⟩
  g→hn (G.var i)         = HN.var (g→hnⁱ i)
  g→hn (G.lam t)         = HN.lam (g→hn t)
  g→hn (G.app t u)       = HN.app (g→hn t) (g→hn u)
--  g→hn (G.multibox ts u) = {!HN.multibox (g→hn⋆ ts) (g→hn u)!}
  g→hn (G.down t)        = HN.down (g→hn t)
  g→hn (G.pair t u)      = HN.pair (g→hn t) (g→hn u)
  g→hn (G.fst t)         = HN.fst (g→hn t)
  g→hn (G.snd t)         = HN.snd (g→hn t)
  g→hn G.unit            = HN.unit

  g→hn⋆ : ∀ {Ξ Γ} → G⟨ Γ ⊢⋆ Ξ ⟩ → HN⟨ g→hnᵀ⋆ Γ ⊢⋆ g→hnᵀ⋆ Ξ ⟩
  g→hn⋆ {∅}     ∙        = ∙
  g→hn⋆ {Ξ , A} (ts , t) = g→hn⋆ ts , g→hn t

-- g→hs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
-- g→hs = hn→hs ∘ g→hn

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Oscar.Class.Semifunctor where

open import Oscar.Class.Semigroup
open import Oscar.Class.Extensionality
open import Oscar.Class.Preservativity
open import Oscar.Function
open import Oscar.Level
open import Oscar.Relation

record Semifunctor
  {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁}
    (_◅₁_ : ∀ {m n} → m ►₁ n → ∀ {l} → m ⟨ l ►₁_ ⟩→ n)
  {ℓ₁}
    (_≋₁_ : ∀ {m n} → m ►₁ n → m ►₁ n → Set ℓ₁)
  {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} {_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂}
    (_◅₂_ : ∀ {m n} → m ►₂ n → ∀ {l} → m ⟨ l ►₂_ ⟩→ n)
  {ℓ₂}
    (_≋₂_ : ∀ {m n} → m ►₂ n → m ►₂ n → Set ℓ₂)
  (μ : 𝔄₁ → 𝔄₂)
  (□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n)
  : Set (𝔞₁ ⊔ 𝔰₁ ⊔ ℓ₁ ⊔ 𝔞₂ ⊔ 𝔰₂ ⊔ ℓ₂) where
  field
    ⦃ ′semigroup₁ ⦄ : Semigroup _◅₁_ _≋₁_
    ⦃ ′semigroup₂ ⦄ : Semigroup _◅₂_ _≋₂_
    ⦃ ′extensionality ⦄ : ∀ {m n} → Extensionality (_≋₁_ {m} {n}) (λ ⋆ → _≋₂_ {μ m} {μ n} ⋆) □ □
    ⦃ ′preservativity ⦄ : ∀ {l m n} → Preservativity (λ ⋆ → _◅₁_ {m = m} {n = n} ⋆ {l = l}) (λ ⋆ → _◅₂_ ⋆) _≋₂_ □ □ □

instance

  Semifunctor⋆ : ∀
    {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁}
      {_◅₁_ : ∀ {m n} → m ►₁ n → ∀ {l} → m ⟨ l ►₁_ ⟩→ n}
    {ℓ₁}
      {_≋₁_ : ∀ {m n} → m ►₁ n → m ►₁ n → Set ℓ₁}
    {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} {_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂}
      {_◅₂_ : ∀ {m n} → m ►₂ n → ∀ {l} → m ⟨ l ►₂_ ⟩→ n}
    {ℓ₂}
      {_≋₂_ : ∀ {m n} → m ►₂ n → m ►₂ n → Set ℓ₂}
    {μ : 𝔄₁ → 𝔄₂}
    {□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n}
    ⦃ _ : Semigroup _◅₁_ _≋₁_ ⦄
    ⦃ _ : Semigroup _◅₂_ _≋₂_ ⦄
    ⦃ _ : ∀ {m n} → Extensionality (_≋₁_ {m} {n}) (λ ⋆ → _≋₂_ {μ m} {μ n} ⋆) □ □ ⦄
    ⦃ _ : ∀ {l m n} → Preservativity (λ ⋆ → _◅₁_ {m = m} {n = n} ⋆ {l = l}) (λ ⋆ → _◅₂_ ⋆) _≋₂_ □ □ □ ⦄
    → Semifunctor _◅₁_ _≋₁_ _◅₂_ _≋₂_ μ □
  Semifunctor.′semigroup₁ Semifunctor⋆ = it
  Semifunctor.′semigroup₂ Semifunctor⋆ = it
  Semifunctor.′extensionality Semifunctor⋆ = it
  Semifunctor.′preservativity Semifunctor⋆ = it

-- record Semifunctor'
--   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
--     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
--   {ℓ₁}
--     (_≋₁_ : ∀ {m n} → m ► n → m ► n → Set ℓ₁)
--   {𝔱} {▸ : 𝔄 → Set 𝔱}
--     (_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n)
--   {ℓ₂}
--     (_≋₂_ : ∀ {n} → ▸ n → ▸ n → Set ℓ₂)
--   (□ : ∀ {m n} → m ► n → m ► n)
--   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ₁ ⊔ 𝔱 ⊔ ℓ₂) where
--   field
--     ⦃ ′semigroup₁ ⦄ : Semigroup _◅_ (λ ⋆ → _◅_ ⋆) _≋₁_
--     ⦃ ′semigroup₂ ⦄ : Semigroup _◅_ _◃_ _≋₂_
--     ⦃ ′extensionality ⦄ : ∀ {m} {t : ▸ m} {n} → Extensionality (_≋₁_ {m} {n}) (λ ⋆ → _≋₂_ {n} ⋆) (_◃ t) (_◃ t)
--     ⦃ ′preservativity ⦄ : Preservativity _►₁_ _◃₁_ _►₂_ _◃₂_ _≋₂_ ◽ □

-- record Semifunctor
--   {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁}
--     (_◅₁_ : ∀ {m n} → m ►₁ n → ∀ {l} → m ⟨ l ►₁_ ⟩→ n)
--   {𝔱₁} {▸₁ : 𝔄₁ → Set 𝔱₁}
--     (_◃₁_ : ∀ {m n} → m ►₁ n → m ⟨ ▸₁ ⟩→ n)
--   {ℓ₁}
--     (_≋₁_ : ∀ {n} → ▸₁ n → ▸₁ n → Set ℓ₁)
--   {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} {_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂}
--     (_◅₂_ : ∀ {m n} → m ►₂ n → ∀ {l} → m ⟨ l ►₂_ ⟩→ n)
--   {𝔱₂} {▸₂ : 𝔄₂ → Set 𝔱₂}
--     (_◃₂_ : ∀ {m n} → m ►₂ n → m ⟨ ▸₂ ⟩→ n)
--   {ℓ₂}
--     (_≋₂_ : ∀ {n} → ▸₂ n → ▸₂ n → Set ℓ₂)
--   (μ : 𝔄₁ → 𝔄₂)
--   (◽ : ∀ {n} → ▸₁ n → ▸₂ (μ n))
--   (□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n)
--   : Set (𝔞₁ ⊔ 𝔰₁ ⊔ 𝔱₁ ⊔ ℓ₁ ⊔ 𝔞₂ ⊔ 𝔰₂ ⊔ 𝔱₂ ⊔ ℓ₂) where
--   field
--     ⦃ ′semigroup₁ ⦄ : Semigroup _◅₁_ _◃₁_ _≋₁_
--     ⦃ ′semigroup₂ ⦄ : Semigroup _◅₂_ _◃₂_ _≋₂_
--     ⦃ ′extensionality ⦄ : ∀ {n} → Extensionality (_≋₁_ {n}) (λ ⋆ → _≋₂_ {μ n} ⋆) ◽ ◽
--     ⦃ ′preservativity ⦄ : Preservativity _►₁_ _◃₁_ _►₂_ _◃₂_ _≋₂_ ◽ □

-- open Semifunctor ⦃ … ⦄ public hiding (′semigroup₁; ′semigroup₂; ′extensionality; ′preservativity)

-- instance

--   Semifunctor⋆ : ∀
--     {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁}
--       {_◅₁_ : ∀ {m n} → m ►₁ n → ∀ {l} → m ⟨ l ►₁_ ⟩→ n}
--     {𝔱₁} {▸₁ : 𝔄₁ → Set 𝔱₁}
--       {_◃₁_ : ∀ {m n} → m ►₁ n → m ⟨ ▸₁ ⟩→ n}
--     {ℓ₁}
--       {_≋₁_ : ∀ {n} → ▸₁ n → ▸₁ n → Set ℓ₁}
--     {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} {_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂}
--       {_◅₂_ : ∀ {m n} → m ►₂ n → ∀ {l} → m ⟨ l ►₂_ ⟩→ n}
--     {𝔱₂} {▸₂ : 𝔄₂ → Set 𝔱₂}
--       {_◃₂_ : ∀ {m n} → m ►₂ n → m ⟨ ▸₂ ⟩→ n}
--     {ℓ₂}
--       {_≋₂_ : ∀ {n} → ▸₂ n → ▸₂ n → Set ℓ₂}
--     {μ : 𝔄₁ → 𝔄₂}
--     {◽ : ∀ {n} → ▸₁ n → ▸₂ (μ n)}
--     {□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n}
--     ⦃ _ : Semigroup _◅₁_ _◃₁_ _≋₁_ ⦄
--     ⦃ _ : Semigroup _◅₂_ _◃₂_ _≋₂_ ⦄
--     ⦃ _ : ∀ {n} → Extensionality (_≋₁_ {n}) (λ ⋆ → _≋₂_ {μ n} ⋆) ◽ ◽ ⦄
--     ⦃ _ : Preservativity _►₁_ _◃₁_ _►₂_ _◃₂_ _≋₂_ ◽ □ ⦄
--     → Semifunctor _◅₁_ _◃₁_ _≋₁_ _◅₂_ _◃₂_ _≋₂_ μ ◽ □
--   Semifunctor.′semigroup₁ Semifunctor⋆ = it
--   Semifunctor.′semigroup₂ Semifunctor⋆ = it
--   Semifunctor.′extensionality Semifunctor⋆ = it
--   Semifunctor.′preservativity Semifunctor⋆ = it


text:
module nform where

open import Data.PropFormula (3) public
open import Data.PropFormula.NormalForms 3 public
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

p : PropFormula
p = Var (# 0)

q : PropFormula
q = Var (# 1)

r : PropFormula
r = Var (# 2)

φ : PropFormula
φ = ¬ ((p ∧ (p ⊃ q)) ⊃ q) -- (p ∧ q) ∨ (¬ r)

cnfφ : PropFormula
cnfφ = ¬ q ∧ (p ∧ (¬ p ∨ q))

postulate
 p1 : ∅ ⊢ φ

p2 : ∅ ⊢ cnfφ
p2 = cnf-lem p1 -- thm-cnf p1

{-
p3 : cnf φ ≡ cnfφ
p3 = refl

ψ : PropFormula
ψ = (¬ r) ∨ (p ∧ q)

cnfψ : PropFormula
cnfψ = (¬ r ∨ p) ∧ (¬ r ∨ q)

p5 : cnf ψ ≡ cnfψ
p5 = refl
-}

to5   = (¬ p) ∨ ((¬ q) ∨ r)
from5 = (¬ p) ∨ (r ∨ ((¬ q) ∧ p))

test : ⌊ eq (cnf from5) to5 ⌋ ≡ false
test = refl

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category hiding (module Heterogeneous)
open import Categories.Congruence

module Categories.Arrow {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Relation.Binary using (Rel)
open import Data.Product using (_×_; _,_; map; zip)

open Category C
open Category.Equiv C

record ArrowObj : Set (o ⊔ ℓ) where
  constructor arrobj
  field
    {A} : Obj
    {B} : Obj
    arr : A ⇒ B

record Arrow⇒ (X Y : ArrowObj) : Set (ℓ ⊔ e) where
  constructor arrarr
  module X = ArrowObj X
  module Y = ArrowObj Y
  field
    {f} : X.A ⇒ Y.A
    {g} : X.B ⇒ Y.B
    .square : CommutativeSquare X.arr f g Y.arr

arrow : Category _ _ _
arrow = record
  { Obj = Obj′
  ; _⇒_ = _⇒′_
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = id′
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assoc′ {f = f} {g} {h}
  ; identityˡ = identityˡ , identityˡ
  ; identityʳ = identityʳ , identityʳ
  ; equiv = record
    { refl = refl , refl
    ; sym = map sym sym
    ; trans = zip trans trans
    }
  ; ∘-resp-≡ = zip ∘-resp-≡ ∘-resp-≡
  }
  where
  Obj′ = ArrowObj

  _⇒′_ : Rel Obj′ _
  _⇒′_ = Arrow⇒

  infixr 9 _∘′_
  infix  4 _≡′_

  _≡′_ : ∀ {A B} → (f g : A ⇒′ B) → Set _
  (arrarr {f} {h} _) ≡′ (arrarr {i} {g} _) = f ≡ i × h ≡ g

  _∘′_ : ∀ {A B C} → (B ⇒′ C) → (A ⇒′ B) → (A ⇒′ C)
  _∘′_ {arrobj x} {arrobj y} {arrobj z} (arrarr {f} {h} pf₁) (arrarr {i} {g} pf₂) = arrarr pf
    where
    .pf : (h ∘ g) ∘ x ≡ z ∘ (f ∘ i)
    pf = begin
           (h ∘ g) ∘ x
         ↓⟨ assoc ⟩
           h ∘ (g ∘ x)
         ↓⟨ ∘-resp-≡ʳ pf₂ ⟩
           h ∘ (y ∘ i)
         ↑⟨ assoc ⟩
           (h ∘ y) ∘ i
         ↓⟨ ∘-resp-≡ˡ pf₁ ⟩
           (z ∘ f) ∘ i
         ↓⟨ assoc ⟩
           z ∘ (f ∘ i)
         ∎
      where
      open HomReasoning

  id′ : ∀ {A} → A ⇒′ A
  id′ = arrarr (sym id-comm)

  .assoc′ : ∀ {A B C D} {f : A ⇒′ B} {g : B ⇒′ C} {h : C ⇒′ D} → (h ∘′ g) ∘′ f ≡′ h ∘′ (g ∘′ f)
  assoc′ = assoc , assoc

module Congruent {q} (Q : Congruence C q) where
  open Congruence Q
  open Heterogeneous Q renaming (refl to ⇉-refl; sym to ⇉-sym; trans to ⇉-trans)

  ArrowEq : Rel ArrowObj _
  ArrowEq (arrobj f) (arrobj g) = f ∼ g

  private
    _⇉_ : Rel ArrowObj _
    _⇉_ = ArrowEq

    open Category arrow using () renaming (_≡_ to _≡′_; _∘_ to _∘′_)

    force : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ⇉ X₂) (pfY : Y₁ ⇉ Y₂)
            → (f : Arrow⇒ X₁ Y₁) → Arrow⇒ X₂ Y₂
    force {arrobj h₁} {arrobj h₂} {arrobj k₁} {arrobj k₂}
          (≡⇒∼ sh th ah) (≡⇒∼ sk tk ak) (arrarr {f} {g} square) = arrarr (
      begin
        coerce th tk g ∘ h₂
      ↑⟨ ∘-resp-≡ʳ ah ⟩
        coerce th tk g ∘ coerce sh th h₁
      ↑⟨ coerce-∘ _ _ _ _ _ ⟩
        coerce sh tk (g ∘ h₁)
      ↓⟨ coerce-resp-≡ _ _ square ⟩
        coerce sh tk (k₁ ∘ f)
      ↓⟨ coerce-∘ _ _ _ _ _ ⟩
        coerce sk tk k₁ ∘ coerce sh sk f
      ↓⟨ ∘-resp-≡ˡ ak ⟩
        k₂ ∘ coerce sh sk f
      ∎)
      where open HomReasoning

    .force-resp-≡′ : ∀ {X₁ X₂ Y₁ Y₂} (pfX : X₁ ⇉ X₂) (pfY : Y₁ ⇉ Y₂)
                  → {f₁ f₂ : Arrow⇒ X₁ Y₁}
                  → f₁ ≡′ f₂ → force pfX pfY f₁ ≡′ force pfX pfY f₂
    force-resp-≡′ (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (eq₁ , eq₂)
      = coerce-resp-≡ _ _ eq₁ , coerce-resp-≡ _ _ eq₂

    .force-refl : ∀ {X Y} (f : Arrow⇒ X Y) → force ⇉-refl ⇉-refl f ≡′ f
    force-refl f = coerce-refl _ , coerce-refl _

    .force-inv : ∀ {X₁ X₂ Y₁ Y₂} (pfX₁ pfX₂ : X₁ ⇉ X₂) (pfY₁ pfY₂ : Y₁ ⇉ Y₂)
                 → (f : Arrow⇒ X₁ Y₁) → force pfX₁ pfY₁ f ≡′ force pfX₂ pfY₂ f
    force-inv (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) f
      = coerce-invariant _ _ _ _ _ , coerce-invariant _ _ _ _ _

    .force-trans : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃} (pfX₁ : X₁ ⇉ X₂) (pfX₂ : X₂ ⇉ X₃)
                                         (pfY₁ : Y₁ ⇉ Y₂) (pfY₂ : Y₂ ⇉ Y₃)
                   → (f : Arrow⇒ X₁ Y₁)
                   →    force (⇉-trans pfX₁ pfX₂) (⇉-trans pfY₁ pfY₂) f
                     ≡′ force pfX₂ pfY₂ (force pfX₁ pfY₁ f)
    force-trans (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) f
      = coerce-trans _ _ _ _ _ , coerce-trans _ _ _ _ _

    .force-∘′ : ∀ {X₁ X₂ Y₁ Y₂ Z₁ Z₂}
                → (pfX : X₁ ⇉ X₂) (pfY : Y₁ ⇉ Y₂) (pfZ : Z₁ ⇉ Z₂)
                → (g : Arrow⇒ Y₁ Z₁) (f : Arrow⇒ X₁ Y₁)
                → force pfX pfZ (g ∘′ f) ≡′ force pfY pfZ g ∘′ force pfX pfY f
    force-∘′ (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) (≡⇒∼ _ _ _) g f
      = coerce-∘ _ _ _ _ _ , coerce-∘ _ _ _ _ _

  arrowQ : Congruence arrow _
  arrowQ = record
    { _≡₀_ = ArrowEq
    ; equiv₀ = record
      { refl = ⇉-refl
      ; sym = ⇉-sym
      ; trans = ⇉-trans
      }
    ; coerce = force
    ; coerce-resp-≡ = force-resp-≡′
    ; coerce-refl = force-refl
    ; coerce-invariant = force-inv
    ; coerce-trans = force-trans
    ; coerce-∘ = force-∘′
    }

open Congruent (TrivialCongruence C) public using () renaming (arrowQ to arrow∼)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Data.Fin.Indexed.Base where

open import Data.Nat using (ℕ; suc; zero)
open import Agda.Builtin.Nat using (_<_)
open import Level
open import Data.Bool.Truth

private variable n m : ℕ

-- This is the more traditional definition of Fin,
-- that you would usually find in Agda code.
-- I tend to use the other one because cubical
-- Agda doesn't yet support transport along
-- equalities of indexed types.
data Fin : ℕ → Type where
  f0 : Fin (suc n)
  fs : Fin n → Fin (suc n)

FinToℕ : Fin n → ℕ
FinToℕ f0 = zero
FinToℕ (fs i) = suc (FinToℕ i)

{-# DISPLAY f0 = zero #-}
{-# DISPLAY fs n = suc n #-}

FinFromℕ : ∀ {m} → (n : ℕ) → T (n < m) → Fin m
FinFromℕ {m = suc m} zero    p = f0
FinFromℕ {m = suc m} (suc n) p = fs (FinFromℕ n p)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.Fin.Instance where

open import Class.Equality
open import Class.Traversable
open import Data.Fin renaming (_≟_ to _≟F_)
open import Data.Fin.Map

instance
  Eq-Fin : ∀ {n} -> Eq (Fin n)
  Eq-Fin = record { _≟_ = _≟F_ }

  Traversable-Fin-Map : ∀ {a} {n} -> Traversable {a} (FinMap n)
  Traversable-Fin-Map = record { sequence = sequenceDepFinMap }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------
-- Various properties
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Delay-monad.Alternative.Properties where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (↑)

open import Bijection equality-with-J as Bijection using (_↔_)
open import Embedding equality-with-J as Embedding using (Embedding)
open import Equality.Decision-procedures equality-with-J
import Equality.Groupoid equality-with-J as EG
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Groupoid equality-with-J
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import Injection equality-with-J using (Injective)
import Nat equality-with-J as N

open import Delay-monad.Alternative

------------------------------------------------------------------------
-- Lemmas related to h-levels

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

  -- _↑ is a family of propositions.

  ↑-propositional : (x : Maybe A) → Is-proposition (x ↑)
  ↑-propositional nothing =
                                        $⟨ mono (N.zero≤ 2) ⊤-contractible ⟩
    Is-proposition (tt ≡ tt)            ↝⟨ H-level.respects-surjection (_↔_.surjection Bijection.≡↔inj₁≡inj₁) 1 ⟩□
    Is-proposition (nothing ≡ nothing)  □

  ↑-propositional (just x) = [inhabited⇒+]⇒+ 0 (

    just x ≡ nothing           ↝⟨ ⊎.inj₁≢inj₂ ∘ sym ⟩
    ⊥₀                         ↝⟨ ⊥-elim ⟩□
    Is-proposition (just x ↑)  □)

  -- LE nothing is a family of contractible types.

  LE-nothing-contractible :
    {x : Maybe A} → Contractible (LE nothing x)
  LE-nothing-contractible {x = x} =
    propositional⇒inhabited⇒contractible
      (λ where
         (inj₁ x↑)        (inj₂ (_ , ¬x↑)) → ⊥-elim (¬x↑ (sym x↑))
         (inj₂ (_ , ¬x↑)) (inj₁ x↑)        → ⊥-elim (¬x↑ (sym x↑))

         (inj₁ p)         (inj₁ q)         →
                                 $⟨ ↑-propositional _ ⟩
           Is-proposition (x ↑)  ↝⟨ (λ hyp → hyp _ _) ⦂ (_ → _) ⟩
           sym p ≡ sym q         ↔⟨ Eq.≃-≡ $ from-bijection $ Groupoid.⁻¹-bijection (EG.groupoid _) ⟩
           p ≡ q                 ↔⟨ Bijection.≡↔inj₁≡inj₁ ⟩□
           inj₁ p ≡ inj₁ q       □

         (inj₂ p) (inj₂ q) →
                                               $⟨ ×-closure 1 (↑-propositional _) (¬-propositional ext) ⟩
           Is-proposition (nothing ↑ × ¬ x ↑)  ↝⟨ (λ hyp → hyp _ _) ⦂ (_ → _) ⟩
           p ≡ q                               ↔⟨ Bijection.≡↔inj₂≡inj₂ ⟩□
           inj₂ p ≡ inj₂ q                     □)
      (case x return LE nothing of λ where
         nothing  → inj₁ refl
         (just x) → inj₂ (refl , ⊎.inj₁≢inj₂ ∘ sym))

  -- If A is a set, then LE is a family of propositions.

  LE-propositional :
    Is-set A → {x y : Maybe A} → Is-proposition (LE x y)
  LE-propositional A-set = irr _ _
    where
    irr : ∀ x y → Is-proposition (LE x y)
    irr nothing _ = mono₁ 0 LE-nothing-contractible

    irr (just x) (just y) (inj₁ p) (inj₁ q) =
      cong inj₁ $ Maybe-closure 0 A-set p q

    irr (just _) (just _) (inj₂ (() , _))
    irr (just _) (just _) _ (inj₂ (() , _))
    irr (just _) nothing  (inj₁ ())
    irr (just _) nothing  (inj₂ (() , _))

  -- If A is a set, then Increasing is a family of propositions.

  Increasing-propositional :
    Is-set A → {f : ℕ → Maybe A} → Is-proposition (Increasing f)
  Increasing-propositional A-set =
    Π-closure ext 1 λ _ →
    LE-propositional A-set

  -- An equality characterisation lemma which applies when A is a set.

  equality-characterisation :
    Is-set A →
    {x y : Delay A} → proj₁ x ≡ proj₁ y ↔ x ≡ y
  equality-characterisation A-set =
    ignore-propositional-component (Increasing-propositional A-set)

  -- If A has h-level 2 + n, then LE {A = A} x y has h-level 2 + n.

  LE-closure :
    ∀ {x y} n → H-level (2 + n) A → H-level (2 + n) (LE x y)
  LE-closure n h =
    ⊎-closure n
      (mono₁ (1 + n) (Maybe-closure n h))
      (mono (N.suc≤suc (N.zero≤ (1 + n)))
         (×-closure 1 (↑-propositional _)
                      (¬-propositional ext)))

  -- If A has h-level 2 + n, then Increasing {A = A} f has h-level
  -- 2 + n.

  Increasing-closure :
    ∀ {f} n → H-level (2 + n) A → H-level (2 + n) (Increasing f)
  Increasing-closure n h =
    Π-closure ext (2 + n) λ _ →
    LE-closure n h

  -- If A has h-level 2 + n, then Delay A has h-level 2 + n.

  Delay-closure :
    ∀ n → H-level (2 + n) A → H-level (2 + n) (Delay A)
  Delay-closure n h =
    Σ-closure (2 + n)
      (Π-closure ext (2 + n) λ _ →
       Maybe-closure n h)
      (λ _ → Increasing-closure n h)

------------------------------------------------------------------------
-- Various properties relating _↓_, _↑ and the usual ordering of the
-- natural numbers

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

  -- If f is increasing and f n has a value, then f (suc n) has the
  -- same value.

  ↓-step : ∀ {f} {x : A} {n} →
           Increasing f → f n ↓ x → f (suc n) ↓ x
  ↓-step {f = f} {x} {n} inc fn↓x = step (inc n)
    module ↓ where
    step : LE (f n) (f (suc n)) → f (suc n) ↓ x
    step (inj₁ fn≡f1+n) =

      f (suc n)  ≡⟨ sym fn≡f1+n ⟩
      f n        ≡⟨ fn↓x ⟩∎
      just x     ∎

    step (inj₂ (fn↑ , _)) =

      ⊥-elim $ ⊎.inj₁≢inj₂ (
        nothing  ≡⟨ sym fn↑ ⟩
        f n      ≡⟨ fn↓x ⟩∎
        just x   ∎)

  -- If f is increasing and f (suc n) does not have a value, then
  -- f n does not have a value.

  ↑-step : ∀ {f : ℕ → Maybe A} {n} →
           Increasing f → f (suc n) ↑ → f n ↑
  ↑-step {f} {n} inc f1+n↑ with inc n
  ... | inj₁ fn≡f1+n   = f n        ≡⟨ fn≡f1+n ⟩
                         f (suc n)  ≡⟨ f1+n↑ ⟩∎
                         nothing    ∎
  ... | inj₂ (fn↑ , _) = fn↑

  -- If f is increasing and f 0 has a value, then f n has the same
  -- value.

  ↓-upwards-closed₀ : ∀ {f} {x : A} →
                      Increasing f → f 0 ↓ x → ∀ n → f n ↓ x
  ↓-upwards-closed₀ _   f0↓ zero    = f0↓
  ↓-upwards-closed₀ inc f0↓ (suc n) =
    ↓-upwards-closed₀ (inc ∘ suc) (↓-step inc f0↓) n

  -- If f is increasing, then (λ n → f n ↓ x) is upwards closed.

  ↓-upwards-closed :
    ∀ {f : ℕ → Maybe A} {m n x} →
    Increasing f → m N.≤ n → f m ↓ x → f n ↓ x
  ↓-upwards-closed _   (N.≤-refl′ refl)     = id
  ↓-upwards-closed inc (N.≤-step′ m≤n refl) =
    ↓-step inc ∘ ↓-upwards-closed inc m≤n

  -- If f is increasing, then (λ n → f n ↑) is downwards closed.

  ↑-downwards-closed : ∀ {f : ℕ → Maybe A} {m n} →
                       Increasing f → m N.≤ n → f n ↑ → f m ↑
  ↑-downwards-closed inc (N.≤-refl′ refl)     = id
  ↑-downwards-closed inc (N.≤-step′ m≤n refl) =
    ↑-downwards-closed inc m≤n ∘ ↑-step inc

  -- If f is increasing and f m does not have a value, but f n does
  -- have a value, then m < n.

  ↑<↓ : ∀ {f : ℕ → Maybe A} {x m n} →
        Increasing f → f m ↑ → f n ↓ x → m N.< n
  ↑<↓ {f} {x} {m} {n} inc fm↑ fn↓x with n N.≤⊎> m
  ... | inj₂ m<n = m<n
  ... | inj₁ n≤m =
    ⊥-elim $ ⊎.inj₁≢inj₂
      (nothing  ≡⟨ sym $ ↑-downwards-closed inc n≤m fm↑ ⟩
       f n      ≡⟨ fn↓x ⟩∎
       just x   ∎)

------------------------------------------------------------------------
-- An unused lemma

private

  -- If the embedding g maps nothing to nothing and just to just, then
  -- there is an isomorphism between Increasing f and
  -- Increasing (g ∘ f).

  Increasing-∘ :
    ∀ {a b} {A : Type a} {B : Type b} {f : ℕ → Maybe A} →
    (g : Embedding (Maybe A) (Maybe B)) →
    Embedding.to g nothing ≡ nothing →
    (∀ {x} → Embedding.to g (just x) ≢ nothing) →
    Increasing f ↔ Increasing (Embedding.to g ∘ f)
  Increasing-∘ {A = A} {B} {f} g g↑ g↓ = record
    { surjection = record
      { logical-equivalence = record
        { to   = to   ∘_
        ; from = from ∘_
        }
      ; right-inverse-of = ⟨ext⟩ ∘ (to∘from ∘_)
      }
    ; left-inverse-of = ⟨ext⟩ ∘ (from∘to ∘_)
    }
    where
    g′ : Maybe A → Maybe B
    g′ = Embedding.to g

    g-injective : Injective g′
    g-injective = Embedding.injective (Embedding.is-embedding g)

    lemma₁ : ∀ {x} → x ↑ → g′ x ↑
    lemma₁ refl = g↑

    lemma₂ : ∀ x → ¬ x ↑ → ¬ g′ x ↑
    lemma₂ nothing  x↓ _ = x↓ refl
    lemma₂ (just _) _    = g↓

    lemma₃ : ∀ x → g′ x ↑ → x ↑
    lemma₃ nothing  _   = refl
    lemma₃ (just _) g↓↑ = ⊥-elim (lemma₂ _ (λ ()) g↓↑)

    lemma₄ : ∀ x → g′ x ≢ nothing → x ≢ nothing
    lemma₄ nothing  g↑↓ _  = g↑↓ g↑
    lemma₄ (just _) _   ()

    to : ∀ {n} → Increasing-at n f → Increasing-at n (g′ ∘ f)
    to = ⊎-map (cong g′) (Σ-map lemma₁ (lemma₂ _))

    from : ∀ {n} → Increasing-at n (g′ ∘ f) → Increasing-at n f
    from = ⊎-map g-injective (Σ-map (lemma₃ _) (lemma₄ _))

    to∘from : ∀ {n} (x : Increasing-at n (g′ ∘ f)) → to (from x) ≡ x
    to∘from (inj₁ p) = cong inj₁ (
      cong g′ (g-injective p)  ≡⟨ _≃_.right-inverse-of (Embedding.equivalence g) _ ⟩∎
      p                        ∎)
    to∘from (inj₂ _) = cong inj₂ $
      ×-closure 1 (↑-propositional _) (¬-propositional ext) _ _

    from∘to : ∀ {n} (x : Increasing-at n f) → from (to x) ≡ x
    from∘to (inj₁ p) = cong inj₁ (
      g-injective (cong g′ p)  ≡⟨ _≃_.left-inverse-of (Embedding.equivalence g) _ ⟩∎
      p                        ∎)
    from∘to (inj₂ _) = cong inj₂ $
      ×-closure 1 (↑-propositional _) (¬-propositional ext) _ _

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedImplicit where

open import BasicIPC.Syntax.Hilbert public
open import BasicIPC.Semantics.KripkeConcreteGluedImplicit public

open ImplicitSyntax (_⊢_) (mono⊢) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A w} → w ⊩ A → unwrap w ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

  reify⋆ : ∀ {Ξ w} → w ⊩⋆ Ξ → unwrap w ⊢⋆ Ξ
  reify⋆ {∅}     ∙        = ∙
  reify⋆ {Ξ , A} (ts , t) = reify⋆ ts , reify t

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A
  ⟪K⟫ {A} a = app ck (reify a) ⅋ λ ξ →
                K (mono⊩ {A} ξ a)

  ⟪S⟫′ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ = app cs (syn s₁) ⅋ λ ξ s₂ →
                          app (app cs (mono⊢ (unwrap≤ ξ) (syn s₁))) (syn s₂) ⅋ λ ξ′ →
                            ⟪S⟫ (mono⊩ {A ▻ B ▻ C} (trans≤ ξ ξ′) s₁) (mono⊩ {A ▻ B} ξ′ s₂)

  _⟪,⟫′_ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a = app cpair (reify a) ⅋ λ ξ →
                   _,_ (mono⊩ {A} ξ a)

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = eval t γ ⟪$⟫ eval u γ
eval ci        γ = ci ⅋ K I
eval ck        γ = ck ⅋ K ⟪K⟫
eval cs        γ = cs ⅋ K ⟪S⟫′
eval cpair     γ = cpair ⅋ K _⟪,⟫′_
eval cfst      γ = cfst ⅋ K π₁
eval csnd      γ = csnd ⅋ K π₂
eval unit      γ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { _⊩ᵅ_   = λ w P → unwrap w ⊢ α P
      ; mono⊩ᵅ = λ ξ t → mono⊢ (unwrap≤ ξ) t
      }

-- Soundness with respect to the canonical model.

reflectᶜ : ∀ {A w} → unwrap w ⊢ A → w ⊩ A
reflectᶜ {α P}   t = t ⅋ t
reflectᶜ {A ▻ B} t = t ⅋ λ ξ a → reflectᶜ (app (mono⊢ (unwrap≤ ξ) t) (reify a))
reflectᶜ {A ∧ B} t = reflectᶜ (fst t) , reflectᶜ (snd t)
reflectᶜ {⊤}    t = ∙

reflectᶜ⋆ : ∀ {Ξ w} → unwrap w ⊢⋆ Ξ → w ⊩⋆ Ξ
reflectᶜ⋆ {∅}     ∙        = ∙
reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {w} → w ⊩⋆ unwrap w
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆

trans⊩⋆ : ∀ {w w′ w″} → w ⊩⋆ unwrap w′ → w′ ⊩⋆ unwrap w″ → w ⊩⋆ unwrap w″
trans⊩⋆ ts us = reflectᶜ⋆ (trans⊢⋆ (reify⋆ ts) (reify⋆ us))

-- Completeness with respect to all models, or quotation.

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ A
quot s = reify (s refl⊩⋆)

-- Normalisation by evaluation.

norm : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A
norm = quot ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.


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

{- This is a copy of Sane, but building upon a rather different notion of permutation -}
module Sane2 where

import Data.Fin as F
--
open import Data.Unit
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _>_ )
open import Data.Sum using (inj₁ ; inj₂ ; _⊎_)
open import Data.Vec
open import Function using ( id ) renaming (_∘_ to _○_)
open import Relation.Binary  -- to make certain goals look nicer
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning )
open ≡-Reasoning

-- start re-splitting things up, as this is getting out of hand
open import FT -- Finite Types
open import VecHelpers
open import NatSimple
open import Eval
open import Permutations

open import CombPerm

-- Suppose we have some combinator c, its output vector v, and the corresponding
-- permutation p. We construct p by looking at how many places each element is
-- displaced from its index in v *to the right* (if it's where it "should" be or
-- to the left, just return 0).

-- In other words, if v[i] = j, then p[j] = j - i. That is, if j is in location
-- i, j - i is how many spaces to the right (if any) j appears from its own
-- index. Note that if v[i] = j, then c(i) = j, and inv(c)(j) = i. This suggests
-- that if I can write a tabulate function for permutations, the permutation for
-- a combinator c will be "tabulate (∩ -> i - (evalCombB c i))", modulo type
-- coercions.
--
-- JC: I think an even easier way is to use LeftCancellation and build it
--    recursively!  By this I mean something which gives a
--    (fromℕ n ⇛ fromℕ n) given a (fromℕ (suc n) ⇛ fromℕ (suc n))
combToPerm : {n : ℕ} → (fromℕ n ⇛ fromℕ n) → Permutation n
combToPerm {zero} c = []
combToPerm {suc n} c = valToFin (evalComb c (inj₁ tt)) ∷ {!!}

-- This is just nasty, prove it 'directly'
key-lemma : {n : ℕ} (i : F.Fin (suc n)) (j : F.Fin (suc (suc n))) →
      (lookup
       (lookup
        ((F.inject₁ i ∷ remove (F.inject₁ i) vId) !! j)
        (insert (remove (F.inject₁ i) vId) (F.suc i) (F.inject₁ i)))
       (insert vS (F.inject₁ i) F.zero))
      ≡
       (F.suc i ∷ insert (remove i vS) i F.zero) !! j
key-lemma {zero} F.zero F.zero = refl
key-lemma {zero} F.zero (F.suc F.zero) = refl
key-lemma {zero} F.zero (F.suc (F.suc ()))
key-lemma {zero} (F.suc ()) j
key-lemma {suc n} F.zero F.zero = refl
key-lemma {suc n} F.zero (F.suc j) =
  begin
    lookup (lookup (vS !! j) swap01vec) vId
      ≡⟨ lookupTab {f = id} (lookup (vS !! j) swap01vec) ⟩
    lookup (vS !! j) swap01vec
      ≡⟨ cong (λ z → lookup z swap01vec) (lookupTab {f = F.suc} j) ⟩
    lookup (F.suc j) swap01vec
      ≡⟨ refl ⟩
     lookup j (F.zero ∷ vSS)
  ∎
key-lemma {suc n} (F.suc i) F.zero =
  begin
    lookup
      (lookup (F.inject₁ i)
       (insert (remove (F.inject₁ i) (tabulate F.suc)) (F.suc i) (F.suc (F.inject₁ i))))
      (F.suc F.zero ∷
       insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)
      ≡⟨ cong (λ z → lookup z (F.suc F.zero ∷ insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)) (lookup+1-insert-remove i (tabulate F.suc)) ⟩
    lookup (lookup (F.suc i) (tabulate F.suc)) (F.suc F.zero ∷ insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)
      ≡⟨ cong (λ z → lookup z  (F.suc F.zero ∷ insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)) (lookupTab {f = F.suc} (F.suc i)) ⟩
   lookup (F.suc (F.suc i))  (F.suc F.zero ∷ insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)
      ≡⟨ refl ⟩
   lookup (F.suc i)  (insert (tabulate (F.suc ○ F.suc)) (F.inject₁ i) F.zero)
      ≡⟨ sym (lookup-insert3 i (tabulate (F.suc ○ F.suc))) ⟩
   lookup i (tabulate (F.suc ○ F.suc))
      ≡⟨ lookupTab {f = F.suc ○ F.suc} i ⟩
    F.suc (F.suc i)
  ∎
key-lemma {suc n} (F.suc i) (F.suc j) =
  begin
     (lookup
       (lookup
        (lookup j
         (remove (F.inject₁ (F.suc i)) vId))
        (insert
         (remove (F.inject₁ (F.suc i)) vId)
         (F.suc (F.suc i)) (F.inject₁ (F.suc i))))
       (insert vS (F.inject₁ (F.suc i)) F.zero))
        ≡⟨ refl ⟩ -- lots of β
     (lookup
       (lookup
        ((F.zero ∷ remove (F.inject₁ i) vS) !! j)
          (F.zero ∷ insert (remove (F.inject₁ i) vS) (F.suc i) (F.inject₁ (F.suc i))))
       (F.suc F.zero ∷ insert vSS (F.inject₁ i) F.zero))
        ≡⟨ {!!} ⟩
    (F.suc F.zero ∷ insert (remove i vSS) i F.zero) !! j
        ≡⟨ refl ⟩
    (insert (remove (F.suc i) vS) (F.suc i) F.zero) !! j
  ∎
{-    (lookup
       (lookup
        ((F.inject₁ i ∷ remove (F.inject₁ i) vId) !! j)
        (insert (remove (F.inject₁ i) vId) (F.suc i) (F.inject₁ i)))
       (insert vS (F.inject₁ i) F.zero))
      ≡
       (F.suc i ∷ insert (remove i vS) i F.zero) !! j -}
--------------------------------------------------------------------------------------------------------------

-- shuffle is like permute, but takes a combinator rather than a permutation as input

shuffle : {n : ℕ} {A : Set} → (fromℕ n ⇛ fromℕ n) → Vec A n → Vec A n
shuffle c v = tabulate (λ x → v !! valToFin (evalComb c (finToVal x)))

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

swapUpCorrect : {n : ℕ} → (i : F.Fin n) → (j : F.Fin (1 + n)) →
                evalComb (swapUpTo i) (finToVal j) ≡ finToVal (evalPerm (swapUpToPerm i) j)
swapUpCorrect {zero} () j
swapUpCorrect {suc zero} F.zero F.zero = refl
swapUpCorrect {suc zero} F.zero (F.suc F.zero) = refl
swapUpCorrect {suc zero} F.zero (F.suc (F.suc ()))
swapUpCorrect {suc zero} (F.suc ()) j
swapUpCorrect {suc (suc n)} F.zero j = cong finToVal (
  begin
    j                            ≡⟨ sym (lookupTab {f = id} j) ⟩
    lookup j (tabulate id)       ≡⟨ cong (λ x → lookup j (F.zero ∷ F.suc F.zero ∷ F.suc (F.suc F.zero) ∷ x)) (sym (idP-id (tabulate (F.suc ○ F.suc ○ F.suc)))) ⟩
    evalPerm (swapUpToPerm F.zero) j ∎ )
swapUpCorrect {suc (suc n)} (F.suc i) F.zero = refl
swapUpCorrect {suc (suc n)} (F.suc i) (F.suc j) =
  begin
    evalComb (assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛) (inj₂ (evalComb (swapUpTo i) (finToVal j)))
         ≡⟨ cong (λ x → evalComb (assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛) (inj₂ x)) (swapUpCorrect i j) ⟩
    evalComb (assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛) (inj₂ (finToVal (evalPerm (swapUpToPerm i) j)))
         ≡⟨ swapi≡swap01 (F.suc (evalPerm (swapUpToPerm i) j)) ⟩
    finToVal (evalPerm (swap01 (suc (suc (suc n)))) (F.suc (evalPerm (swapUpToPerm i) j)))
         ≡⟨ cong finToVal ( begin
             evalPerm (swap01 (suc (suc (suc n)))) (F.suc (evalPerm (swapUpToPerm i) j))
                 ≡⟨ cong (λ x → evalPerm (swap01 (suc (suc (suc n)))) (F.suc (lookup j x))) (swapUpToAct i (tabulate id)) ⟩
             lookup
                (F.suc (lookup j (insert (tabulate (λ z → F.suc z)) (F.inject₁ i) F.zero)))
                (F.suc F.zero ∷ F.zero ∷ F.suc (F.suc F.zero) ∷ permute idP (tabulate (λ z → F.suc (F.suc (F.suc z)))))
                  ≡⟨ cong (λ x → (lookup
                    (F.suc
                     (lookup j
                      (insert (tabulate F.suc) (F.inject₁ i) F.zero)))
                      (F.suc F.zero ∷ F.zero ∷ F.suc (F.suc F.zero) ∷ x)))
                    (idP-id _) ⟩
             (swap01vec !!
                 (F.suc ((insert (tabulate F.suc) (F.inject₁ i) F.zero) !! j)))
                  ≡⟨ cong (λ x → swap01vec !! x) (sym (map!! F.suc _ j)) ⟩
             (swap01vec !!
                 (vmap F.suc (insert (tabulate F.suc) (F.inject₁ i) F.zero) !! j))
                  ≡⟨ sym (lookupTab {f = (λ j →
                       (swap01vec !!
                          (vmap F.suc (insert (tabulate F.suc) (F.inject₁ i) F.zero) !! j)))} j) ⟩
             (tabulate (λ k → (swap01vec !!
                 (vmap F.suc (insert (tabulate F.suc) (F.inject₁ i) F.zero) !! k))) !! j)
                  ≡⟨ refl ⟩
             (((vmap F.suc (insert (tabulate F.suc) (F.inject₁ i) F.zero)) ∘̬ swap01vec) !! j)
                  ≡⟨ cong (λ x → x !! j) (∘̬≡∘̬′ _ _) ⟩
             (((vmap F.suc (insert (tabulate F.suc) (F.inject₁ i) F.zero)) ∘̬′ swap01vec) !! j)
                  ≡⟨ cong (λ x →
                       ((vmap F.suc (insert x (F.inject₁ i) F.zero) ∘̬′ swap01vec) !! j))
                       (sym (mapTab F.suc id)) ⟩
{-- For reference:
newlemma6 : {m n : ℕ} → (i : F.Fin n) → (v : Vec (F.Fin m) n) →
            (vmap F.suc (insert (vmap F.suc v) (F.inject₁ i) F.zero)) ∘̬′ swap01vec
          ≡ insert (vmap F.suc (vmap F.suc v)) (F.inject₁ i) F.zero
--}
             (((vmap F.suc (insert (vmap F.suc (tabulate id)) (F.inject₁ i) F.zero)) ∘̬′ swap01vec) !! j)
                 ≡⟨ cong (λ x → x !! j) (newlemma6 i (tabulate id)) ⟩
             (insert (vmap F.suc (vmap F.suc (tabulate id))) (F.inject₁ i) F.zero !! j)
                 ≡⟨ cong (λ x → insert (vmap F.suc x) (F.inject₁ i) F.zero !! j)
                         (mapTab F.suc id) ⟩
             (insert (vmap F.suc (tabulate F.suc)) (F.inject₁ i) F.zero !! j)
                 ≡⟨ cong (λ x → insert x (F.inject₁ i) F.zero !! j)
                         (mapTab F.suc F.suc) ⟩
             (insert (tabulate (λ x → F.suc (F.suc x))) (F.inject₁ i) F.zero !! j)
                 ≡⟨ cong (λ x → lookup j (insert x (F.inject₁ i) F.zero))
                        (sym (idP-id _)) ⟩
             (lookup j
                 (insert (permute idP (tabulate (λ x → F.suc (F.suc x)))) (F.inject₁ i) F.zero))
                 ≡⟨ refl ⟩
             evalPerm (swapUpToPerm (F.suc i)) (F.suc j)
           ∎ ) ⟩
    finToVal (evalPerm (swapUpToPerm (F.suc i)) (F.suc j))
  ∎

swapDownCorrect : {n : ℕ} → (i : F.Fin n) → (j : F.Fin (1 + n)) →
                  evalComb (swapDownFrom i) (finToVal j) ≡
                  finToVal (evalPerm (swapDownFromPerm i) j)
swapDownCorrect F.zero j =
  begin
    evalComb (swapDownFrom F.zero) (finToVal j)
      ≡⟨ refl ⟩
    finToVal j
      ≡⟨ cong finToVal (sym (lookupTab {f = id} j)) ⟩
    finToVal ((tabulate id) !! j)
      ≡⟨ cong (λ x → finToVal (x !! j)) (sym (idP-id (tabulate id))) ⟩
    finToVal (permute idP (tabulate id) !! j)
      ≡⟨ refl ⟩
    finToVal (evalPerm (swapDownFromPerm F.zero) j) ∎
swapDownCorrect (F.suc i) F.zero =
  begin
    evalComb (swapDownFrom (F.suc i)) (finToVal F.zero)
      ≡⟨ refl ⟩
    evalComb (swapi F.zero ◎ (id⇛ ⊕ swapDownFrom i)) (finToVal F.zero)
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (evalComb (swapi F.zero) (finToVal F.zero))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (finToVal (F.suc F.zero))
      ≡⟨ refl ⟩
    inj₂ (evalComb (swapDownFrom i) (finToVal F.zero))
      ≡⟨ cong inj₂ (swapDownCorrect i F.zero) ⟩
    inj₂ (finToVal (evalPerm (swapDownFromPerm i) F.zero))
      ≡⟨ refl ⟩
    finToVal (F.suc (evalPerm (swapDownFromPerm i) F.zero))
      ≡⟨ refl ⟩ -- beta
    finToVal (F.suc (permute (swapDownFromPerm i) (tabulate id) !! F.zero))
      ≡⟨ cong finToVal (push-f-through F.suc F.zero (swapDownFromPerm i) id ) ⟩
    finToVal (lookup F.zero (permute (swapDownFromPerm i) (tabulate F.suc)))
      ≡⟨ cong finToVal (sym (lookup-insert (permute (swapDownFromPerm i) (tabulate F.suc))))  ⟩
    finToVal (evalPerm (swapDownFromPerm (F.suc i)) F.zero) ∎
swapDownCorrect (F.suc i) (F.suc F.zero) =
  begin
    evalComb (swapDownFrom (F.suc i)) (finToVal (F.suc F.zero))
      ≡⟨ refl ⟩
    evalComb (swapi F.zero ◎ (id⇛ ⊕ swapDownFrom i)) (finToVal (F.suc F.zero))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (evalComb (swapi F.zero) (finToVal (F.suc F.zero)))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (inj₁ tt)
      ≡⟨ refl ⟩
    inj₁ tt
      ≡⟨ refl ⟩
    finToVal (F.zero)
      ≡⟨ cong finToVal (sym (lookup-insert′ (F.suc F.zero) (permute (swapDownFromPerm i) (tabulate F.suc)))) ⟩
    finToVal (evalPerm (swapDownFromPerm (F.suc i)) (F.suc F.zero)) ∎
swapDownCorrect (F.suc i) (F.suc (F.suc j)) =
  begin
    evalComb (swapDownFrom (F.suc i)) (finToVal (F.suc (F.suc j)))
      ≡⟨ refl ⟩
    evalComb (swapi F.zero ◎ (id⇛ ⊕ swapDownFrom i)) (finToVal (F.suc (F.suc j)))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (evalComb (swapi F.zero) (finToVal (F.suc (F.suc j))))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (finToVal (F.suc (F.suc j)))
      ≡⟨ refl ⟩
    evalComb (id⇛ ⊕ swapDownFrom i) (inj₂ (finToVal (F.suc j)))
      ≡⟨ refl ⟩
    inj₂ (evalComb (swapDownFrom i) (finToVal (F.suc j)))
      ≡⟨ cong inj₂ (swapDownCorrect i (F.suc j)) ⟩
    inj₂ (finToVal (evalPerm (swapDownFromPerm i) (F.suc j)))
      ≡⟨ refl ⟩
    finToVal (F.suc (evalPerm (swapDownFromPerm i) (F.suc j)))
      ≡⟨ cong finToVal (push-f-through F.suc (F.suc j) (swapDownFromPerm i) id) ⟩
      -- need to do a little β-expansion to see this
    finToVal (lookup (F.suc j) (permute (1iP i) (tabulate F.suc)))
      ≡⟨ cong finToVal (lookup-insert′′ j (permute (1iP i) (tabulate F.suc))) ⟩
    finToVal (evalPerm (swapDownFromPerm (F.suc i)) (F.suc (F.suc j))) ∎

swapmCorrect : {n : ℕ} → (i j : F.Fin n) → evalComb (swapm i) (finToVal j) ≡ finToVal (evalPerm (swapmPerm i) j)
swapmCorrect {zero} () _
swapmCorrect {suc n} F.zero j =
 begin
    finToVal j
      ≡⟨ cong finToVal (sym (lookupTab {f = id} j)) ⟩
    finToVal (lookup j (tabulate id))
      ≡⟨ cong (λ x → finToVal (lookup j x)) (sym (idP-id (tabulate id))) ⟩
    finToVal (lookup j (permute idP (tabulate id)))  ∎
swapmCorrect {suc zero} (F.suc ()) _
swapmCorrect {suc (suc n)} (F.suc i) j = -- requires the breakdown of swapm ?
  begin
    evalComb (swapm (F.suc i)) (finToVal j)
      ≡⟨ refl ⟩
    evalComb (swapDownFrom i ◎ swapi i ◎ swapUpTo i) (finToVal j)
      ≡⟨ refl ⟩
    evalComb (swapUpTo i)
      (evalComb (swapi i)
        (evalComb (swapDownFrom i) (finToVal j)))
      ≡⟨ cong (λ x → evalComb (swapUpTo i) (evalComb (swapi i) x))
           (swapDownCorrect i j) ⟩
    evalComb (swapUpTo i)
      (evalComb (swapi i)
        (finToVal (permute (swapDownFromPerm i) (tabulate id) !! j)))
      ≡⟨ cong (λ x → evalComb (swapUpTo i) x)
           (swapiCorrect i (permute (swapDownFromPerm i) (tabulate id) !! j)) ⟩
    evalComb (swapUpTo i)
      (finToVal
        (permute (swapiPerm i) (tabulate id) !!
          (permute (swapDownFromPerm i) (tabulate id) !! j)))
      ≡⟨ (swapUpCorrect i )
           (permute (swapiPerm i) (tabulate id) !!
             (permute (swapDownFromPerm i) (tabulate id) !! j))⟩
    finToVal
      (permute (swapUpToPerm i) (tabulate id) !!
        (permute (swapiPerm i) (tabulate id) !!
          (permute (swapDownFromPerm i) (tabulate id) !! j)))
      ≡⟨ cong (λ x → finToVal (x !! (permute (swapiPerm i) (tabulate id) !! (permute (swapDownFromPerm i) (tabulate id) !! j)))) (swapUpToAct i (tabulate id)) ⟩
    finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (permute (swapiPerm i) (tabulate id) !!
           (permute (swapDownFromPerm i) (tabulate id) !! j)))
      ≡⟨ cong (λ z → finToVal (insert (tabulate F.suc) (F.inject₁ i) F.zero !! (z !! (permute (swapDownFromPerm i) (tabulate id) !! j)))) (swapiAct i (tabulate id)) ⟩
    finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) ((tabulate id) !! (F.inject₁ i)) !!
           (permute (swapDownFromPerm i) (tabulate id) !! j)))
      ≡⟨ cong (λ z → finToVal (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) ((tabulate id) !! (F.inject₁ i)) !!
           (z !! j)))) (swapDownFromAct i (tabulate id)) ⟩
    finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) ((tabulate id) !! (F.inject₁ i)) !!
           ( swapDownFromVec (F.inject₁ i) (tabulate id) !! j)))
      ≡⟨ cong (λ z →  finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) z !!
           ( swapDownFromVec (F.inject₁ i) (tabulate id) !! j)))) (lookupTab {f = id} (F.inject₁ i)) ⟩
     finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) (F.inject₁ i) !!
           ( swapDownFromVec (F.inject₁ i) (tabulate id) !! j)))
      ≡⟨ refl ⟩
    finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) (F.inject₁ i) !!
           ( (((tabulate id) !! (F.inject₁ i)) ∷ (remove (F.inject₁ i) (tabulate id))) !! j)))
      ≡⟨ cong (λ z →     finToVal
       (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) (F.inject₁ i) !!
           ( (z ∷ (remove (F.inject₁ i) (tabulate id))) !! j)))) (lookupTab {f = id} (F.inject₁ i)) ⟩
    finToVal
      (insert (tabulate F.suc) (F.inject₁ i) F.zero !!
         (insert (remove (F.inject₁ i) (tabulate id)) (F.suc i) (F.inject₁ i) !!
           ( ((F.inject₁ i) ∷ (remove (F.inject₁ i) (tabulate id))) !! j)))
      ≡⟨ cong finToVal (key-lemma i j) ⟩
    finToVal ( ((F.suc i) ∷ (insert (remove i (tabulate F.suc)) i F.zero)) !! j)
      ≡⟨ cong (λ z → finToVal ((z ∷  (insert (remove i (tabulate F.suc)) i F.zero)) !! j)) (sym (lookupTab {f = F.suc} i)) ⟩
    finToVal ( (((tabulate F.suc) !! i) ∷ (insert (remove i (tabulate F.suc)) i F.zero)) !! j)
      ≡⟨ refl ⟩
    finToVal (swapmVec (F.suc i) (tabulate id) !! j)
      ≡⟨ cong (λ z → finToVal (z !! j)) (sym (swapmAct (F.suc i) (tabulate id))) ⟩
    finToVal (permute (swapmPerm (F.suc i)) (tabulate id) !! j)
      ≡⟨ refl ⟩
    finToVal (evalPerm (swapmPerm (F.suc i)) j) ∎

lemma1 : {n : ℕ} (p : Permutation n) → (i : F.Fin n) →
    evalComb (permToComb p) (finToVal i) ≡ finToVal (evalPerm p i)
lemma1 {zero} [] ()
lemma1 {suc n} (F.zero ∷ p) F.zero = refl
lemma1 {suc zero} (F.zero ∷ p) (F.suc ())
lemma1 {suc (suc n)} (F.zero ∷ p) (F.suc i) = begin
    inj₂ (evalComb (permToComb p) (finToVal i))
         ≡⟨ cong inj₂ (lemma1 p i) ⟩
     inj₂ (finToVal (evalPerm p i))
         ≡⟨ refl ⟩
      finToVal (F.suc (evalPerm p i))
         ≡⟨ cong finToVal (push-f-through F.suc i p id) ⟩
      finToVal (evalPerm (F.zero ∷ p) (F.suc i)) ∎
lemma1 {suc n} (F.suc j ∷ p) i = {!!} -- needs all the previous ones first.

{-  This is cleaner as a proof, but is not headed the right way as the cases are not the 'right' ones
swapmCorrect2 : {n : ℕ} → (i j : F.Fin n) → evalComb (swapm i) (finToVal j) ≡ finToVal (evalPerm (swapmPerm i) j)
swapmCorrect2 {zero} () _
swapmCorrect2 {suc zero} F.zero F.zero = refl
swapmCorrect2 {suc zero} F.zero (F.suc ())
swapmCorrect2 {suc zero} (F.suc ()) _
swapmCorrect2 {suc (suc n)} F.zero j = sym (
    trans (cong (λ x → finToVal (lookup j (F.zero ∷ F.suc F.zero ∷ x))) (idP-id (tabulate (F.suc ○ F.suc))))
          (cong finToVal (lookupTab {f = id} j)))
swapmCorrect2 {suc (suc n)} (F.suc F.zero) F.zero = refl
swapmCorrect2 {suc (suc n)} (F.suc (F.suc i)) F.zero =
  let up = λ x → evalComb (swapUpTo (F.suc i)) x
      swap = λ x → evalComb (swapi (F.suc i)) x
      down = λ x → evalComb (swapDownFrom (F.suc i)) x in
  begin
    evalComb (swapm (F.suc (F.suc i))) (inj₁ tt)
        ≡⟨ refl ⟩
    evalComb (swapDownFrom (F.suc i) ◎ swapi (F.suc i) ◎ swapUpTo (F.suc i)) (inj₁ tt)
        ≡⟨ refl ⟩
    up (swap (down (inj₁ tt)))
        ≡⟨ cong (up ○ swap) (swapDownCorrect (F.suc i) F.zero) ⟩
    up (swap ( finToVal (evalPerm (swapDownFromPerm (F.suc i)) F.zero) ))
        ≡⟨ refl ⟩
    up (swap (finToVal (permute (swapDownFromPerm (F.suc i)) (tabulate id) !! F.zero)))
        ≡⟨ cong (λ x → up (swap (finToVal (x !! F.zero )))) (swapDownFromAct (F.suc i) (tabulate id)) ⟩
    up (swap (finToVal (swapDownFromVec (F.inject₁ (F.suc i)) (tabulate id) !! F.zero)))
        ≡⟨ refl ⟩
    up (swap (finToVal ( (((tabulate id) !! (F.inject₁ (F.suc i))) ∷ remove (F.inject₁ (F.suc i)) (tabulate id)) !! F.zero )))
        ≡⟨ refl ⟩
    up (swap (finToVal ((tabulate id) !! (F.inject₁ (F.suc i)))))
        ≡⟨ cong (up ○ swap ○ finToVal) (lookupTab {f = id} (F.inject₁ (F.suc i))) ⟩
    up (swap (finToVal (F.inject₁ (F.suc i))))
        ≡⟨ cong up (swapiCorrect (F.suc i) (F.inject₁ (F.suc i))) ⟩
    up (finToVal (evalPerm (swapiPerm (F.suc i)) (F.inject₁ (F.suc i))))
        ≡⟨ refl ⟩
    up (finToVal (permute (swapiPerm (F.suc i)) (tabulate id) !! (F.inject₁ (F.suc i))))
        ≡⟨ cong (λ x → up (finToVal( x !! (F.inject₁ (F.suc i))))) (swapiAct (F.suc i) (tabulate id)) ⟩
    up (finToVal (insert (remove (F.inject₁ (F.suc i)) (tabulate id)) (F.suc (F.suc i)) ((tabulate id) !! (F.inject₁ (F.suc i))) !! (F.inject₁ (F.suc i))))
        ≡⟨ cong (λ x →  up (finToVal (insert (remove (F.inject₁ (F.suc i)) (tabulate id)) (F.suc (F.suc i)) x !! (F.inject₁ (F.suc i))))) (lookupTab {f = id} (F.inject₁ (F.suc i))) ⟩
    up (finToVal (insert (remove (F.inject₁ (F.suc i)) (tabulate id)) (F.suc (F.suc i)) (F.inject₁ (F.suc i)) !! (F.inject₁ (F.suc i))))
        ≡⟨ cong (up ○ finToVal) (lookup+1-insert-remove (F.suc i) (tabulate id)) ⟩
    up (finToVal (lookup (F.suc (F.suc i)) (tabulate id)))
        ≡⟨ cong (up ○ finToVal) (lookupTab {f = id} (F.suc (F.suc i))) ⟩
    up (finToVal (F.suc (F.suc i)))
        ≡⟨ swapUpCorrect (F.suc i) (F.suc (F.suc i)) ⟩
    finToVal (evalPerm (swapUpToPerm (F.suc i)) (F.suc (F.suc i)))
        ≡⟨ cong (λ x → finToVal (x !! (F.suc (F.suc i)))) (swapUpToAct (F.suc i) (tabulate id)) ⟩
    finToVal ( insert (tabulate F.suc) (F.inject₁ (F.suc i)) (F.zero) !! (F.suc (F.suc i)))
        ≡⟨ cong finToVal (sym (lookup-insert3 (F.suc i) (tabulate F.suc))) ⟩
    finToVal ((tabulate F.suc) !! (F.suc i))
        ≡⟨ cong finToVal (lookupTab {f = F.suc} (F.suc i)) ⟩
    finToVal (F.suc (F.suc i))
        ≡⟨ cong finToVal (sym (lookupTab {f = F.suc ○ F.suc} i)) ⟩
    finToVal (lookup i (tabulate (F.suc ○ F.suc)))
        ≡⟨ refl ⟩
    finToVal (lookup F.zero (swapmVec (F.suc (F.suc i)) (tabulate id)))
        ≡⟨ cong (λ x → finToVal (x !! F.zero)) (sym (swapmAct (F.suc (F.suc i)) (tabulate id))) ⟩
    finToVal (evalPerm (swapmPerm (F.suc (F.suc i))) F.zero)
  ∎
swapmCorrect2 {suc (suc n)} (F.suc F.zero) (F.suc j) =
  begin
    evalComb (swapi F.zero) (inj₂ (finToVal j))
      ≡⟨ swapi≡swap01 (F.suc j) ⟩
    finToVal
      (lookup j
       (F.zero ∷ permute idP (tabulate (λ z → F.suc (F.suc z)))))
      ≡⟨ refl ⟩
    finToVal (permute (F.suc F.zero ∷ idP) (tabulate id) !! (F.suc j))
  ∎
swapmCorrect2 {suc (suc n)} (F.suc (F.suc i)) (F.suc j) = {!!}
-}
{-
-- this alternate version of lemma1 might, in the long term, but a better
-- way to go?
lemma1′ : {n : ℕ} → (i : F.Fin n) → vmap (evalComb (swapm i)) (tabulate finToVal) ≡ vmap finToVal (permute (swapmPerm i) (tabulate id))
lemma1′ {zero} ()
lemma1′ {suc n} F.zero = cong (_∷_ (inj₁ tt)) (
  begin
    vmap id (tabulate (inj₂ ○ finToVal))
               ≡⟨ mapTab id (inj₂ ○ finToVal) ⟩
    tabulate (inj₂ ○ finToVal)
               ≡⟨ cong tabulate refl ⟩
    tabulate (finToVal ○ F.suc)
               ≡⟨ sym (mapTab finToVal F.suc) ⟩
    vmap finToVal (tabulate F.suc)
               ≡⟨ cong (vmap finToVal) (sym (idP-id _)) ⟩
    vmap finToVal (permute idP (tabulate F.suc))
  ∎ )
lemma1′ {suc n} (F.suc i) =
  begin
    vmap (evalComb (swapm (F.suc i))) (tabulate finToVal)
        ≡⟨ refl ⟩
    evalComb (swapm (F.suc i)) (inj₁ tt) ∷ vmap (evalComb (swapm (F.suc i))) (tabulate (inj₂ ○ finToVal))
       ≡⟨ cong (λ x → x ∷ vmap (evalComb (swapm (F.suc i))) (tabulate (inj₂ ○ finToVal))) (swapmCorrect {suc n} (F.suc i) F.zero) ⟩
    (finToVal (evalPerm (swapmPerm (F.suc i)) F.zero)) ∷ vmap (evalComb (swapm (F.suc i))) (tabulate (inj₂ ○ finToVal))
       ≡⟨ cong (λ x → (finToVal (evalPerm (swapmPerm (F.suc i)) F.zero)) ∷ x ) {!!} ⟩ -- need to generalize the inductive hyp. for this to work
    {!!}
       ≡⟨ {!!} ⟩
    vmap finToVal (insert (permute (swapOne i) (tabulate F.suc)) (F.suc i) F.zero)
  ∎

lemma2 : {n : ℕ} (c : (fromℕ n) ⇛ (fromℕ n)) → (i : F.Fin n) →
    (evalComb c (finToVal i)) ≡ finToVal (evalPerm (combToPerm c) i)
lemma2 c i = {!!}
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Functor.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function renaming (_∘_ to _◍_)
open import Cubical.Foundations.GroupoidLaws using (lUnit; rUnit; assoc; cong-∙)
open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base

private
  variable
    ℓ ℓ' ℓ'' : Level
    B C D E : Precategory ℓ ℓ'

open Precategory
open Functor

{-
x ---p--- x'
         ⇓ᵍ
       g x' ---q--- y
                   ⇓ʰ
                 h y ---r--- z

The path from `h (g x) ≡ z` obtained by
  1. first applying cong to p and composing with q; then applying cong again and composing with r
  2. first applying cong to q and composing with r; then applying a double cong to p and precomposing
are path equal.
-}
congAssoc : ∀ {X : Type ℓ} {Y : Type ℓ'} {Z : Type ℓ''} (g : X → Y) (h : Y → Z) {x x' : X} {y : Y} {z : Z}
          → (p : x ≡ x') (q : g x' ≡ y) (r : h y ≡ z)
          → cong (h ◍ g) p ∙ (cong h q ∙ r) ≡ cong h (cong g p ∙ q) ∙ r
congAssoc g h p q r
  = cong (h ◍ g) p ∙ (cong h q ∙ r)
  ≡⟨ assoc _ _ _ ⟩
    ((cong (h ◍ g) p) ∙ (cong h q)) ∙ r
  ≡⟨ refl ⟩
    (cong h (cong g p) ∙ (cong h q)) ∙ r
  ≡⟨ cong (_∙ r) (sym (cong-∙ h _ _)) ⟩
    cong h (cong g p ∙ q) ∙ r
  ∎

-- composition is associative
F-assoc : {F : Functor B C} {G : Functor C D} {H : Functor D E}
        → H ∘F (G ∘F F) ≡ (H ∘F G) ∘F F
F-assoc {F = F} {G} {H} i .F-ob x = H ⟅ G ⟅ F ⟅ x ⟆ ⟆ ⟆
F-assoc {F = F} {G} {H} i .F-hom f = H ⟪ G ⟪ F ⟪ f ⟫ ⟫ ⟫
F-assoc {F = F} {G} {H} i .F-id {x} =  congAssoc (G ⟪_⟫) (H ⟪_⟫) (F .F-id {x}) (G .F-id {F ⟅ x ⟆}) (H .F-id) (~ i)
F-assoc {F = F} {G} {H} i .F-seq f g =  congAssoc (G ⟪_⟫) (H ⟪_⟫) (F .F-seq f g) (G .F-seq _ _) (H .F-seq _ _) (~ i)

-- Results about functors

module _ {F : Functor C D} where

  -- the identity is the identity
  F-lUnit : F ∘F 𝟙⟨ C ⟩ ≡ F
  F-lUnit i .F-ob x = F ⟅ x ⟆
  F-lUnit i .F-hom f = F ⟪ f ⟫
  F-lUnit i .F-id {x} = lUnit (F .F-id) (~ i)
  F-lUnit i .F-seq f g = lUnit (F .F-seq f g) (~ i)

  F-rUnit : 𝟙⟨ D ⟩ ∘F F  ≡ F
  F-rUnit i .F-ob x = F ⟅ x ⟆
  F-rUnit i .F-hom f = F ⟪ f ⟫
  F-rUnit i .F-id {x} = rUnit (F .F-id) (~ i)
  F-rUnit i .F-seq f g = rUnit (F .F-seq f g) (~ i)

  -- functors preserve commutative diagrams (specificallysqures here)
  preserveCommF : ∀ {x y z w} {f : C [ x , y ]} {g : C [ y , w ]} {h : C [ x , z ]} {k : C [ z , w ]}
                → f ⋆⟨ C ⟩ g ≡ h ⋆⟨ C ⟩ k
                → (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ≡ (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫)
  preserveCommF {f = f} {g = g} {h = h} {k = k} eq
    = (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫)
    ≡⟨ sym (F .F-seq _ _) ⟩
      F ⟪ f ⋆⟨ C ⟩ g ⟫
    ≡⟨ cong (F ⟪_⟫) eq ⟩
      F ⟪ h ⋆⟨ C ⟩ k ⟫
    ≡⟨ F .F-seq _ _ ⟩
      (F ⟪ h ⟫) ⋆⟨ D ⟩ (F ⟪ k ⟫)
    ∎

  -- functors preserve isomorphisms
  preserveIsosF : ∀ {x y} → CatIso {C = C} x y → CatIso {C = D} (F ⟅ x ⟆) (F ⟅ y ⟆)
  preserveIsosF {x} {y} (catiso f f⁻¹ sec' ret') =
    catiso
      g g⁻¹
      -- sec
      ( (g⁻¹ ⋆⟨ D ⟩ g)
      ≡⟨ sym (F .F-seq f⁻¹ f) ⟩
        F ⟪ f⁻¹ ⋆⟨ C ⟩ f ⟫
      ≡⟨ cong (F .F-hom) sec' ⟩
        F ⟪ C .id y ⟫
      ≡⟨ F .F-id ⟩
        D .id y'
      ∎ )
      -- ret
      ( (g ⋆⟨ D ⟩ g⁻¹)
        ≡⟨ sym (F .F-seq f f⁻¹) ⟩
      F ⟪ f ⋆⟨ C ⟩ f⁻¹ ⟫
        ≡⟨ cong (F .F-hom) ret' ⟩
      F ⟪ C .id x ⟫
      ≡⟨ F .F-id ⟩
        D .id x'
      ∎ )

      where
        x' : D .ob
        x' = F ⟅ x ⟆
        y' : D .ob
        y' = F ⟅ y ⟆

        g : D [ x' , y' ]
        g = F ⟪ f ⟫
        g⁻¹ : D [ y' , x' ]
        g⁻¹ = F ⟪ f⁻¹ ⟫

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical