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

open import lib.Basics
open import lib.NType2
open import lib.types.Sigma

module lib.types.Modality where

  -- Where to put this?  Or maybe there's
  -- a simpler proof from some library function?
  !ᵈ-inv-l-out : ∀ {ℓ} {A : Type ℓ} {P : A → Type ℓ}
    {a₀ a₁ : A} {p : a₀ == a₁} {x₀ x₁ : P a₁}
    → (q : x₀ == x₁ [ P ↓ ! p ∙ p ])
    → x₀ == x₁
  !ᵈ-inv-l-out {p = idp} q = q

  record Modality ℓ : Type (lsucc ℓ) where
    field

      is-local : Type ℓ → Type ℓ
      is-local-is-prop : {A : Type ℓ} → is-prop (is-local A)

      ◯ : Type ℓ → Type ℓ
      ◯-is-local : {A : Type ℓ} → is-local (◯ A)

      η : {A : Type ℓ} → A → ◯ A

      ◯-elim : {A : Type ℓ} {B : ◯ A → Type ℓ}
        (B-local : (x : ◯ A) → is-local (B x))
        → Π A (B ∘ η) → Π (◯ A) B

      ◯-elim-β : {A : Type ℓ} {B : ◯ A → Type ℓ}
        (B-local : (x : ◯ A) → is-local (B x)) (f : Π A (B ∘ η))
        → (a : A) → ◯-elim B-local f (η a) == f a

      ◯-=-is-local : {A : Type ℓ} (a₀ a₁ : ◯ A) → is-local (a₀ == a₁)

    ◯-Type : Type (lsucc ℓ)
    ◯-Type = Σ (Type ℓ) is-local

    {- elimination rules -}

    module ◯Elim {A : Type ℓ} {B : ◯ A → Type ℓ}
      (B-local : (x : ◯ A) → is-local (B x)) (η* : Π A (B ∘ η)) where

      f = ◯-elim B-local η*
      η-β = ◯-elim-β B-local η*

    module ◯Rec {A : Type ℓ} {B : Type ℓ}
      (B-local : is-local B) (η* : A → B)
      = ◯Elim (λ _ → B-local) η*
    ◯-rec = ◯Rec.f
    ◯-rec-β = ◯Rec.η-β

    {- functoriality -}

    module ◯Fmap {A B : Type ℓ} (f : A → B) =
      ◯Rec ◯-is-local (η ∘ f)
    ◯-fmap = ◯Fmap.f
    ◯-fmap-β = ◯Fmap.η-β

    ◯-isemap : {A B : Type ℓ} (f : A → B) → is-equiv f → is-equiv (◯-fmap f)
    ◯-isemap f f-ise = is-eq _ (◯-fmap g) to-from from-to where
      open is-equiv f-ise
      abstract
        to-from : ∀ ◯b → ◯-fmap f (◯-fmap g ◯b) == ◯b
        to-from = ◯-elim
          (λ ◯b → ◯-=-is-local (◯-fmap f (◯-fmap g ◯b)) ◯b)
          (λ b → ap (◯-fmap f) (◯-fmap-β g b) ∙ ◯-fmap-β f (g b) ∙ ap η (f-g b))
        from-to : ∀ ◯a → ◯-fmap g (◯-fmap f ◯a) == ◯a
        from-to = ◯-elim
          (λ ◯a → ◯-=-is-local (◯-fmap g (◯-fmap f ◯a)) ◯a)
          (λ a → ap (◯-fmap g) (◯-fmap-β f a) ∙ ◯-fmap-β g (f a) ∙ ap η (g-f a))

    ◯-emap : {A B : Type ℓ} → A ≃ B → ◯ A ≃ ◯ B
    ◯-emap (f , f-ise) = ◯-fmap f , ◯-isemap f f-ise

    {- equivalences preserve locality -}

    -- This is the only appearence of univalence, but ...
    local-is-replete : {A B : Type ℓ} → is-local A → A ≃ B → is-local B
    local-is-replete w eq = transport is-local (ua eq) w

    -- This name aligns with the current codebase better.
    equiv-preserves-local : {A B : Type ℓ} → A ≃ B → is-local A → is-local B
    equiv-preserves-local e A-is-loc = local-is-replete A-is-loc e

    {- locality and [η] being an equivalence -}

    local-implies-η-equiv : {A : Type ℓ} → is-local A → is-equiv (η {A})
    local-implies-η-equiv {A} w = is-eq (η {A}) η-inv inv-l inv-r

       where η-inv : ◯ A → A
             η-inv = ◯-rec w (idf A)

             abstract
               inv-r : (a : A) → η-inv (η a) == a
               inv-r = ◯-rec-β w (idf A)

               inv-l : (a : ◯ A) → η (η-inv a) == a
               inv-l = ◯-elim (λ a₀ → ◯-=-is-local _ _)
                              (λ a₀ → ap η (inv-r a₀))

    abstract
      η-equiv-implies-local : {A : Type ℓ} → is-equiv (η {A}) → is-local A
      η-equiv-implies-local {A} eq = local-is-replete {◯ A} {A} ◯-is-local ((η , eq) ⁻¹)

      retract-is-local : {A B : Type ℓ} (w : is-local A)
        (f : A → B) (g : B → A) (r : (b : B) → f (g b) == b) →
        is-local B
      retract-is-local {A} {B} w f g r = η-equiv-implies-local (is-eq η η-inv inv-l inv-r)

        where η-inv : ◯ B → B
              η-inv = f ∘ (◯-rec w g)

              inv-r : (b : B) → η-inv (η b) == b
              inv-r b = ap f (◯-rec-β w g b) ∙ r b

              inv-l : (b : ◯ B) → η (η-inv b) == b
              inv-l = ◯-elim (λ b → ◯-=-is-local _ _) (λ b → ap η (inv-r b))

    {- locality of identification -}

    abstract
      =-preserves-local : {A : Type ℓ} → is-local A → {a₀ a₁ : A} → is-local (a₀ == a₁)
      =-preserves-local {A} w {a₀} {a₁} = local-is-replete
        (◯-=-is-local (η a₀) (η a₁)) (ap-equiv (η , local-implies-η-equiv w) a₀ a₁ ⁻¹)

  {- ◯-connectness and ◯-equivalences -}

    is-◯-connected : Type ℓ → Type ℓ
    is-◯-connected A = is-contr (◯ A)

    is-◯-connected-is-prop : ∀ {A} → is-prop (is-◯-connected A)
    is-◯-connected-is-prop {A} = is-contr-is-prop

    is-◯-equiv : {A B : Type ℓ} → (A → B) → Type ℓ
    is-◯-equiv {B = B} f = (b : B) → is-◯-connected (hfiber f b)

    has-◯-conn-fibers = is-◯-equiv

    is-lex : Type (lsucc ℓ)
    is-lex = {A B : Type ℓ} (f : A → B)
      → is-◯-connected A → is-◯-connected B → is-◯-equiv f

    equiv-preserves-◯-conn : {A B : Type ℓ} → A ≃ B → is-◯-connected A → is-◯-connected B
    equiv-preserves-◯-conn e c = equiv-preserves-level (◯-emap e) {{c}}

    total-◯-equiv : {A : Type ℓ} {P Q : A → Type ℓ} (φ : ∀ a → P a → Q a) →
                     (∀ a → is-◯-equiv (φ a)) → is-◯-equiv (Σ-fmap-r φ)
    total-◯-equiv φ e (a , q) = equiv-preserves-◯-conn (hfiber-Σ-fmap-r φ q ⁻¹) (e a q)

    module _ {A B : Type ℓ} {h : A → B} (c : is-◯-equiv h) (P : B → ◯-Type) where
      abstract
        pre∘-◯-conn-is-equiv : is-equiv (λ (s : Π B (fst ∘ P)) → s ∘ h)
        pre∘-◯-conn-is-equiv = is-eq f g f-g g-f

          where f : Π B (fst ∘ P) → Π A (fst ∘ P ∘ h)
                f k a = k (h a)

                helper : Π A (fst ∘ P ∘ h) → (b : B) → ◯ (Σ A (λ a → h a == b)) → (fst (P b))
                helper t b = ◯-rec (snd (P b)) (λ x → transport (fst ∘ P) (snd x) (t (fst x)))

                helper-β : (t : Π A (fst ∘ P ∘ h)) → (b : B) → (r : hfiber h b) →
                           helper t b (η r) == transport (fst ∘ P) (snd r) (t (fst r))
                helper-β t b = ◯-rec-β (snd (P b)) (λ x → transport (fst ∘ P) (snd x) (t (fst x)))

                g : Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
                g t b = helper t b (contr-center (c b))

                f-g : ∀ t → f (g t) == t
                f-g t = λ= $ λ a → transport
                  (λ r → ◯-rec (snd (P (h a))) _ r == t a)
                  (! (contr-path (c (h a)) (η (a , idp))))
                  (◯-rec-β (snd (P (h a))) _ (a , idp))

                g-f : ∀ k → g (f k) == k
                g-f k = λ= λ (b : B) →
                  ◯-elim {A = hfiber h b}
                         (λ r → =-preserves-local (snd (P b)) {g (f k) b})
                         (λ r → lemma₁ (fst r) b (snd r))
                         (contr-center (c b))

                    where lemma₀ : (a : A) → (b : B) → (p : h a == b) →
                                 helper (k ∘ h) b (η (a , p)) == k b
                          lemma₀ a .(h a) idp = helper-β (k ∘ h) (h a) (a , idp)

                          lemma₁ : (a : A) → (b : B) → (p : h a == b) →
                                 helper (k ∘ h) b (contr-center (c b)) == k b
                          lemma₁ a b p = transport! (λ r → helper (k ∘ h) b r == k b)
                            (contr-path (c b) (η (a , p))) (lemma₀ a b p)

      ◯-extend : Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
      ◯-extend = is-equiv.g pre∘-◯-conn-is-equiv

      ◯-extend-β : ∀ f a → ◯-extend f (h a) == f a
      ◯-extend-β f = app= (is-equiv.f-g pre∘-◯-conn-is-equiv f)

    {- locality of function types -}

    abstract
      Π-is-local : {A : Type ℓ} {B : A → Type ℓ} (w : (a : A) → is-local (B a)) → is-local (Π A B)
      Π-is-local {A} {B} w = retract-is-local {◯ (Π A B)} {Π A B} ◯-is-local η-inv η r

        where η-inv : ◯ (Π A B) → Π A B
              η-inv φ' a = ◯-rec (w a) (λ φ → φ a) φ'

              r : (φ : Π A B) → η-inv (η φ) == φ
              r φ = λ= (λ a → ◯-rec-β (w a) (λ φ₀ → φ₀ a) φ)

      →-is-local : {A B : Type ℓ} → is-local B → is-local (A → B)
      →-is-local w = Π-is-local (λ _ → w)

    -- Fmap2 because of locality of function types
    module ◯Fmap2 {A B C : Type ℓ} (η* : A → B → C) where
      private module M = ◯Rec (→-is-local ◯-is-local) (◯-fmap ∘ η*)
      f = M.f
      η-β : ∀ a b → f (η a) (η b) == η (η* a b)
      η-β a b = app= (M.η-β a) (η b) ∙ ◯-fmap-β (η* a) b
    ◯-fmap2 = ◯Fmap2.f
    ◯-fmap2-β = ◯Fmap2.η-β

    {- locality of sigma types -}

    abstract
      Σ-is-local : {A : Type ℓ} (B : A → Type ℓ)
        → is-local A → ((a : A) → is-local (B a))
        → is-local (Σ A B)
      Σ-is-local {A} B lA lB = retract-is-local {◯ (Σ A B)} {Σ A B} ◯-is-local η-inv η r

        where h : ◯ (Σ A B) → A
              h = ◯-rec lA fst

              h-β : (ab : Σ A B) → h (η ab) == fst ab
              h-β = ◯-rec-β lA fst

              k : (w : ◯ (Σ A B)) → B (h w)
              k = ◯-elim (lB ∘ h) λ ab → transport! B (h-β ab) (snd ab)

              k-β : (ab : Σ A B) → k (η ab) == snd ab [ B ↓ h-β ab ]
              k-β ab = from-transp! B (h-β ab) $
                ◯-elim-β (lB ∘ h) (λ ab → transport! B (h-β ab) (snd ab)) ab

              η-inv : ◯ (Σ A B) → Σ A B
              η-inv w = h w , k w

              r : (x : Σ A B) → η-inv (η x) == x
              r ab = pair= (h-β ab) (k-β ab)

      ×-is-local : {A B : Type ℓ}
        → is-local A → is-local B → is-local (A × B)
      ×-is-local {B = B} lA lB = Σ-is-local (λ _ → B) lA (λ _ → lB)

    ◯-×-econv : {A B : Type ℓ} → ◯ (A × B) ≃ ◯ A × ◯ B
    ◯-×-econv {A} {B} = equiv ◯-split ◯-pair inv-l inv-r

      where ◯-fst : ◯ (A × B) → ◯ A
            ◯-fst = ◯-fmap fst

            ◯-fst-β : (ab : A × B) → ◯-fst (η ab) == η (fst ab)
            ◯-fst-β = ◯-fmap-β fst

            ◯-snd : ◯ (A × B) → ◯ B
            ◯-snd = ◯-fmap snd

            ◯-snd-β : (ab : A × B) → ◯-snd (η ab) == η (snd ab)
            ◯-snd-β = ◯-fmap-β snd

            ◯-split : ◯ (A × B) → ◯ A × ◯ B
            ◯-split = fanout ◯-fst ◯-snd

            ◯-pair : ◯ A × ◯ B → ◯ (A × B)
            ◯-pair = uncurry (◯-fmap2 _,_)

            ◯-pair-β : (a : A) (b : B) → ◯-pair (η a , η b) == η (a , b)
            ◯-pair-β = ◯-fmap2-β _,_

            abstract
              inv-l : (ab : ◯ A × ◯ B) → ◯-split (◯-pair ab) == ab
              inv-l = uncurry $
                ◯-elim (λ _ → Π-is-local λ _ → =-preserves-local (×-is-local ◯-is-local ◯-is-local))
                  (λ a → ◯-elim (λ _ → =-preserves-local (×-is-local ◯-is-local ◯-is-local))
                    (λ b → ap ◯-split (◯-pair-β a b)
                         ∙ pair×= (◯-fst-β (a , b)) (◯-snd-β (a , b))))

              inv-r : (ab : ◯ (A × B)) → ◯-pair (◯-split ab) == ab
              inv-r = ◯-elim (λ _ → ◯-=-is-local _ _)
                             (λ ab → ap ◯-pair (pair×= (◯-fst-β ab) (◯-snd-β ab)) ∙ ◯-pair-β (fst ab) (snd ab))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Cubical.Data.DiffInt.Base public
open import Cubical.Data.DiffInt.Properties public

ext: agda

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module MLib.Fin.Parts where

open import MLib.Prelude
open import MLib.Prelude.RelProps
import MLib.Fin.Parts.Core as C
open import MLib.Fin.Parts.Nat

open import Function.Surjection using (_↠_)
open import Function.Related renaming (module EquationalReasoning to BijReasoning)

import Relation.Binary.Indexed as I

open Nat using (_*_; _+_; _<_)
open Fin using (toℕ; fromℕ≤)
open Table

open C using (Parts; constParts) hiding (module Parts) public

module Parts {a} {A : Set a} {size : A → ℕ} (P : Parts A size) where
  open C.Parts P public
  module PN = Partsℕ P

  -- Fin functions

  private
    bounded′ : ∀ {i} (j : Fin (sizeAt i)) → toℕ j < PN.sizeAt (fromℕ≤ (Fin.bounded i))
    bounded′ j = Nat.≤-trans (Fin.bounded j) (Nat.≤-reflexive (≡.sym (≡.cong sizeAt (Fin.fromℕ≤-toℕ _ _))))

  fromParts : Σ (Fin numParts) (Fin ∘ sizeAt) → Fin totalSize
  fromParts (i , j) = fromℕ≤ {PN.fromParts (toℕ i , toℕ j)} (PN.fromParts-prop (Fin.bounded i) (bounded′ j))

  toParts : Fin totalSize → Σ (Fin numParts) (Fin ∘ sizeAt)
  toParts k =
    let p , q = PN.toParts-prop (Fin.bounded k)
    in fromℕ≤ p , fromℕ≤ q

  abstract
    fromParts-fromPartsℕ : (i : Fin numParts) (j : Fin (sizeAt i)) → toℕ (fromParts (i , j)) ≡ PN.fromParts (toℕ i , toℕ j)
    fromParts-fromPartsℕ _ _ = Fin.toℕ-fromℕ≤ _

    toParts-toPartsℕ : (k : Fin totalSize) → Σ.map toℕ toℕ (toParts k) ≡ PN.toParts (toℕ k)
    toParts-toPartsℕ k = Σ.≡×≡⇒≡ (Fin.toℕ-fromℕ≤ _ , Fin.toℕ-fromℕ≤ _)

    toParts-fromParts : ∀ {i j} → toParts (fromParts (i , j)) ≡ (i , j)
    toParts-fromParts {i} {j} = Fin.toℕ-injective₂ (begin
      Σ.map toℕ toℕ (toParts (fromParts (i , j)))   ≡⟨ toParts-toPartsℕ _ ⟩
      PN.toParts (toℕ (fromParts (i , j)))          ≡⟨ ≡.cong PN.toParts (fromParts-fromPartsℕ i j) ⟩
      PN.toParts (PN.fromParts (toℕ i , toℕ j))    ≡⟨ PN.toParts-fromParts (Fin.bounded i) (bounded′ j) ⟩
      (toℕ i , toℕ j)                                 ∎)
      where open ≡.Reasoning

    fromParts-toParts : ∀ {k} → fromParts (toParts k) ≡ k
    fromParts-toParts {k} = Fin.toℕ-injective (
      begin
        toℕ (fromParts (toParts k))               ≡⟨ uncurry fromParts-fromPartsℕ (toParts k) ⟩
        PN.fromParts (Σ.map toℕ toℕ (toParts k))  ≡⟨ ≡.cong PN.fromParts (toParts-toPartsℕ k) ⟩
        PN.fromParts (PN.toParts (toℕ k))         ≡⟨ PN.fromParts-toParts (toℕ k) (Fin.bounded k) ⟩
        toℕ k                                       ∎)
      where open ≡.Reasoning

  asParts : Fin totalSize ↔ Σ (Fin numParts) (Fin ∘ sizeAt)
  asParts = record
    { to = ≡.→-to-⟶ toParts
    ; from = ≡.→-to-⟶ fromParts
    ; inverse-of = record
      { left-inverse-of = λ _ → fromParts-toParts
      ; right-inverse-of = λ _ → toParts-fromParts
      }
    }

Parts² : ∀ {a} (A : Set a) (size : A → ℕ) → Set a
Parts² A size = Parts (Parts A size) Parts.totalSize

module _ {a} {A : Set a} {size : A → ℕ} (P₁ : Parts² A size) where
  private
    module P₁ = Parts P₁

  module _ (i : Fin P₁.numParts) where
    private
      P₂ = P₁.partAt i
      module P₂ = Parts P₂

    fromParts² : (j : Fin P₂.numParts) → Fin (size (P₂.partAt j)) → Fin P₁.totalSize
    fromParts² j = curry P₁.fromParts i ∘ curry P₂.fromParts j

  asParts² :
    Fin P₁.totalSize ↔
    Σ (Fin P₁.numParts) (λ i →
      let P₂ = P₁.partAt i
          module P₂ = Parts P₂
      in Σ (Fin P₂.numParts) (Fin ∘ P₂.sizeAt))
  asParts² =
    Fin P₁.totalSize ↔⟨ P₁.asParts ⟩
    Σ (Fin P₁.numParts) (Fin ∘ P₁.sizeAt) ↔⟨ Σ-bij (Parts.asParts ∘ P₁.partAt) ⟩
    Σ (Fin P₁.numParts) (λ i →
      let P₂ = P₁.partAt i
          module P₂ = Parts P₂
      in Σ (Fin P₂.numParts) (Fin ∘ P₂.sizeAt)) ∎
    where open BijReasoning


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

open import Cubical.Core.Everything
open import Cubical.Algebra.Semigroup

module Cubical.Algebra.Semigroup.Construct.Opposite {ℓ} (S : Semigroup ℓ) where

open import Cubical.Foundations.Prelude

open Semigroup S

import Cubical.Algebra.Magma.Construct.Opposite magma as OpMagma
open OpMagma public hiding (Op-isMagma; Mᵒᵖ)

•ᵒᵖ-assoc : Associative _•ᵒᵖ_
•ᵒᵖ-assoc _ _ _ = sym (assoc _ _ _)

Op-isSemigroup : IsSemigroup Carrier _•ᵒᵖ_
Op-isSemigroup = record
  { isMagma = OpMagma.Op-isMagma
  ; assoc   = •ᵒᵖ-assoc
  }

Sᵒᵖ : Semigroup ℓ
Sᵒᵖ = record { isSemigroup = Op-isSemigroup }


text:
-- Andreas, 2014-09-09

{-# NON_TERMINATING #-}
Foo : Set
Foo = Foo

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Definition.Typed.Consequences.SucCong where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Congurence of the type of the successor case in natrec.
sucCong : ∀ {F G rF lF Γ} → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F ≡ G ^ [ rF , ι lF ]
        → Γ ⊢ Π ℕ ^ ! ° ⁰ ▹ (F ^ rF ° lF ▹▹ F [ suc (var 0) ]↑ ° lF ° lF) ° lF ° lF
            ≡ Π ℕ ^ ! ° ⁰ ▹ (G ^ rF ° lF ▹▹ G [ suc (var 0) ]↑ ° lF ° lF) ° lF ° lF ^ [ rF , ι lF ]
sucCong F≡G with wfEq F≡G
sucCong {lF = lF} F≡G | ⊢Γ ∙ ⊢ℕ =
  let ⊢F , _ = syntacticEq F≡G
  in  univ (Π-cong (⁰min lF) (≡is≤ PE.refl) ⊢ℕ (refl (un-univ ⊢ℕ))
             (Π-cong (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F (un-univ≡ F≡G)
                     (wkEqTerm (step id) (⊢Γ ∙ ⊢ℕ ∙ ⊢F)
                               (un-univ≡ (subst↑TypeEq F≡G
                                                       (refl (sucⱼ (var (⊢Γ ∙ ⊢ℕ) here))))))))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module Reasoning where

open import Algebra

-- Standard syntax sugar for writing equational proofs
infix 4 _≈_
data _≈_ {A} (x y : Graph A) : Set where
    prove : x ≡ y -> x ≈ y

infix 1 begin_
begin_ : ∀ {A} {x y : Graph A} -> x ≈ y -> x ≡ y
begin prove p = p

infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ {A} (x : Graph A) {y z : Graph A} -> x ≡ y -> y ≈ z -> x ≈ z
_ ≡⟨ p ⟩ prove q = prove (transitivity p q)

infix 3 _∎
_∎ : ∀ {A} (x : Graph A) -> x ≈ x
_∎ _ = prove reflexivity

infixl 8 _>>_
_>>_ : ∀ {A} {x y z : Graph A} -> x ≡ y -> y ≡ z -> x ≡ z
_>>_ = transitivity

data BinaryOperator : Set where
  +op : BinaryOperator
  *op : BinaryOperator

apply : ∀ {A} -> BinaryOperator -> Graph A -> Graph A -> Graph A
apply +op a b = a + b
apply *op a b = a * b

L : ∀ {op : BinaryOperator} -> ∀ {A} {x y z : Graph A} -> x ≡ y -> apply op x z ≡ apply op y z
L {+op} {x} {y} {z} eq = +left-congruence {x} {y} {z} eq
L {*op} {x} {y} {z} eq = *left-congruence {x} {y} {z} eq

R : ∀ {op : BinaryOperator} -> ∀ {A} {x y z : Graph A} -> x ≡ y -> apply op z x ≡ apply op z y
R {+op} {x} {y} {z} eq = +right-congruence {x} {y} {z} eq
R {*op} {x} {y} {z} eq = *right-congruence {x} {y} {z} eq

max_stars_repo_name: asr/alga

max_issues_repo_name: asr/alga

max_forks_repo_name: asr/alga


text:
module CTL.Modalities.EG where

open import FStream.Core
open import Library

-- Possibly forever : s₀ ⊧ φ ⇔ ∃ s₀ R s₁ R ... ∀ i . sᵢ ⊧ φ
{-# NO_POSITIVITY_CHECK #-} -- Not necessary from EGda 2.6 upwards
record EG' {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁}
  (props : FStream' C (Set ℓ₂)) : Set (ℓ₁ ⊔ ℓ₂) where
  coinductive
  field
    nowE   : head props
    laterE : {j : Size< i} → E (fmap EG' (inF (tail props)))
open EG' public

EG : ∀ {i : Size} {ℓ₁ ℓ₂} {C : Container ℓ₁}
   → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
EG props = EPred EG' (inF props)

mutual
  EGₛ' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  head (EGₛ' props) = EG' props
  tail (EGₛ' props) = EGₛ (tail props)

  EGₛ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  inF (EGₛ props) = fmap EGₛ' (inF props)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module IPL where

  data _∧_ (P : Set) (Q : Set) : Set where
    ∧-intro : P → Q → (P ∧ Q)

  _⇔_ : (P : Set) → (Q : Set) → Set
  a ⇔ b = (a → b) ∧ (b → a)

  proof₁ : {P Q : Set} → (P ∧ Q) → P
  proof₁ (∧-intro p q) = p

  proof₂ : {P Q : Set} → (P ∧ Q) → Q
  proof₂ (∧-intro p q) = q

  ∧-assoc₁ : { P Q R : Set } → ((P ∧ Q) ∧ R) → (P ∧ (Q ∧ R))
  ∧-assoc₁ (∧-intro (∧-intro p q) r) = ∧-intro p (∧-intro q r)

  ∧-assoc₂ : { P Q R : Set } → (P ∧ (Q ∧ R)) → ((P ∧ Q) ∧ R)
  ∧-assoc₂ (∧-intro p (∧-intro q r)) = ∧-intro (∧-intro p q) r

  ∧-assoc : { P Q R : Set } → ((P ∧ Q) ∧ R) ⇔  (P ∧ (Q ∧ R))
  ∧-assoc = ∧-intro ∧-assoc₁ ∧-assoc₂

  data _∨_ (P Q : Set) : Set where
   ∨-intro₁ : P → P ∨ Q
   ∨-intro₂ : Q → P ∨ Q

  ∨-elim : {A B C : Set} → (A → C) → (B → C) → (A ∨ B) → C
  ∨-elim ac bc (∨-intro₁ a) = ac a
  ∨-elim ac bc (∨-intro₂ b) = bc b

  ∨-comm′ : {P Q : Set} → (P ∨ Q) → (Q ∨ P)
  ∨-comm′ (∨-intro₁ p) = ∨-intro₂ p
  ∨-comm′ (∨-intro₂ q) = ∨-intro₁ q

  ∨-comm : {P Q : Set} → (P ∨ Q) ⇔ (Q ∨ P)
  ∨-comm = ∧-intro ∨-comm′ ∨-comm′

  ∨-assoc : { P Q R : Set } → ((P ∨ Q) ∨ R) → (P ∨ (Q ∨ R))
  ∨-assoc (∨-intro₁ (∨-intro₁ p)) = ∨-intro₁ p
  ∨-assoc (∨-intro₁ (∨-intro₂ q)) = ∨-intro₂ (∨-intro₁ q)
  ∨-assoc (∨-intro₂ r) = ∨-intro₂ (∨-intro₂ r)

  data ⊥ : Set where

  ¬ : Set → Set
  ¬ A = A → ⊥


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

open import Base
open import Homotopy.Connected

{-
  An example of using the overkilling covering space library.
-}

module Homotopy.Cover.ExamplePi1Circle where

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation
  open import Spaces.Circle

  {-
      The 1st step: Show that the circle is connected.
  -}
  S¹-is-conn : is-connected ⟨0⟩ S¹
  S¹-is-conn = proj base ,
    τ-extend ⦃ λ _ → ≡-is-set $ π₀-is-set S¹ ⦄
      (S¹-rec (λ x → proj x ≡ proj base) refl
        (prop-has-all-paths (π₀-is-set S¹ _ _) _ _))

  open import Integers
  open import Homotopy.Pointed
  open import Homotopy.Cover.Def S¹
  open import Homotopy.Cover.HomotopyGroupSetIsomorphism (⋆[ S¹ , base ]) S¹-is-conn

  S¹-covering : covering
  S¹-covering = let fiber = S¹-rec-nondep Set ℤ (eq-to-path succ-equiv) in
    cov[ fiber , S¹-rec (is-set ◯ fiber) ℤ-is-set (prop-has-all-paths is-set-is-prop _ _) ]

  open covering S¹-covering

  {-
      The 2nd step : Show that S¹ is contractible.
  -}

  -- One step.
  trans-fiber-!loop : ∀ z → transport fiber (! loop) z ≡ pred z
  trans-fiber-!loop z =
    transport fiber (! loop) z
      ≡⟨ ! $ trans-ap (id _) fiber (! loop) z ⟩
    transport (id _) (ap fiber (! loop)) z
      ≡⟨ ap (λ x → transport (id _) x z) $ ap-opposite fiber loop ⟩
    transport (id _) (! (ap fiber loop)) z
      ≡⟨ ap (λ x → transport (id _) (! x) z) $ S¹-β-loop-nondep Set ℤ (eq-to-path _) ⟩
    transport (id _) (! (eq-to-path succ-equiv)) z
      ≡⟨ trans-id-!eq-to-path _ _ ⟩∎
    pred z
      ∎

  -- The end of this function.  This can save some type annotations.
  loop⁻ⁿ-end : Σ S¹ fiber
  loop⁻ⁿ-end = (base , O)

  -- Climbing up the stairs.
  loop⁻¹ : ∀ z → _≡_ {A = Σ S¹ fiber} (base , z) (base , pred z)
  loop⁻¹ z = Σ-eq (! loop) (trans-fiber-!loop z)

  -- Agda needs us to show the induction order explicitly,
  -- and so there are so many functions.
  loop⁻ⁿ : ∀ z → (base , z) ≡ loop⁻ⁿ-end
  loop⁻ⁿ-pos : ∀ n → (base , pos n) ≡ loop⁻ⁿ-end
  loop⁻ⁿ-neg : ∀ n → (base , neg n) ≡ loop⁻ⁿ-end

  loop⁻ⁿ O = refl
  loop⁻ⁿ (pos _) = loop⁻ⁿ-pos _
  loop⁻ⁿ (neg _) = loop⁻ⁿ-neg _
  loop⁻ⁿ-pos 0 = loop⁻¹ _
  loop⁻ⁿ-pos (S _) = loop⁻¹ _ ∘ loop⁻ⁿ-pos _
  loop⁻ⁿ-neg 0 = ! (loop⁻¹ _)
  loop⁻ⁿ-neg (S _) = ! (loop⁻¹ _) ∘ loop⁻ⁿ-neg _

  private
    -- These are specialized J rules that work for this development only.
    -- I am too lazy to generalize them.

    lemma₁ : ∀ {x₁ x₂} (q : x₁ ≡ x₂) (f : ∀ z → (x₁ , z) ≡ loop⁻ⁿ-end) (z : fiber x₂)
      → transport (λ s → ∀ z → (s , z) ≡ loop⁻ⁿ-end) q f z
      ≡ Σ-eq (! q) refl ∘ f (transport fiber (! q) z)
    lemma₁ refl f z = refl

    lemma₂ : ∀ {b₁} {b₂} (q : b₁ ≡ b₂) p
      → transport (λ z → (base , z) ≡ loop⁻ⁿ-end) (! q) p
      ≡ Σ-eq refl q ∘ p
    lemma₂ refl p = refl

    compose-Σ-eq : ∀ {a₁} {a₂} (p : a₁ ≡ a₂)
      {b₁ : fiber a₁} {b₂} (q : transport fiber p b₁ ≡ b₂)
      → Σ-eq {A = S¹} {P = fiber} p refl ∘ Σ-eq refl q ≡ Σ-eq p q
    compose-Σ-eq refl q = refl

    loop⁻¹-loop⁻ⁿ-pred : ∀ z → loop⁻¹ z ∘ loop⁻ⁿ (pred z) ≡ loop⁻ⁿ z
    loop⁻¹-loop⁻ⁿ-pred O = opposite-right-inverse (loop⁻¹ _)
    loop⁻¹-loop⁻ⁿ-pred (pos O) = refl-right-unit _
    loop⁻¹-loop⁻ⁿ-pred (pos (S _)) = refl
    loop⁻¹-loop⁻ⁿ-pred (neg _) =
      loop⁻¹ _ ∘ (! (loop⁻¹ _) ∘ loop⁻ⁿ-neg _)
        ≡⟨ ! $ concat-assoc (loop⁻¹ _) (! (loop⁻¹ _)) _ ⟩
      (loop⁻¹ _ ∘ ! (loop⁻¹ _)) ∘ loop⁻ⁿ-neg _
        ≡⟨ ap (λ x → x ∘ loop⁻ⁿ-neg _) $ opposite-right-inverse (loop⁻¹ _) ⟩∎
      loop⁻ⁿ-neg _
        ∎

  path : ∀ x z → (x , z) ≡ loop⁻ⁿ-end
  path = S¹-rec (λ s → ∀ z → (s , z) ≡ loop⁻ⁿ-end) loop⁻ⁿ $ funext λ z →
    transport (λ s → ∀ z → (s , z) ≡ loop⁻ⁿ-end) loop loop⁻ⁿ z
        ≡⟨ lemma₁ loop loop⁻ⁿ z ⟩
    Σ-eq (! loop) refl ∘ loop⁻ⁿ (transport fiber (! loop) z)
        ≡⟨ ap (λ x → Σ-eq (! loop) refl ∘ x) $ apd! loop⁻ⁿ (trans-fiber-!loop z) ⟩
    Σ-eq (! loop) refl ∘
      (transport (λ z → (base , z) ≡ loop⁻ⁿ-end) (! $ trans-fiber-!loop z) (loop⁻ⁿ (pred z)))
        ≡⟨ ap (λ x → Σ-eq (! loop) refl ∘ x) $ lemma₂ (trans-fiber-!loop z) (loop⁻ⁿ (pred z)) ⟩
    Σ-eq (! loop) refl ∘ (Σ-eq refl (trans-fiber-!loop z) ∘ loop⁻ⁿ (pred z))
        ≡⟨ ! $ concat-assoc (Σ-eq (! loop) refl) _ _ ⟩
    (Σ-eq (! loop) refl ∘ Σ-eq refl (trans-fiber-!loop z)) ∘ loop⁻ⁿ (pred z)
        ≡⟨ ap (λ x → x ∘ loop⁻ⁿ (pred z)) $ compose-Σ-eq (! loop) (trans-fiber-!loop z) ⟩
    loop⁻¹ z ∘ loop⁻ⁿ (pred z)
        ≡⟨ loop⁻¹-loop⁻ⁿ-pred z ⟩∎
    loop⁻ⁿ z
        ∎

  S¹-covering-is-universal : is-universal S¹-covering
  S¹-covering-is-universal = contr-is-connected ⟨1⟩ $ loop⁻ⁿ-end , uncurry path

  ℤ-π¹S¹-equiv : ℤ ≃ (base ≡₀ base)
  ℤ-π¹S¹-equiv = GiveMeAPoint.fiber-a≃fg S¹-covering S¹-covering-is-universal O

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- The NO_POSITIVITY_CHECK pragma can only precede a mutual block or a
-- data/record definition.

module Issue1614c where

{-# NO_POSITIVITY_CHECK #-}
postulate Foo : Set


text:
module Properties where

import Properties.Dec

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
------------------------------------------------------------------------------
-- The alternating bit protocol (ABP)
------------------------------------------------------------------------------

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

-- This module define the ABP following the presentation in Dybjer and
-- Sander (1989).

module FOTC.Program.ABP.ABP where

open import FOTC.Base
open import FOTC.Base.Loop
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Stream.Type
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- ABP equations

postulate
  send ack out corrupt : D → D
  await                : D → D → D → D → D

postulate send-eq : ∀ b i is ds →
                    send b · (i ∷ is) · ds ≡ < i , b > ∷ await b i is ds
{-# ATP axioms send-eq #-}

postulate
  await-ok≡ : ∀ b b' i is ds →
              b ≡ b' →
              await b i is (ok b' ∷ ds) ≡ send (not b) · is · ds

  await-ok≢ : ∀ b b' i is ds →
              b ≢ b' →
              await b i is (ok b' ∷ ds) ≡ < i , b > ∷ await b i is ds

  await-error : ∀ b i is ds →
                await b i is (error ∷ ds) ≡ < i , b > ∷ await b i is ds
{-# ATP axioms await-ok≡ await-ok≢ await-error #-}

postulate
  ack-ok≡ : ∀ b b' i bs →
            b ≡ b' →
            ack b · (ok < i , b' > ∷ bs) ≡ b ∷ ack (not b) · bs

  ack-ok≢ : ∀ b b' i bs →
            b ≢ b' →
            ack b · (ok < i , b' > ∷ bs) ≡ not b ∷ ack b · bs

  ack-error : ∀ b bs → ack b · (error ∷ bs) ≡ not b ∷ ack b · bs
{-# ATP axioms ack-ok≡ ack-ok≢ ack-error #-}

postulate
  out-ok≡ : ∀ b b' i bs →
            b ≡ b' →
            out b · (ok < i , b' > ∷ bs) ≡ i ∷ out (not b) · bs

  out-ok≢ : ∀ b b' i bs →
            b ≢ b' →
            out b · (ok < i , b' > ∷ bs) ≡ out b · bs

  out-error : ∀ b bs → out b · (error ∷ bs) ≡ out b · bs
{-# ATP axioms out-ok≡ out-ok≢ out-error #-}

postulate
  corrupt-T : ∀ os x xs →
              corrupt (T ∷ os) · (x ∷ xs) ≡ ok x ∷ corrupt os · xs
  corrupt-F : ∀ os x xs →
              corrupt (F ∷ os) · (x ∷ xs) ≡ error ∷ corrupt os · xs
{-# ATP axioms corrupt-T corrupt-F #-}

postulate has hbs hcs hds : D → D → D → D → D → D → D

postulate has-eq : ∀ f₁ f₂ f₃ g₁ g₂ is →
                   has f₁ f₂ f₃ g₁ g₂ is ≡ f₁ · is · (hds f₁ f₂ f₃ g₁ g₂ is)
{-# ATP axioms has-eq #-}

postulate hbs-eq : ∀ f₁ f₂ f₃ g₁ g₂ is →
                   hbs f₁ f₂ f₃ g₁ g₂ is ≡ g₁ · (has f₁ f₂ f₃ g₁ g₂ is)
{-# ATP axioms hbs-eq #-}

postulate hcs-eq : ∀ f₁ f₂ f₃ g₁ g₂ is →
                   hcs f₁ f₂ f₃ g₁ g₂ is ≡ f₂ · (hbs f₁ f₂ f₃ g₁ g₂ is)
{-# ATP axioms hcs-eq #-}

postulate hds-eq : ∀ f₁ f₂ f₃ g₁ g₂ is →
                   hds f₁ f₂ f₃ g₁ g₂ is ≡ g₂ · (hcs f₁ f₂ f₃ g₁ g₂ is)
{-# ATP axioms hds-eq #-}

postulate
  transfer    : D → D → D → D → D → D → D
  transfer-eq : ∀ f₁ f₂ f₃ g₁ g₂ is →
                transfer f₁ f₂ f₃ g₁ g₂ is ≡ f₃ · (hbs f₁ f₂ f₃ g₁ g₂ is)
{-# ATP axioms transfer-eq #-}

postulate
  abpTransfer : D → D → D → D → D
  abpTransfer-eq :
    ∀ b os₁ os₂ is →
      abpTransfer b os₁ os₂ is ≡
        transfer (send b) (ack b) (out b) (corrupt os₁) (corrupt os₂) is
{-# ATP axiom abpTransfer-eq #-}

------------------------------------------------------------------------------
-- ABP relations

-- Start state for the ABP.
S : D → D → D → D → D → D → D → D → D → Set
S b is os₁ os₂ as bs cs ds js =
  as ≡ send b · is · ds
  ∧ bs ≡ corrupt os₁ · as
  ∧ cs ≡ ack b · bs
  ∧ ds ≡ corrupt os₂ · cs
  ∧ js ≡ out b · bs
{-# ATP definition S #-}

-- Auxiliary state for the ABP.
S' : D → D → D → D → D → D → D → D → D → D → Set
S' b i' is' os₁' os₂' as' bs' cs' ds' js' =
  as' ≡ await b i' is' ds'  -- Typo in ds'.
  ∧ bs' ≡ corrupt os₁' · as'
  ∧ cs' ≡ ack (not b) · bs'
  ∧ ds' ≡ corrupt os₂' · (b ∷ cs')
  ∧ js' ≡ out (not b) · bs'
{-# ATP definition S' #-}

-- Auxiliary bisimulation.
B : D → D → Set
B is js = ∃[ b ] ∃[ os₁ ] ∃[ os₂ ] ∃[ as ] ∃[ bs ] ∃[ cs ] ∃[ ds ]
            Stream is
            ∧ Bit b
            ∧ Fair os₁
            ∧ Fair os₂
            ∧ S b is os₁ os₂ as bs cs ds js
{-# ATP definition B #-}

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module HasDecidableSatisfaction where

open import OscarPrelude
open import 𝓐ssertion
open import HasSatisfaction
open import Interpretation

record HasDecidableSatisfaction (A : Set) ⦃ _ : 𝓐ssertion A ⦄ ⦃ _ : HasSatisfaction A ⦄ : Set₁
 where
  field
    _⊨?_ : (I : Interpretation) → (x : A) → Dec (I ⊨ x)

open HasDecidableSatisfaction ⦃ … ⦄ public

{-# DISPLAY HasDecidableSatisfaction._⊨?_ _ = _⊨?_ #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lifting of two predicates
------------------------------------------------------------------------

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

module Data.Product.Relation.Unary.All where

open import Level
open import Data.Product
open import Function.Base
open import Relation.Unary

private
  variable
    a b p q : Level
    A : Set a
    B : Set b

All : (A → Set p) → (B → Set q) → (A × B → Set (p ⊔ q))
All P Q (a , b) = P a × Q b


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

module Categories.Adjoint.TwoSided where

-- A "two sided" adjoint is an adjoint of two functors L and R where the
-- unit and counit are natural isomorphisms.

-- A two sided adjoint is the underlying data to an Adjoint Equivalence
open import Level

open import Categories.Adjoint
open import Categories.Category.Core using (Category)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_; NaturalIsomorphism)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e    : Level
    o′ ℓ′ e′ : Level
    C D      : Category o ℓ e

infix 5 _⊣⊢_

record _⊣⊢_ (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
  field
    unit   : idF ≃ (R ∘F L)
    counit : (L ∘F R) ≃ idF

  module unit   = NaturalIsomorphism unit
  module counit = NaturalIsomorphism counit

  private
    module C = Category C using (Obj; id; _∘_; _≈_; module HomReasoning)
    module D = Category D using (Obj; id; _∘_; _≈_; module HomReasoning)
    module L = Functor L using (₀; ₁; op; identity)
    module R = Functor R using (₀; ₁; op; identity)

  field
    zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id
    zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id

  op₁ : R.op ⊣⊢ L.op
  op₁ = record
    { unit   = counit.op
    ; counit = unit.op
    ; zig    = zag
    ; zag    = zig
    }

  zag⁻¹ : {B : D.Obj} → unit.⇐.η (R.₀ B) C.∘ R.₁ (counit.⇐.η B) C.≈ C.id
  zag⁻¹ {B} = begin
    unit.⇐.η (R.₀ B) C.∘ R.₁ (counit.⇐.η B)   ≈˘⟨ flip-fromʳ unit.FX≅GX zag ⟩∘⟨refl ⟩
    R.₁ (counit.⇒.η B) C.∘ R.₁ (counit.⇐.η B) ≈⟨ [ R ]-resp-∘ (counit.iso.isoʳ B) ⟩
    R.₁ D.id                                  ≈⟨ R.identity ⟩
    C.id                                      ∎
    where open C.HomReasoning
          open MR C

  zig⁻¹ : {A : C.Obj} → L.₁ (unit.⇐.η A) D.∘ counit.⇐.η (L.₀ A) D.≈ D.id
  zig⁻¹ {A} = begin
      L.₁ (unit.⇐.η A) D.∘ counit.⇐.η (L.₀ A) ≈˘⟨ refl⟩∘⟨ flip-fromˡ counit.FX≅GX zig ⟩
      L.₁ (unit.⇐.η A) D.∘ L.₁ (unit.⇒.η A)   ≈⟨ [ L ]-resp-∘ (unit.iso.isoˡ A) ⟩
      L.₁ C.id                                ≈⟨ L.identity ⟩
      D.id                                    ∎
      where open D.HomReasoning
            open MR D

  op₂ : R ⊣⊢ L
  op₂ = record
    { unit   = ≃.sym counit
    ; counit = ≃.sym unit
    ; zig    = zag⁻¹
    ; zag    = zig⁻¹
    }

  L⊣R : L ⊣ R
  L⊣R = record
    { unit   = unit.F⇒G
    ; counit = counit.F⇒G
    ; zig    = zig
    ; zag    = zag
    }

  module L⊣R = Adjoint L⊣R
  open L⊣R hiding (unit; counit; zig; zag; op) public

  R⊣L : R ⊣ L
  R⊣L = record
    { unit   = counit.F⇐G
    ; counit = unit.F⇐G
    ; zig    = zag⁻¹
    ; zag    = zig⁻¹
    }

  module R⊣L = Adjoint R⊣L

private

  record WithZig (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
    field
      unit   : idF ≃ (R ∘F L)
      counit : (L ∘F R) ≃ idF

    private
      module unit   = NaturalIsomorphism unit
      module counit = NaturalIsomorphism counit
      module C = Category C using (Obj; id; _∘_; _≈_; module HomReasoning)
      module D = Category D using (Obj; id; _∘_; _≈_; module HomReasoning)
      module L = Functor L using (₀; ₁; op; identity)
      module R = Functor R using (₀; ₁; op; identity; F-resp-≈)

    field
      zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id

    zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id
    zag {B} = F≃id⇒id (≃.sym unit) helper
      where open C
            open HomReasoning
            helper : R.₁ (L.₁ (R.₁ (counit.⇒.η B) ∘ unit.⇒.η (R.₀ B))) ≈ id
            helper = begin
              R.₁ (L.₁ (R.₁ (counit.⇒.η B) ∘ unit.⇒.η (R.₀ B)))             ≈⟨ Functor.homomorphism (R ∘F L) ⟩
              R.₁ (L.₁ (R.₁ (counit.⇒.η B))) ∘ R.₁ (L.₁ (unit.⇒.η (R.₀ B))) ≈˘⟨ R.F-resp-≈ (F≃id-comm₁ counit) ⟩∘⟨refl ⟩
              R.₁ (counit.⇒.η (L.₀ (R.₀ B))) ∘ R.₁ (L.₁ (unit.⇒.η (R.₀ B))) ≈⟨ [ R ]-resp-∘ zig ⟩
              R.₁ D.id                                                      ≈⟨ R.identity ⟩
              id                                                            ∎

  record WithZag (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
    field
      unit   : idF ≃ (R ∘F L)
      counit : (L ∘F R) ≃ idF

    private
      module unit   = NaturalIsomorphism unit
      module counit = NaturalIsomorphism counit
      module C = Category C using (Obj; id; _∘_; _≈_; module HomReasoning)
      module D = Category D using (Obj; id; _∘_; _≈_; module HomReasoning)
      module L = Functor L using (₀; ₁; op; identity; F-resp-≈)
      module R = Functor R using (₀; ₁; op; identity)

    field
      zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id

    zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id
    zig {A} = F≃id⇒id counit helper
      where open D
            open HomReasoning
            helper : L.₁ (R.₁ (counit.⇒.η (L.₀ A) ∘ L.₁ (unit.⇒.η A))) ≈ id
            helper = begin
              L.₁ (R.₁ (counit.⇒.η (L.₀ A) ∘ L.₁ (unit.⇒.η A)))               ≈⟨ Functor.homomorphism (L ∘F R) ⟩
              (L.₁ (R.₁ (counit.⇒.η (L.₀ A))) ∘ L.₁ (R.₁ (L.₁ (unit.⇒.η A)))) ≈˘⟨ refl⟩∘⟨ L.F-resp-≈ (F≃id-comm₂ (≃.sym unit)) ⟩
              L.₁ (R.₁ (counit.⇒.η (L.₀ A))) ∘ L.₁ (unit.⇒.η (R.₀ (L.₀ A)))   ≈⟨ [ L ]-resp-∘ zag ⟩
              L.₁ C.id                                                       ≈⟨ L.identity ⟩
              id                                                              ∎

module _ {L : Functor C D} {R : Functor D C} where

  withZig : WithZig L R → L ⊣⊢ R
  withZig LR = record
    { unit   = unit
    ; counit = counit
    ; zig    = zig
    ; zag    = zag
    }
    where open WithZig LR

  withZag : WithZag L R → L ⊣⊢ R
  withZag LR = record
    { unit   = unit
    ; counit = counit
    ; zig    = zig
    ; zag    = zag
    }
    where open WithZag LR

id⊣⊢id : idF {C = C} ⊣⊢ idF
id⊣⊢id {C = C} = record
  { unit   = ≃.sym ≃.unitor²
  ; counit = ≃.unitor²
  ; zig    = identity²
  ; zag    = identity²
  }
  where open Category C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Consensus.Types

module LibraBFT.Impl.Crypto.Crypto.Hash where

postulate -- TODO-1: valueZero
  valueZero : HashValue


text:
-- Andreas, 2014-09-01 restored this test case

module ClashingImport where

postulate A : Set

import Imports.A
open Imports.A public

-- only a public import creates a clash
-- since an ambiguous identifier would be exported

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Types.IND1 where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Product

open import Function

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

open import Types.Direction
open import Auxiliary.Extensionality
open import Auxiliary.RewriteLemmas

private
  variable
    m n : ℕ

----------------------------------------------------------------------
-- session type inductively with explicit rec
-- without polarized variables

mutual
  data Type n : Set where
    TUnit TInt : Type n
    TPair : (T₁ : Type n) (T₂ : Type n) → Type n
    TChan : (S : SType n) → Type n

  data SType n : Set where
    gdd : (G : GType n) → SType n
    rec : (G : GType (suc n) ) → SType n
    var : (x : Fin n) → SType n

  data GType n : Set where
    transmit : (d : Dir) (T : Type n) (S : SType n) → GType n
    choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
    end : GType n

TType = Type

-- weakening

weakenS : (n : ℕ) → SType m → SType (m + n)
weakenG : (n : ℕ) → GType m → GType (m + n)
weakenT : (n : ℕ) → TType m → TType (m + n)

weakenS n (gdd gst) = gdd (weakenG n gst)
weakenS n (rec gst) = rec (weakenG n gst)
weakenS n (var x) = var (inject+ n x)

weakenG n (transmit d t s) = transmit d (weakenT n t) (weakenS n s)
weakenG n (choice d m alt) = choice d m (weakenS n ∘ alt)
weakenG n end = end

weakenT n TUnit = TUnit
weakenT n TInt = TInt
weakenT n (TPair ty ty₁) = TPair (weakenT n ty) (weakenT n ty₁)
weakenT n (TChan x) = TChan (weakenS n x)

weaken1 : SType m → SType (suc m)
weaken1{m} stm with weakenS 1 stm
... | r rewrite n+1=suc-n {m} = r

module CheckWeaken where
  s0 : SType 0
  s0 = rec (transmit SND TUnit (var zero))
  s1 : SType 1
  s1 = rec (transmit SND TUnit (var zero))
  s2 : SType 2
  s2 = rec (transmit SND TUnit (var zero))

  check-weakenS1 : weakenS 1 s0 ≡ s1
  check-weakenS1 = cong rec (cong (transmit SND TUnit) refl)

  check-weakenS2 : weakenS 2 s0 ≡ s2
  check-weakenS2 = cong rec (cong (transmit SND TUnit) refl)

weaken1'N : Fin (suc n) → Fin n → Fin (suc n)
weaken1'N zero x = suc x
weaken1'N (suc i) zero = zero
weaken1'N (suc i) (suc x) = suc (weaken1'N i x)

weaken1'S : Fin (suc n) → SType n → SType (suc n)
weaken1'G : Fin (suc n) → GType n → GType (suc n)
weaken1'T : Fin (suc n) → TType n → TType (suc n)

weaken1'S i (gdd gst) = gdd (weaken1'G i gst)
weaken1'S i (rec gst) = rec (weaken1'G (suc i) gst)
weaken1'S i (var x) = var (weaken1'N i x)

weaken1'G i (transmit d t s) = transmit d (weaken1'T i t) (weaken1'S i s)
weaken1'G i (choice d m alt) = choice d m (weaken1'S i ∘ alt)
weaken1'G i end = end

weaken1'T i TUnit = TUnit
weaken1'T i TInt = TInt
weaken1'T i (TPair t₁ t₂) = TPair (weaken1'T i t₁) (weaken1'T i t₂)
weaken1'T i (TChan x) = TChan (weaken1'S i x)

weaken1S : SType n → SType (suc n)
weaken1G : GType n → GType (suc n)
weaken1T : Type n → Type (suc n)

weaken1S = weaken1'S zero
weaken1G = weaken1'G zero
weaken1T = weaken1'T zero

module CheckWeaken1' where
  sxy : ∀ n → Fin (suc n) → SType n
  sxy n x = rec (transmit SND TUnit (var x))

  s00 : SType 0
  s00 = sxy 0 zero
  s10 : SType 1
  s10 = sxy 1 zero
  s11 : SType 1
  s11 = sxy 1 (suc zero)
  s22 : SType 2
  s22 = sxy 2 (suc (suc zero))

  check-weaken-s01 : weaken1'S zero s00 ≡ s10
  check-weaken-s01 = refl

  check-weaken-s1-s2 : weaken1'S zero s11 ≡ s22
  check-weaken-s1-s2 = refl

  check-weaken-s21 : weaken1'S (suc zero) (sxy 2 (suc zero)) ≡ sxy 3 (suc zero)
  check-weaken-s21 = refl
--------------------------------------------------------------------

weak-weakN : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (x : Fin n)
  → weaken1'N (suc i) (weaken1'N j x) ≡ weaken1'N (inject₁ j) (weaken1'N i x)
weak-weakG : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (g : GType n)
  → weaken1'G (suc i) (weaken1'G j g) ≡ weaken1'G (inject₁ j) (weaken1'G i g)
weak-weakS : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s : SType n)
  → weaken1'S (suc i) (weaken1'S j s) ≡ weaken1'S (inject₁ j) (weaken1'S i s)
weak-weakT : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (t : Type n)
  → weaken1'T (suc i) (weaken1'T j t) ≡ weaken1'T (inject₁ j) (weaken1'T i t)

weak-weakN zero zero le x                              = refl
weak-weakN (suc i) zero le x                         = refl
weak-weakN (suc i) (suc j) (s≤s le) zero           = refl
weak-weakN{suc n} (suc i) (suc j) (s≤s le) (suc x) = cong suc (weak-weakN i j le x)

weak-weakG i j le (transmit d t s) = cong₂ (transmit d) (weak-weakT i j le t) (weak-weakS i j le s)
weak-weakG i j le (choice d m alt) = cong (choice d m) (ext (weak-weakS i j le ∘ alt))
weak-weakG i j le end              = refl

weak-weakS i j le (gdd gst) = cong gdd (weak-weakG i j le gst)
weak-weakS i j le (rec gst) = cong rec (weak-weakG (suc i) (suc j) (s≤s le) gst)
weak-weakS i j le (var x) = cong (var) (weak-weakN i j le x)

weak-weakT i j le TUnit        = refl
weak-weakT i j le TInt         = refl
weak-weakT i j le (TPair t t₁) = cong₂ TPair (weak-weakT i j le t) (weak-weakT i j le t₁)
weak-weakT i j le (TChan s)    = cong TChan (weak-weakS i j le s)

weaken1-weakenN : (m : ℕ) (j : Fin (suc n)) (x : Fin n)
  → inject+ m (weaken1'N j x) ≡ weaken1'N (inject+ m j) (inject+ m x)
weaken1-weakenN m zero zero           = refl
weaken1-weakenN m zero (suc x)      = refl
weaken1-weakenN m (suc j) zero      = refl
weaken1-weakenN m (suc j) (suc x) = cong suc (weaken1-weakenN m j x)

weaken1-weakenS : (m : ℕ) (j : Fin (suc n)) (s : SType n)
  → weakenS m (weaken1'S j s) ≡ weaken1'S (inject+ m j) (weakenS m s)
weaken1-weakenG : (m : ℕ) (j : Fin (suc n)) (g : GType n)
  → weakenG m (weaken1'G j g) ≡ weaken1'G (inject+ m j) (weakenG m g)
weaken1-weakenT : (m : ℕ) (j : Fin (suc n)) (t : Type n)
  → weakenT m (weaken1'T j t) ≡ weaken1'T (inject+ m j) (weakenT m t)
weaken1-weakenS m j (gdd gst) = cong gdd (weaken1-weakenG m j gst)
weaken1-weakenS m j (rec gst) = cong rec (weaken1-weakenG m (suc j) gst)
weaken1-weakenS m zero (var zero)      = refl
weaken1-weakenS m zero (var (suc x)) = refl
weaken1-weakenS {suc n} m (suc j) (var zero)      = refl
weaken1-weakenS {suc n} m (suc j) (var (suc x)) = cong (var) (cong suc (weaken1-weakenN m j x))

weaken1-weakenG m j (transmit d t s)  = cong₂ (transmit d) (weaken1-weakenT m j t) (weaken1-weakenS m j s)
weaken1-weakenG m j (choice d m₁ alt) = cong (choice d m₁) (ext (weaken1-weakenS m j ∘ alt))
weaken1-weakenG m j end = refl

weaken1-weakenT m j TUnit = refl
weaken1-weakenT m j TInt = refl
weaken1-weakenT m j (TPair t t₁) = cong₂ TPair (weaken1-weakenT m j t) (weaken1-weakenT m j t₁)
weaken1-weakenT m j (TChan x) = cong TChan (weaken1-weakenS m j x)

--------------------------------------------------------------------
-- substitution

st-substS : SType (suc n) → Fin (suc n) → SType 0 → SType n
st-substG : GType (suc n) → Fin (suc n) → SType 0 → GType n
st-substT : Type (suc n) → Fin (suc n) → SType 0 → Type n

st-substS (gdd gst) i st0 = gdd (st-substG gst i st0)
st-substS (rec gst) i st0 = rec (st-substG gst (suc i) st0)
st-substS {n} (var zero) zero st0 = weakenS n st0
st-substS {suc n} (var zero) (suc i) st0 = var zero
st-substS {suc n} (var (suc x)) zero st0 = var x
st-substS {suc n} (var (suc x)) (suc i) st0 = weaken1S (st-substS (var x) i st0)

st-substG (transmit d t s) i st0 = transmit d (st-substT t i st0) (st-substS s i st0)
st-substG (choice d m alt) i st0 = choice d m (λ j → st-substS (alt j) i st0)
st-substG end i st0 = end

st-substT TUnit i st0 = TUnit
st-substT TInt i st0 = TInt
st-substT (TPair ty ty₁) i st0 = TPair (st-substT ty i st0) (st-substT ty₁ i st0)
st-substT (TChan st) i st0 = TChan (st-substS st i st0)

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

trivial-subst-var : (x : Fin n) (ist₁ ist₂ : SType 0)
  → st-substS (var (suc x)) zero ist₁ ≡ st-substS (var (suc x)) zero ist₂
trivial-subst-var zero ist1 ist2 = refl
trivial-subst-var (suc x) ist1 ist2 = refl

trivial-subst-var' : (i : Fin n) (ist₁ ist₂ : SType 0)
  → st-substS (var zero) (suc i) ist₁ ≡ st-substS (var zero) (suc i) ist₂
trivial-subst-var' zero ist1 ist2 = refl
trivial-subst-var' (suc x) ist1 ist2 = refl

--------------------------------------------------------------------
-- equivalence
variable
  t t₁ t₂ t₁' t₂' : Type n
  s s₁ s₂ : SType n
  g g₁ g₂ : GType n

unfold : SType 0 → GType 0
unfold (gdd gst) = gst
unfold (rec gst) = st-substG gst zero (rec gst)

-- type equivalence
data EquivT (R : SType n → SType n → Set) : Type n → Type n → Set where
  eq-unit : EquivT R TUnit TUnit
  eq-int  : EquivT R TInt TInt
  eq-pair : EquivT R t₁ t₁' → EquivT R t₂ t₂' → EquivT R (TPair t₁ t₂) (TPair t₁' t₂')
  eq-chan : R s₁ s₂ → EquivT R (TChan s₁) (TChan s₂)

-- session type equivalence
data EquivG (R : SType n → SType n → Set) : GType n → GType n → Set where
  eq-transmit : (d : Dir) → EquivT R t₁ t₂ → R s₁ s₂ → EquivG R (transmit d t₁ s₁) (transmit d t₂ s₂)
  eq-choice : ∀ {alt alt'} → (d : Dir) → ((i : Fin m) → R (alt i) (alt' i)) → EquivG R (choice d m alt) (choice d m alt')
  eq-end : EquivG R end end

record Equiv (s₁ s₂ : SType 0) : Set where
  coinductive
  field force : EquivG Equiv (unfold s₁) (unfold s₂)

open Equiv

_≈_ = Equiv
_≈'_ = EquivG Equiv
_≈ᵗ_ = EquivT Equiv

-- reflexive

≈-refl : s ≈ s
≈'-refl : g ≈' g
≈ᵗ-refl : t ≈ᵗ t

force (≈-refl {s}) = ≈'-refl

≈'-refl {transmit d t s} = eq-transmit d ≈ᵗ-refl ≈-refl
≈'-refl {choice d m alt} = eq-choice d (λ i → ≈-refl)
≈'-refl {end} = eq-end

≈ᵗ-refl {TUnit} = eq-unit
≈ᵗ-refl {TInt} = eq-int
≈ᵗ-refl {TPair t t₁} = eq-pair ≈ᵗ-refl ≈ᵗ-refl
≈ᵗ-refl {TChan x} = eq-chan ≈-refl

-- symmetric

≈-symm : s₁ ≈ s₂ → s₂ ≈ s₁
≈'-symm : g₁ ≈' g₂ → g₂ ≈' g₁
≈ᵗ-symm : t₁ ≈ᵗ t₂ → t₂ ≈ᵗ t₁

force (≈-symm s₁≈s₂) = ≈'-symm (force s₁≈s₂)

≈'-symm (eq-transmit d x x₁) = eq-transmit d (≈ᵗ-symm x) (≈-symm x₁)
≈'-symm (eq-choice d x) = eq-choice d (≈-symm ∘ x)
≈'-symm eq-end = eq-end

≈ᵗ-symm eq-unit = eq-unit
≈ᵗ-symm eq-int = eq-int
≈ᵗ-symm (eq-pair t₁≈ᵗt₂ t₁≈ᵗt₃) = eq-pair (≈ᵗ-symm t₁≈ᵗt₂) (≈ᵗ-symm t₁≈ᵗt₃)
≈ᵗ-symm (eq-chan x) = eq-chan (≈-symm x)

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
open import Oscar.Prelude
open import Oscar.Data.¶
open import Oscar.Data.Fin
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Data.Maybe
open import Oscar.Data.Proposequality
open import Oscar.Data.Vec
open import Oscar.Class.Congruity
open import Oscar.Class.Thickandthin
open import Oscar.Class.Injectivity
open import Oscar.Class.Smap
open import Oscar.Class.Pure
open import Oscar.Class.Apply
import Oscar.Property.Monad.Maybe
import Oscar.Property.Thickandthin.FinFinProposequalityMaybeProposequality
import Oscar.Class.Surjection.⋆
import Oscar.Class.Congruity.Proposequality
import Oscar.Class.Injectivity.Vec
import Oscar.Class.Smap.ExtensionFinExtensionTerm

module Oscar.Property.Thickandthin.FinTermProposequalityMaybeProposequality where

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Substitunction 𝔓
  open Term 𝔓

  instance

    [𝓣hick]FinTerm : [𝓣hick] Fin Term
    [𝓣hick]FinTerm = ∁

    𝓣hickFinTerm : 𝓣hick Fin Term
    𝓣hickFinTerm .𝓣hick.thick x t = thick x ◃ t

    [𝓣hick]FinTerms : ∀ {N} → [𝓣hick] Fin (Terms N)
    [𝓣hick]FinTerms = ∁

    𝓣hickFinTerms : ∀ {N} → 𝓣hick Fin (Terms N)
    𝓣hickFinTerms .𝓣hick.thick x t = thick x ◃ t

    [𝓣hin]FinTerm : [𝓣hin] Fin Term
    [𝓣hin]FinTerm = ∁

    𝓣hinFinTerm : 𝓣hin Fin Term
    𝓣hinFinTerm .𝓣hin.thin = smap ∘ thin

    [𝓣hin]FinTerms : ∀ {N} → [𝓣hin] Fin (Terms N)
    [𝓣hin]FinTerms = ∁

    𝓣hinFinTerms : ∀ {N} → 𝓣hin Fin (Terms N)
    𝓣hinFinTerms .𝓣hin.thin = smap ∘ thin

    [𝓘njectivity₂,₁]FinTerm : ∀ {m} → [𝓘njectivity₂,₁] (𝔱hin Fin Term m) Proposequality Proposequality
    [𝓘njectivity₂,₁]FinTerm = ∁

    𝓘njection₂FinTerm : ∀ {m} → 𝓘njection₂ (λ (_ : ¶⟨< ↑ m ⟩) (_ : Term m) → Term (↑ m))
    𝓘njection₂FinTerm {m} .𝓘njection₂.injection₂ = thin

    [𝓘njectivity₂,₁]FinTerms : ∀ {N m} → [𝓘njectivity₂,₁] (𝔱hin Fin (Terms N) m) Proposequality Proposequality
    [𝓘njectivity₂,₁]FinTerms = ∁

    𝓘njection₂FinTerms : ∀ {N m} → 𝓘njection₂ (λ (_ : ¶⟨< ↑ m ⟩) (_ : Terms N m) → Terms N (↑ m))
    𝓘njection₂FinTerms {m} .𝓘njection₂.injection₂ = thin

    𝓘njection₁-TermI : ∀ {n} → 𝓘njection₁ (λ (_ : ¶⟨< n ⟩) → Term n)
    𝓘njection₁-TermI .𝓘njection₁.injection₁ = i

    [𝓘njectivity₁]TermI : ∀ {n} → [𝓘njectivity₁] (λ (_ : ¶⟨< n ⟩) → Term n) Proposequality Proposequality
    [𝓘njectivity₁]TermI = ∁

    𝓘njectivity₁TermI : ∀ {n} → 𝓘njectivity₁ (λ (_ : ¶⟨< n ⟩) → Term n) Proposequality Proposequality
    𝓘njectivity₁TermI {n} .𝓘njectivity₁.injectivity₁ ∅ = ∅

    𝓘njection₂-TermFork : ∀ {n} → 𝓘njection₂ (λ (_ : Term n) (_ : Term n) → Term n)
    𝓘njection₂-TermFork .𝓘njection₂.injection₂ = _fork_

    [𝓘njection₂,₀,₁]-TermFork : ∀ {n} → [𝓘njectivity₂,₀,₁] (λ (_ : Term n) (_ : Term n) → Term n) Proposequality Proposequality
    [𝓘njection₂,₀,₁]-TermFork = ∁

    𝓘njection₂,₀,₁-TermFork : ∀ {n} → 𝓘njectivity₂,₀,₁ (λ (_ : Term n) (_ : Term n) → Term n) Proposequality Proposequality
    𝓘njection₂,₀,₁-TermFork .𝓘njectivity₂,₀,₁.injectivity₂,₀,₁ ∅ = ∅

    [𝓘njection₂,₀,₂]-TermFork : ∀ {n} → [𝓘njectivity₂,₀,₂] (λ (_ : Term n) (_ : Term n) → Term n) Proposequality Proposequality
    [𝓘njection₂,₀,₂]-TermFork = ∁

    𝓘njection₂,₀,₂-TermFork : ∀ {n} → 𝓘njectivity₂,₀,₂ (λ (_ : Term n) (_ : Term n) → Term n) Proposequality Proposequality
    𝓘njection₂,₀,₂-TermFork .𝓘njectivity₂,₀,₂.injectivity₂,₀,₂ ∅ = ∅

    𝓘njection₃TermFunction : ∀ {n} → 𝓘njection₃ (λ (_ : 𝔓) (N : ¶) (_ : Terms N n) → Term n)
    𝓘njection₃TermFunction {n} .𝓘njection₃.injection₃ p N ts = function p ts

    [𝓘njectivity₃,₀,₁]TermFunction : ∀ {n} → [𝓘njectivity₃,₀,₁] (λ (_ : 𝔓) (N : ¶) (_ : Terms N n) → Term n) Proposequality Proposequality
    [𝓘njectivity₃,₀,₁]TermFunction = ∁

    𝓘njectivity₃,₀,₁TermFunction : ∀ {n} → 𝓘njectivity₃,₀,₁ (λ (_ : 𝔓) (N : ¶) (_ : Terms N n) → Term n) Proposequality Proposequality
    𝓘njectivity₃,₀,₁TermFunction .𝓘njectivity₃,₀,₁.injectivity₃,₀,₁ ∅ = ∅

    [𝓘njectivity₃,₀,₂]TermFunction : ∀ {n} → [𝓘njectivity₃,₀,₂] (λ (_ : 𝔓) (N : ¶) (_ : Terms N n) → Term n) Proposequality Proposequality
    [𝓘njectivity₃,₀,₂]TermFunction = ∁

    𝓘njectivity₃,₀,₂TermFunction : ∀ {n} → 𝓘njectivity₃,₀,₂ (λ (_ : 𝔓) (N : ¶) (_ : Terms N n) → Term n) Proposequality Proposequality
    𝓘njectivity₃,₀,₂TermFunction .𝓘njectivity₃,₀,₂.injectivity₃,₀,₂ ∅ = ∅

    𝓘njection₂TermFunction : ∀ {N n} → 𝓘njection₂ (λ (_ : 𝔓) (_ : Terms N n) → Term n)
    𝓘njection₂TermFunction {N} {n} .𝓘njection₂.injection₂ p ts = function p ts

    [𝓘njectivity₂,₀,₂]TermFunction : ∀ {N n} → [𝓘njectivity₂,₀,₂] (λ (_ : 𝔓) (_ : Terms N n) → Term n) Proposequality Proposequality
    [𝓘njectivity₂,₀,₂]TermFunction = ∁

    𝓘njectivity₂,₀,₂TermFunction : ∀ {N n} → 𝓘njectivity₂,₀,₂ (λ (_ : 𝔓) (_ : Terms N n) → Term n) Proposequality Proposequality
    𝓘njectivity₂,₀,₂TermFunction .𝓘njectivity₂,₀,₂.injectivity₂,₀,₂ ∅ = ∅

  mutual

    instance

      𝓘njectivity₂,₁FinTerm : ∀ {m} → 𝓘njectivity₂,₁ (𝔱hin Fin Term m) Proposequality Proposequality
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ x {i _} {i _} eq = congruity i (injectivity₂,₁ x (injectivity₁[ Proposequality ] eq))
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {i _} {leaf} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {i _} {_ fork _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {i _} {function _ _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {leaf} {i _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {leaf} {leaf} _ = ∅
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {leaf} {_ fork _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {leaf} {function _ _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {_ fork _} {i _} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {_ fork _} {leaf} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ x {y₁ fork y₂} {y₃ fork y₄} eq
        rewrite injectivity₂,₁ {_∼₂_ = Proposequality} x {y₁ = y₁} (injectivity₂,₀,₁[ Proposequality ] eq)
              | injectivity₂,₁ {_∼₂_ = Proposequality} x {y₁ = y₂} (injectivity₂,₀,₂[ Proposequality ] eq)
        = ∅
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {y₁ fork y₂} {function x₁ x₂} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {function _ _} {i x₃} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {function _ _} {leaf} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ _ {function _ _} {y₂ fork y₃} ()
      𝓘njectivity₂,₁FinTerm .𝓘njectivity₂,₁.injectivity₂,₁ x {function p1 {N1} ts1} {function p2 {N2} ts2} t₁≡t₂
        rewrite injectivity₃,₀,₁[ Proposequality ] {x₂ = p2} t₁≡t₂
        with injectivity₃,₀,₂[ Proposequality ] {y₂ = N2} t₁≡t₂
      … | ∅
        with injectivity₂,₀,₂[ Proposequality ] {y₂ = thin x ts2} t₁≡t₂
      … | ts₁≡ts₂ = congruity (function p2) (injectivity₂,₁ x ts₁≡ts₂)

      𝓘njectivity₂,₁FinTerms : ∀ {N m} → 𝓘njectivity₂,₁ (𝔱hin Fin (Terms N) m) Proposequality Proposequality
      𝓘njectivity₂,₁FinTerms .𝓘njectivity₂,₁.injectivity₂,₁ x {∅} {∅} x₁ = ∅
      𝓘njectivity₂,₁FinTerms .𝓘njectivity₂,₁.injectivity₂,₁ x {_ , _} {t₂ , ts₂} eq
        rewrite injectivity₂,₁ {_∼₂_ = Proposequality} x {y₂ = t₂} (injectivity₂,₀,₁[ Proposequality ] eq)
              | injectivity₂,₁ {_∼₂_ = Proposequality} x {y₂ = ts₂} (injectivity₂,₀,₂[ Proposequality ] eq)
        = ∅

  instance

    [𝓒heck]FinTermMaybe : [𝓒heck] Fin Term Maybe
    [𝓒heck]FinTermMaybe = ∁

    [𝓒heck]FinTermsMaybe : ∀ {N} → [𝓒heck] Fin (Terms N) Maybe
    [𝓒heck]FinTermsMaybe = ∁

  open import Oscar.Class.Smap
  open import Oscar.Class.Fmap

  mutual

    instance

      𝓒heckFinTermMaybe : 𝓒heck Fin Term Maybe
      𝓒heckFinTermMaybe .𝓒heck.check x (i y) = ⦇ i (check x y) ⦈
      𝓒heckFinTermMaybe .𝓒heck.check x leaf = ⦇ leaf ⦈
      𝓒heckFinTermMaybe .𝓒heck.check x (y₁ fork y₂) = ⦇ _fork_ (check x y₁) (check x y₂) ⦈
      𝓒heckFinTermMaybe .𝓒heck.check x (function p ts) = ⦇ (function p) (check x ts) ⦈

      𝓒heckFinTermsMaybe : ∀ {N} → 𝓒heck Fin (Terms N) Maybe
      𝓒heckFinTermsMaybe .𝓒heck.check _ ∅ = ⦇ ∅ ⦈
      𝓒heckFinTermsMaybe .𝓒heck.check x (t , ts) = ⦇ check x t , check x ts ⦈

  instance

    [𝓣hick/thin=1]FinTermProposequality : [𝓣hick/thin=1] Fin Term Proposequality
    [𝓣hick/thin=1]FinTermProposequality = ∁

    [𝓣hick/thin=1]FinTermsProposequality : ∀ {N} → [𝓣hick/thin=1] Fin (Terms N) Proposequality
    [𝓣hick/thin=1]FinTermsProposequality = ∁

  mutual

    instance

      𝓣hick/thin=1FinTermProposequality : 𝓣hick/thin=1 Fin Term Proposequality
      𝓣hick/thin=1FinTermProposequality .𝓣hick/thin=1.thick/thin=1 x (i y) rewrite thick/thin=1 {_≈_ = Proposequality} x y = ∅ -- congruity i $ thick/thin=1 x y
      𝓣hick/thin=1FinTermProposequality .𝓣hick/thin=1.thick/thin=1 x leaf = ∅
      𝓣hick/thin=1FinTermProposequality .𝓣hick/thin=1.thick/thin=1 x (y₁ fork y₂) = congruity₂ _fork_ (thick/thin=1 x y₁) (thick/thin=1 x y₂)
      𝓣hick/thin=1FinTermProposequality .𝓣hick/thin=1.thick/thin=1 x (function p ts) = congruity (function p) (thick/thin=1 x ts)

      𝓣hick/thin=1FinTermsProposequality : ∀ {N} → 𝓣hick/thin=1 Fin (Terms N) Proposequality
      𝓣hick/thin=1FinTermsProposequality .𝓣hick/thin=1.thick/thin=1 x ∅ = ∅
      𝓣hick/thin=1FinTermsProposequality .𝓣hick/thin=1.thick/thin=1 x (t , ts) = congruity₂ _,_ (thick/thin=1 x t) (thick/thin=1 x ts)

  instance

    [𝓒heck/thin=1]FinTermMaybe : [𝓒heck/thin=1] Fin Term Maybe Proposequality
    [𝓒heck/thin=1]FinTermMaybe = ∁

    [𝓒heck/thin=1]FinTermsMaybe : ∀ {N} → [𝓒heck/thin=1] Fin (Terms N) Maybe Proposequality
    [𝓒heck/thin=1]FinTermsMaybe = ∁

  mutual

    instance

      𝓒heck/thin=1FinTermMaybe : 𝓒heck/thin=1 Fin Term Maybe Proposequality
      𝓒heck/thin=1FinTermMaybe .𝓒heck/thin=1.check/thin=1 x (i y) rewrite check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x y = ∅
      𝓒heck/thin=1FinTermMaybe .𝓒heck/thin=1.check/thin=1 x leaf = ∅
      𝓒heck/thin=1FinTermMaybe .𝓒heck/thin=1.check/thin=1 x (y₁ fork y₂)
        rewrite check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x y₁
              | check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x y₂
        = ∅
      𝓒heck/thin=1FinTermMaybe .𝓒heck/thin=1.check/thin=1 x (function p ys) rewrite check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x ys = ∅

      𝓒heck/thin=1FinTermsMaybe : ∀ {N} → 𝓒heck/thin=1 Fin (Terms N) Maybe Proposequality
      𝓒heck/thin=1FinTermsMaybe .𝓒heck/thin=1.check/thin=1 x ∅ = ∅
      𝓒heck/thin=1FinTermsMaybe .𝓒heck/thin=1.check/thin=1 x (y , ys)
        rewrite check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x y
              | check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x ys
        = ∅

  instance

    IsThickandthinFinTerm : IsThickandthin Fin Term Proposequality Maybe Proposequality
    IsThickandthinFinTerm = ∁

    IsThickandthinFinTerms : ∀ {N} → IsThickandthin Fin (Terms N) Proposequality Maybe Proposequality
    IsThickandthinFinTerms = ∁

module _ {𝔭} (𝔓 : Ø 𝔭) where

  open Substitunction 𝔓
  open Term 𝔓

  ThickandthinFinTerm : Thickandthin _ _ _ _ _ _
  ThickandthinFinTerm = ∁ Fin Term Proposequality Maybe Proposequality

  ThickandthinFinTerms : ∀ N → Thickandthin _ _ _ _ _ _
  ThickandthinFinTerms N = ∁ Fin (Terms N) Proposequality Maybe Proposequality


text:
------------------------------------------------------------------------------
-- Proving properties without using pattern matching on refl
------------------------------------------------------------------------------

{-# OPTIONS --no-pattern-matching      #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}

module FOT.PA.Inductive2Standard.NoPatternMatchingOnRefl where

open import PA.Inductive.Base

------------------------------------------------------------------------------
-- From PA.Inductive2Standard

-- 20 May 2013. Requires the predecessor function.
-- PA₂ : ∀ {m n} → succ m ≡ succ n → m ≡ n


text:
module Syntax where

import Level
open import Data.Empty
open import Data.Unit as Unit
open import Data.Nat
open import Data.List as List renaming ([] to Ø; [_] to [_]L)
open import NonEmptyList as NList
open import Data.Vec as Vec hiding ([_]; _++_)
open import Data.Product as Prod
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

open import Common.Context as Context

open import Algebra
open Monoid {{ ... }} hiding (refl)

open import SyntaxRaw

infixr 5 _§ₒ_ _§ₘ_

-----------------------------------------
--- Separate types and terms
-----------------------------------------

mutual
  data DecentType : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → Raw Θ Γ₁ Γ₂ → Set where
    DT-⊤ : (Θ : TyCtx) (Γ : RawCtx) → DecentType (⊤-Raw Θ Γ)
    DT-tyVar : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ : RawCtx} →
               (X : TyVar Θ Γ₂) → DecentType (tyVarRaw Γ₁ X)
    DT-inst : ∀{Θ Γ₁ Γ₂ A} →
              (B : Raw Θ Γ₁ (Γ₂ ↑ A)) → (t : Raw Ø Γ₁ Ø) →
              DecentType B → DecentTerm t →
              DecentType (instRaw {Γ₂ = Γ₂} B t)
    DT-paramAbstr : ∀{Θ Γ₂} {B : U} (Γ₁ : RawCtx) →
                    {A : Raw Θ (B ∷ Γ₁) Γ₂} →
                    DecentType A →
                    DecentType (paramAbstrRaw Γ₁ A)
    DT-fp : ∀{Θ Γ₂} (Γ₁ : RawCtx) →
            (ρ : FP) → (D : FpData Raw Θ Γ₂) →
            DecentFpData D →
            DecentType (fpRaw Γ₁ ρ D)

  data DecentTerm : {Γ₁ Γ₂ : RawCtx} → Raw Ø Γ₁ Γ₂ → Set where
    DO-unit : (Γ : RawCtx) → DecentTerm (unitRaw Γ)
    DO-objVar : {Γ : RawCtx} {A : U} →
                (x : RawVar Γ A) → DecentTerm (objVarRaw x)
    DO-inst : {Γ₁ Γ₂ : RawCtx} {A : U} →
              (t : Raw Ø Γ₁ (Γ₂ ↑ A)) → (s : Raw Ø Γ₁ Ø) →
              DecentTerm t → DecentTerm s →
              DecentTerm (instRaw {Γ₂ = Γ₂} t s)
    DO-dialg : (Δ : RawCtx) (Γ : RawCtx) (A : U) →
               (ρ : FP) (k : ℕ) →
               DecentTerm (dialgRaw Δ Γ A ρ k)
    DO-mapping : (Γ : RawCtx) (Δ : RawCtx) →
                 (gs : FpMapData Raw Γ) → (ρ : FP) →
                 DecentFpMapData gs →
                 DecentTerm (recRaw Γ Δ gs ρ)

  DecentFpMapData : {Γ : RawCtx} → FpMapData Raw Γ → Set
  DecentFpMapData [ (Γ' , A , f , t) ] =
    DecentType A × DecentCtxMor f × DecentTerm t
  DecentFpMapData ((Γ' , A , f , t) ∷ ts) =
    DecentType A × DecentCtxMor f × DecentTerm t × DecentFpMapData ts

  DecentCtxMor : {Γ₁ Γ₂ : RawCtx} → CtxMor Raw Γ₁ Γ₂ → Set
  DecentCtxMor {Γ₂ = Ø}      []      = ⊤
  DecentCtxMor {Γ₂ = x ∷ Γ₂} (t ∷ f) = DecentTerm t × DecentCtxMor f

  DecentFpData : ∀{Θ Γ₂} → FpData Raw Θ Γ₂ → Set
  DecentFpData [ Γ , f , A ] = DecentCtxMor f × DecentType A
  DecentFpData ((Γ , f , A) ∷ D)
    = (DecentCtxMor f × DecentType A) × DecentFpData D

{-
DT-syntax : (Θ : TyCtx) (Γ₁ Γ₂ : RawCtx) → Raw Θ Γ₁ Γ₂ → Set
DT-syntax _ _ _ A = DecentType A

syntax DT-syntax Θ Γ₁ Γ₁ A = Θ ∥ Γ₁ ⊨ A ε Γ₂ ━

DO-syntax : (Γ₁ Γ₂ : RawCtx) → Raw Ø Γ₁ Γ₂ → Set
DO-syntax _ _ t = DecentTerm t

syntax DO-syntax Γ₁ Γ₂ t = Γ₁ ⊢ t ∈ Γ₂ ⊸?
-}

-------------------------------------
------- Pre-types and terms
-------------------------------------

PreType : (Θ : TyCtx) (Γ₁ Γ₂ : RawCtx) → Set
PreType Θ Γ₁ Γ₂ = Σ (Raw Θ Γ₁ Γ₂) λ A → DecentType A

_∣_/_⊸Ty = PreType

mkPreType : ∀ {Θ Γ₁ Γ₂} {A : Raw Θ Γ₁ Γ₂} → DecentType A → PreType Θ Γ₁ Γ₂
mkPreType {A = A} p = (A , p)

PreTerm : (Γ₁ Γ₂ : RawCtx) → Set
PreTerm Γ₁ Γ₂ = Σ (Raw Ø Γ₁ Γ₂) λ t → DecentTerm t

mkPreTerm : ∀ {Γ₁ Γ₂} {t : Raw Ø Γ₁ Γ₂} → DecentTerm t → PreTerm Γ₁ Γ₂
mkPreTerm {t = t} p = (t , p)

CtxMorP = CtxMor (λ _ → PreTerm)

mkCtxMorP : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
             DecentCtxMor f → CtxMorP Γ₁ Γ₂
mkCtxMorP {Γ₂ = Ø}              p        = []
mkCtxMorP {Γ₂ = x ∷ Γ₂} {t ∷ f} (p , ps) = (t , p) ∷ (mkCtxMorP ps)

TyCtxMorP : TyCtx → TyCtx → Set
TyCtxMorP Θ₁ Ø = ⊤
TyCtxMorP Θ₁ (Γ ∷ Θ₂) = PreType Θ₁ Ø Γ × TyCtxMorP Θ₁ Θ₂

FpDataP : TyCtx → RawCtx → Set
FpDataP Θ Γ = NList (Σ RawCtx (λ Γ' → CtxMorP Γ' Γ × PreType (Γ ∷ Θ) Γ' Ø))

mkFpDataP : ∀ {Θ Γ} {D : FpData Raw Θ Γ} → DecentFpData D → FpDataP Θ Γ
mkFpDataP {D = [ Γ , f , A ]} (p , q) = [ Γ , (mkCtxMorP p) , mkPreType q ]
mkFpDataP {D = (Γ , f , A) ∷ D} ((p , q) , r) =
  (Γ , mkCtxMorP p , mkPreType q) ∷ mkFpDataP {D = D} r

-- | List of types, context morphisms and terms (Aₖ, fₖ, gₖ) such that
--            Γₖ, x : Aₖ[C/X] ⊢ gₖ : C fₖ or
--            Γₖ, x : C fₖ ⊢ gₖ : Aₖ[C/X],
-- which are the premisses of the rule for recursion and corecursion,
-- respectively.
FpMapDataP : RawCtx → Set
FpMapDataP Γ = NList (Σ RawCtx λ Γ' →
                        PreType [ Γ ]L Γ' Ø × CtxMorP Γ' Γ × PreTerm (∗ ∷ Γ') Ø)

mkFpMapDataP : ∀{Γ} {gs : FpMapData Raw Γ} → DecentFpMapData gs → FpMapDataP Γ
mkFpMapDataP {Γ} {[ Γ' , A , f , t ]} (A-decent , f-decent , t-decent) =
  [ Γ' , mkPreType A-decent , mkCtxMorP f-decent , mkPreTerm t-decent ]
mkFpMapDataP {Γ} {(Γ' , A , f , t) ∷ gs} (A-decent , f-decent , t-decent , r) =
  (Γ' , mkPreType A-decent , mkCtxMorP f-decent , mkPreTerm t-decent)
  ∷ mkFpMapDataP {Γ} {gs} r

getFpData : ∀{Γ} → FpMapDataP Γ → FpDataP Ø Γ
getFpData [ Γ' , A , f , _ ]     = [ Γ' , f , A ]
getFpData ((Γ' , A , f , _) ∷ d) = (Γ' , f , A) ∷ getFpData d

projCtxMor₁ : {Γ₁ Γ₂ : RawCtx} → CtxMorP Γ₂ Γ₁ → CtxMor Raw Γ₂ Γ₁
projCtxMor₁ = Vec.map proj₁

projCtxMor₂ : {Γ₁ Γ₂ : RawCtx} →
              (f : CtxMorP Γ₂ Γ₁) →  DecentCtxMor (projCtxMor₁ f)
projCtxMor₂ {Ø} [] = tt
projCtxMor₂ {x ∷ Γ₁} ((t , p) ∷ f) = (p , projCtxMor₂ f)

projPTList₁ : ∀{Γ} → FpMapDataP Γ → FpMapData Raw Γ
projPTList₁ =
  NList.map (Prod.map id (Prod.map proj₁ (Prod.map projCtxMor₁ proj₁)))

projPTList₂ : ∀{Γ} → (gs : FpMapDataP Γ) → DecentFpMapData (projPTList₁ gs)
projPTList₂ [ (Γ' , A , f , t) ] = (proj₂ A , projCtxMor₂ f , proj₂ t)
projPTList₂ ((Γ' , A , f , t) ∷ gs) =
  (proj₂ A , projCtxMor₂ f , proj₂ t , projPTList₂ gs)

projFpData₁ : ∀ {Θ Γ} → FpDataP Θ Γ → FpData Raw Θ Γ
projFpData₁ = NList.map (Prod.map id (Prod.map projCtxMor₁ proj₁))

projFpData₂ : ∀ {Θ Γ} → (D : FpDataP Θ Γ) → DecentFpData (projFpData₁ D)
projFpData₂ [ (Γ , f , A) ] = (projCtxMor₂ f , proj₂ A)
projFpData₂ ((Γ , f , A) ∷ D) = ((projCtxMor₂ f , proj₂ A) , projFpData₂ D)

-----------------------------------------
----- Constructors for pre terms
-----------------------------------------

⊤-PT : (Θ : TyCtx) (Γ : RawCtx) → PreType Θ Γ Ø
⊤-PT Θ Γ = mkPreType (DT-⊤ Θ Γ)

instPT : ∀ {Θ Γ₁ Γ₂ A} → PreType Θ Γ₁ (Γ₂ ↑ A) → PreTerm Γ₁ Ø → PreType Θ Γ₁ Γ₂
instPT (B , p) (t , q) = mkPreType (DT-inst _ _ p q)

_⊙_ = instPT

tyVarPT : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ : RawCtx} → TyVar Θ Γ₂ → PreType Θ Γ₁ Γ₂
tyVarPT Γ₁ X = mkPreType (DT-tyVar _ X)

paramAbstrPT : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) {A : U} →
               PreType Θ (A ∷ Γ₁) Γ₂ → PreType Θ Γ₁ (Γ₂ ↑ A)
paramAbstrPT Γ₁ (A , p) = mkPreType (DT-paramAbstr Γ₁ p)

fpPT : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) →
       FP → FpDataP Θ Γ₂ → PreType Θ Γ₁ Γ₂
fpPT Γ₁ ρ D = mkPreType (DT-fp Γ₁ ρ (projFpData₁ D) (projFpData₂ D))

unitPO : (Γ : RawCtx) → PreTerm Γ Ø
unitPO Γ = mkPreTerm (DO-unit _)

varPO : {Γ : RawCtx} {A : U} → RawVar Γ A → PreTerm Γ Ø
varPO x = mkPreTerm (DO-objVar x)

instPO : ∀ {Γ₁ Γ₂ A} → PreTerm Γ₁ (Γ₂ ↑ A) → PreTerm Γ₁ Ø → PreTerm Γ₁ Γ₂
instPO (t , p) (s , q) = mkPreTerm (DO-inst _ _ p q)

_§ₒ_ = instPO

dialgPO : (Δ : RawCtx) (Γ : RawCtx) (A : U) → FP → ℕ → PreTerm Δ (A ∷ Γ)
dialgPO Δ Γ A ρ k = mkPreTerm (DO-dialg _ Γ A ρ k)

α : (Δ : RawCtx) (Γ : RawCtx) (A : U) → ℕ → PreTerm Δ (A ∷ Γ)
α Δ Γ A k = dialgPO Δ Γ A μ k

ξ : (Δ : RawCtx) (Γ : RawCtx) (A : U) → ℕ → PreTerm Δ (A ∷ Γ)
ξ Δ Γ A k = dialgPO Δ Γ A ν k

-- | Generalised recursion, does recursion or corecursion, depending on ρ
grec : (Γ : RawCtx) (Δ : RawCtx) →
       FpMapDataP Γ → FP → PreTerm Δ (∗ ∷ Γ)
grec Γ Δ gs ρ = mkPreTerm (DO-mapping Γ Δ (projPTList₁ gs) ρ (projPTList₂ gs))

-- | Recursion for inductive types
rec : (Γ : RawCtx) (Δ : RawCtx) →
      FpMapDataP Γ → PreTerm Δ (∗ ∷ Γ)
rec Γ Δ gs = grec Γ Δ gs μ

-- Corecursion
corec : (Γ : RawCtx) (Δ : RawCtx) →
        FpMapDataP Γ → PreTerm Δ (∗ ∷ Γ)
corec Γ Δ gs = grec Γ Δ gs ν

instWCtxMorP : {Γ₁ Γ₂ Γ₃ : RawCtx} →
               PreTerm Γ₁ (Γ₃ ++ Γ₂) → CtxMorP Γ₁ Γ₂ → PreTerm Γ₁ Γ₃
instWCtxMorP {Γ₁} {Ø}      {Γ₃} t [] = subst (PreTerm Γ₁) (proj₂ identity Γ₃) t
instWCtxMorP {Γ₁} {x ∷ Γ₂} {Γ₃} t (s ∷ f) =
  instPO
    (instWCtxMorP {Γ₂ = Γ₂} {Γ₃ = Γ₃ ↑ x}
      (subst (PreTerm Γ₁) (mvVar _ Γ₃ x) t) f)
    s

_§ₘ'_ = instWCtxMorP

_§ₘ_ : {Γ₁ Γ₂ : RawCtx} →
       PreTerm Γ₁ Γ₂ → CtxMorP Γ₁ Γ₂ → PreTerm Γ₁ Ø
t §ₘ f = instWCtxMorP {Γ₃ = Ø} t f

instTyWCtxMorP : ∀ {Θ Γ₁ Γ₂ Γ₃} →
                 PreType Θ Γ₁ (Γ₃ ++ Γ₂) → CtxMorP Γ₁ Γ₂ → PreType Θ Γ₁ Γ₃
instTyWCtxMorP {Θ} {Γ₁} {Ø}      {Γ₃} A [] =
  subst (PreType Θ Γ₁) (proj₂ identity Γ₃) A
instTyWCtxMorP {Θ} {Γ₁} {x ∷ Γ₂} {Γ₃} A (s ∷ f) =
  (instTyWCtxMorP (subst (PreType Θ Γ₁) (mvVar _ Γ₃ x) A) f) ⊙ s

_§ₜ_ : ∀ {Θ Γ₁ Γ₂} →
       PreType Θ Γ₁ Γ₂ → CtxMorP Γ₁ Γ₂ → PreType Θ Γ₁ Ø
A §ₜ f = instTyWCtxMorP {Γ₃ = Ø} A f

---------------------------------------------------------
--------- Recursion for pre-types
---------------------------------------------------------

FpDataP' : (TyCtx → RawCtx → RawCtx → Set) → TyCtx → RawCtx → Set
FpDataP' V Θ Γ = NList (Σ RawCtx (λ Γ' → CtxMorP Γ' Γ × V (Γ ∷ Θ) Γ' Ø))

{-# NON_TERMINATING #-}
mapPT : {V : TyCtx → RawCtx → RawCtx → Set} →
        ((Θ : TyCtx) (Γ₁ : RawCtx) → V Θ Γ₁ Ø) →
        (∀{Θ Γ₁ Γ₂} → TyVar Θ Γ₂ → V Θ Γ₁ Γ₂) →
        (∀{Θ Γ₁ Γ₂ A} → V Θ Γ₁ (Γ₂ ↑ A) → PreTerm Γ₁ Ø → V Θ Γ₁ Γ₂) →
        (∀{Θ Γ₁ Γ₂ A} → V Θ (A ∷ Γ₁) Γ₂ → V Θ Γ₁ (Γ₂ ↑ A)) →
        (∀{Θ Γ₁ Γ₂} → FP → FpDataP' V Θ Γ₂ → V Θ Γ₁ Γ₂) →
        ∀{Θ Γ₁ Γ₂} → PreType Θ Γ₁ Γ₂ → V Θ Γ₁ Γ₂
mapPT ⊤-x _ _ _ _ (._ , DT-⊤ Θ Γ) = ⊤-x Θ Γ
mapPT _ var-x _ _ _ (._ , DT-tyVar Γ₁ X) = var-x X
mapPT ⊤-x var-x inst-x abstr-x fp-x (._ , DT-inst B t B-dec t-dec) =
  let r = mapPT ⊤-x var-x inst-x abstr-x fp-x (B , B-dec)
  in inst-x r (t , t-dec)
mapPT ⊤-x var-x inst-x abstr-x fp-x (._ , DT-paramAbstr Γ₁ {A} A-dec) =
  let r = mapPT ⊤-x var-x inst-x abstr-x fp-x (A , A-dec)
  in abstr-x r
mapPT ⊤-x var-x inst-x abstr-x fp-x (._ , DT-fp Γ₁ ρ D D-dec) =
  let D' = NList.map
           (Prod.map id
             (Prod.map id
               (mapPT ⊤-x var-x inst-x abstr-x fp-x))) (mkFpDataP {D = D} D-dec)
  in fp-x ρ D'

----------------------------------------------------------
--------- Meta theory for decent type predicate
---------------------------------------------------------

weakenDO : (Γ₁ : RawCtx) → {Γ₂ Γ₃ : RawCtx} {t : Raw Ø (Γ₁ ++ Γ₂) Γ₃} →
           (A : U) → DecentTerm t → DecentTerm (weaken Γ₁ A t)
weakenDO Γ₁ B (DO-unit ._)             = DO-unit _
weakenDO Γ₁ B (DO-objVar x)            = DO-objVar (weakenObjVar Γ₁ B x)
weakenDO Γ₁ B (DO-inst t s p q)        =
  DO-inst _ _ (weakenDO Γ₁ B p) (weakenDO Γ₁ B q)
weakenDO Γ₁ B (DO-dialg ._ Γ A ρ k)    = DO-dialg _ _ A ρ k
weakenDO Γ₁ B (DO-mapping Γ ._ gs ρ p) = DO-mapping Γ _ gs ρ p

weakenDT : ∀ {Θ} → (Γ₁ : RawCtx) → {Γ₂ Γ₃ : RawCtx} {A : Raw Θ (Γ₁ ++ Γ₂) Γ₃} →
           (B : U) → DecentType A → DecentType (weaken Γ₁ B A)
weakenDT Γ₁ B (DT-⊤ Θ ._)           = DT-⊤ Θ _
weakenDT Γ₁ B (DT-tyVar _ X)        = DT-tyVar _ X
weakenDT Γ₁ B (DT-inst A t p q)     =
  DT-inst _ _ (weakenDT Γ₁ B p) (weakenDO Γ₁ B q)
weakenDT Γ₁ B (DT-paramAbstr _ p)   = DT-paramAbstr _ (weakenDT _ B p)
weakenDT Γ₁ B (DT-fp _ ρ D p)       = DT-fp _ ρ D p

weakenDO₁ : ∀ {Γ₁ Γ₂} {t : Raw Ø Γ₁ Γ₂} →
            (A : U) → DecentTerm t → DecentTerm (weaken₁ A t)
weakenDO₁ = weakenDO Ø

weakenDT₁ : ∀ {Θ Γ₁ Γ₂} {A : Raw Θ Γ₁ Γ₂} →
            (B : U) → DecentType A → DecentType (weaken₁ B A)
weakenDT₁ = weakenDT Ø

weakenDecentCtxMor : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
                     (A : U) → DecentCtxMor f →
                     DecentCtxMor (Vec.map (weaken₁ A) f)
weakenDecentCtxMor {Γ₂ = Ø}      {[]}    A p        = tt
weakenDecentCtxMor {Γ₂ = x ∷ Γ₂} {t ∷ f} A (p , ps) =
  (weakenDO₁ A p , weakenDecentCtxMor A ps)

weakenCtxMorP : {Γ₁ Γ₂ : RawCtx} → CtxMorP Γ₁ Γ₂ → CtxMorP (∗ ∷ Γ₁) Γ₂
weakenCtxMorP f = mkCtxMorP (weakenDecentCtxMor ∗ (projCtxMor₂ f))

-----------------------------------------------------
------ Meta operations on pre-terms and pre-types
-----------------------------------------------------

weakenPT : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ Γ₃ : RawCtx} →
           (A : U) → PreType Θ (Γ₁ ++ Γ₂) Γ₃ → PreType Θ (Γ₁ ++ A ∷ Γ₂) Γ₃
weakenPT Γ₁ A (B , p) = (_ , weakenDT Γ₁ A p)

weakenPT₁ : ∀ {Θ Γ₁ Γ₂} → (A : U) → PreType Θ Γ₁ Γ₂ → PreType Θ (A ∷ Γ₁) Γ₂
weakenPT₁ = weakenPT Ø

weakenPO : (Γ₁ : RawCtx) {Γ₂ Γ₃ : RawCtx} →
           (A : U) → PreTerm (Γ₁ ++ Γ₂) Γ₃ → PreTerm (Γ₁ ++ A ∷ Γ₂) Γ₃
weakenPO Γ₁ A (t , p) = (_ , weakenDO Γ₁ A p)

weakenPO₁ : {Γ₁ Γ₂ : RawCtx} → (A : U) → PreTerm Γ₁ Γ₂ → PreTerm (A ∷ Γ₁) Γ₂
weakenPO₁ = weakenPO Ø

get' : {Γ₁ Γ₂ : RawCtx} {A : U} →
       (f : CtxMor (λ _ → PreTerm) Γ₂ Γ₁) →
       (x : RawVar Γ₁ A) →
       DecentTerm (get {Raw} (projCtxMor₁ f) x)
get' (t ∷ f) zero                = proj₂ t
get' (t ∷ f) (succ {b = _} _ x)  = get' f x

-- | Lift substitutions to DecentTerm predicate
substDO : {Γ₁ Γ Γ₂ : RawCtx} {t : Raw Ø Γ₁ Γ} →
          (f : CtxMorP Γ₂ Γ₁) →
          DecentTerm t → DecentTerm (substRaw t (projCtxMor₁ f))
substDO f (DO-unit Γ₁)              = DO-unit _
substDO f (DO-objVar x)             = get' f x
substDO f (DO-inst t s p q)         = DO-inst _ _ (substDO f p) (substDO f q)
substDO f (DO-dialg Γ₁ Γ A ρ k)     = DO-dialg _ _ A ρ k
substDO f (DO-mapping Γ Γ₁ gs ρ p)  = DO-mapping Γ _ _ _ p

-- | Lift substRaw to pre terms
substP : {Γ₁ Γ Γ₂ : RawCtx} →
         PreTerm Γ₁ Γ → CtxMorP Γ₂ Γ₁ → PreTerm Γ₂ Γ
substP (t , p) f = (substRaw t (projCtxMor₁ f) , substDO f p)

_↓[_] = substP

-- | Context identity is a decent context morphism
ctxidDO : (Γ : RawCtx) → DecentCtxMor (ctxid Γ)
ctxidDO Ø       = tt
ctxidDO (x ∷ Γ) = (DO-objVar zero , weakenDecentCtxMor _ (ctxidDO Γ))

mkCtxMorP₁ : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
             (p : DecentCtxMor f) → projCtxMor₁ (mkCtxMorP p) ≡ f
mkCtxMorP₁ {Γ₂ = Ø}      {[]} p = refl
mkCtxMorP₁ {Γ₂ = A ∷ Γ₂} {t ∷ f} (p , ps) =
  begin
    projCtxMor₁ {A ∷ Γ₂} ((t , p) ∷ mkCtxMorP ps)
  ≡⟨ refl ⟩
    t ∷ projCtxMor₁ (mkCtxMorP ps)
  ≡⟨ cong (λ u → t ∷ u) (mkCtxMorP₁ ps) ⟩
    t ∷ f
  ∎

ctxidP : (Γ : RawCtx) → CtxMorP Γ Γ
ctxidP Γ = mkCtxMorP (ctxidDO Γ)

_↓[_/0] : {Γ₁ Γ Γ₂ : RawCtx} →
          PreTerm (∗ ∷ Γ₁) Γ → PreTerm Γ₁ Ø  → PreTerm Γ₁ Γ
_↓[_/0] t s = t ↓[ s ∷ ctxidP _ ]

_•_ : {Γ₁ Γ₂ Γ₃ : RawCtx} → CtxMorP Γ₂ Γ₃ → CtxMorP Γ₁ Γ₂ → CtxMorP Γ₁ Γ₃
_•_ {Γ₃ = Ø} [] f = []
_•_ {Γ₃ = A ∷ Γ₃} (t ∷ g) f = substP t f ∷ (g • f)

-- | Context projection is a decent context morphism
ctxProjDO : (Γ₁ Γ₂ : RawCtx) → DecentCtxMor (ctxProjRaw Γ₁ Γ₂)
ctxProjDO Γ₁ Ø        = ctxidDO Γ₁
ctxProjDO Γ₁ (x ∷ Γ₂) = weakenDecentCtxMor _ (ctxProjDO Γ₁ Γ₂)

ctxProjP : (Γ₁ Γ₂ : RawCtx) → CtxMorP (Γ₂ ++ Γ₁) Γ₁
ctxProjP Γ₁ Γ₂ = mkCtxMorP (ctxProjDO Γ₁ Γ₂)

ctxProjP' : (Γ₁ Γ₂ Γ₃ : RawCtx) → CtxMorP (Γ₁ ++ Γ₂ ++ Γ₃) Γ₂
ctxProjP' Γ₁ Γ₂ Ø =
  subst (λ Γ → CtxMorP (Γ₁ ++ Γ) Γ₂)
        (PE.sym (proj₂ identity Γ₂))
        (ctxProjP Γ₂ Γ₁)
ctxProjP' Γ₁ Γ₂ (A ∷ Γ₃) =
  let f = ctxProjP' Γ₁ Γ₂ Γ₃
  in subst (λ Γ → Vec (PreTerm Γ Ø) (length' Γ₂))
           (assoc Γ₁ Γ₂ (A ∷ Γ₃))
           (Vec.map (weakenPO (Γ₁ ++ Γ₂) A)
                    (subst (λ Γ → Vec (PreTerm Γ Ø) (length' Γ₂))
                           (PE.sym (assoc Γ₁ Γ₂ Γ₃))
                           f
                    )
           )

weakenDO' : {Γ₁ Γ₃ : RawCtx} {t : Raw Ø Γ₁ Γ₃} →
            (Γ₂ : RawCtx) → DecentTerm t → DecentTerm (weaken' Γ₂ t)
weakenDO' {Γ₁} {t = t} Γ₂ p =
  subst DecentTerm
        (cong (substRaw t) (mkCtxMorP₁ (ctxProjDO Γ₁ Γ₂)))
        (substDO (ctxProjP Γ₁ Γ₂) p)

weakenPO' : {Γ₁ Γ₃ : RawCtx} →
            (Γ₂ : RawCtx) → PreTerm Γ₁ Γ₃ → PreTerm (Γ₂ ++ Γ₁) Γ₃
weakenPO' Γ₂ (t , p) = (weaken' Γ₂ t , weakenDO' Γ₂ p)

-- | Lift extension of context morphism to decent terms
extendP : {Γ₁ Γ₂ : RawCtx} →
           (A : U) → (f : CtxMorP Γ₂ Γ₁) → CtxMorP (A ∷ Γ₂) (A ∷ Γ₁)
extendP {Γ₁} {Γ₂} A f = varPO zero ∷ Vec.map (weakenPO₁ A) f

getPO : {Γ₁ Γ₂ : RawCtx} {A : U} → CtxMorP Γ₂ Γ₁ → RawVar Γ₁ A → PreTerm Γ₂ Ø
getPO f x = (get {Raw} (projCtxMor₁ f) x , get' f x)

substPO : ∀ {Γ₁ Γ Γ₂} → PreTerm Γ₁ Γ → CtxMorP Γ₂ Γ₁ → PreTerm Γ₂ Γ
substPO (._ , DO-unit Γ₁)             f = unitPO _
substPO (._ , DO-objVar x)            f = getPO f x
substPO (._ , DO-inst t s p q)        f =
  instPO (substPO (t , p) f) (substPO (s , q) f)
substPO (._ , DO-dialg Γ₁ Γ A ρ k)    f = dialgPO _ Γ A ρ k
substPO (._ , DO-mapping Γ Γ₁ gs ρ p) f = grec Γ _ (mkFpMapDataP {Γ} {gs} p) ρ

weakenPO'' : {Γ₁ Γ₃ : RawCtx} →
             (Γ₂ Γ₂' : RawCtx) → PreTerm Γ₁ Γ₃ → PreTerm (Γ₂' ++ Γ₁ ++ Γ₂) Γ₃
weakenPO'' Γ₂ Γ₂' t = substPO t (ctxProjP' Γ₂' _ Γ₂)

-- | Lift substitution to pretypes
substPT : ∀ {Θ Γ₁ Γ Γ₂} → PreType Θ Γ₁ Γ → CtxMorP Γ₂ Γ₁ → PreType Θ Γ₂ Γ
substPT (._ , DT-⊤ Θ Γ)               f = ⊤-PT _ _
substPT (._ , DT-tyVar Γ₁ X)          f = tyVarPT _ X
substPT (._ , DT-inst B t p q)        f =
  (substPT (B , p) f) ⊙ (substPO (t , q) f)
substPT (._ , DT-paramAbstr Γ₁ {A} p) f =
  paramAbstrPT _ (substPT (A , p) (extendP _ f))
substPT (._ , DT-fp Γ₁ ρ D q)         f = fpPT _ ρ (mkFpDataP {D = D} q)

weakenPT' : ∀ {Θ Γ₁ Γ₂} (Γ : RawCtx) → PreType Θ Γ₁ Γ₂ → PreType Θ (Γ ++ Γ₁) Γ₂
weakenPT' {Γ₁ = Γ₁} Γ A = substPT A (ctxProjP Γ₁ Γ)

weakenPT'' : ∀ {Θ Γ₁} (Γ : RawCtx) → PreType Θ Ø Γ₁ → PreType Θ Γ Γ₁
weakenPT'' Γ A =
  subst (λ u → PreType _ u _) (proj₂ identity Γ) (weakenPT' Γ A)

-- | Project a specific variable out
projVar : (Γ₁ Γ₂ : RawCtx) (A : U) → PreTerm (Γ₂ ++ A ∷ Γ₁) Ø
projVar Γ₁ Ø        A = varPO zero
projVar Γ₁ (∗ ∷ Γ₂) A = weakenPO₁ _ (projVar Γ₁ Γ₂ A)

extendProj : {Γ₁ Γ₂ : RawCtx} → (Γ₃ Γ₄ : RawCtx) →
             CtxMorP (Γ₄ ++ Γ₃ ++ Γ₂) Γ₁ →
             CtxMorP (Γ₄ ++ Γ₃ ++ Γ₂) (Γ₃ ++ Γ₁)
extendProj Ø Γ₄ f = f
extendProj {Γ₁} {Γ₂ = Γ₂} (A ∷ Γ₃) Γ₄ f =
  let p = (assoc Γ₄ (A ∷ Ø) (Γ₃ ++ Γ₂))
      f' = subst (λ u → CtxMorP u Γ₁) (PE.sym p) f
      g = extendProj {Γ₁} {Γ₂} Γ₃ (Γ₄ ↑ A) f'
      g' = subst (λ u → CtxMorP u (Γ₃ ++ Γ₁)) p g
  in projVar (Γ₃ ++ Γ₂) Γ₄ A ∷ g'

weakenTyVar₁ : ∀{Θ₂ Γ₁} (Θ₁ : TyCtx) (Γ : RawCtx) →
               TyVar (Θ₁ ++ Θ₂) Γ₁ → TyVar (Θ₁ ++ Γ ∷ Θ₂) Γ₁
weakenTyVar₁ Ø         Γ X           = succ _ X
weakenTyVar₁ (Γ₁ ∷ Θ₁) Γ zero        = zero
weakenTyVar₁ (Γ₂ ∷ Θ₁) Γ (succ Γ₁ X) = succ Γ₁ (weakenTyVar₁ Θ₁ Γ X)

weakenTyFpData'₁ : ∀ {Θ₂ Γ₁} (Θ₁ : TyCtx) →
                   {D : FpData Raw (Θ₁ ++ Θ₂) Γ₁} →
                   (Γ : RawCtx) → DecentFpData D →
                   Σ (FpData Raw (Θ₁ ++ Γ ∷ Θ₂) Γ₁) DecentFpData

-- | Auxiliary definition to allow Agda to see that it is provided with
-- a well-defined reursion.
weakenTy'₁ : ∀ {Θ₂ Γ₁ Γ₂} (Θ₁ : TyCtx) (Γ : RawCtx) →
             (A : Raw (Θ₁ ++ Θ₂) Γ₁ Γ₂) → DecentType A →
             PreType (Θ₁ ++ Γ ∷ Θ₂) Γ₁ Γ₂
weakenTy'₁ Θ₁ Γ ._ (DT-⊤ ._ Γ₁) =
  ⊤-PT _ _
weakenTy'₁ Θ₁ Γ .(tyVarRaw Γ₁ X) (DT-tyVar Γ₁ X) =
  tyVarPT Γ₁ (weakenTyVar₁ Θ₁ Γ X)
weakenTy'₁ Θ₁ Γ .(instRaw B t) (DT-inst B t p q) =
  (weakenTy'₁ Θ₁ Γ B p) ⊙ (t , q)
weakenTy'₁ Θ₁ Γ .(paramAbstrRaw Γ₁ A) (DT-paramAbstr Γ₁ {A} p) =
  paramAbstrPT Γ₁ (weakenTy'₁ Θ₁ Γ A p)
weakenTy'₁ Θ₁ Γ .(fpRaw Γ₁ ρ D) (DT-fp Γ₁ ρ D p) =
  let (D' , p') = weakenTyFpData'₁ Θ₁ {D} Γ p
  in fpPT Γ₁ ρ (mkFpDataP {D = D'} p')

weakenTyFpData'₁ {Γ₁ = Γ₁} Θ₁ {[ Γ₂ , f , A ]}   Γ (p , q) =
  let (A' , q') = weakenTy'₁ (Γ₁ ∷ Θ₁) Γ A q
  in ([ Γ₂ , f , A' ] , p , q')
weakenTyFpData'₁ {Γ₁ = Γ₁} Θ₁ {(Γ₂ , f , A) ∷ D} Γ ((p , q) , r) =
  let (A' , q') = weakenTy'₁ (Γ₁ ∷ Θ₁) Γ A q
      (D' , r') = weakenTyFpData'₁ Θ₁ {D} Γ r
  in ((Γ₂ , f , A') ∷ D' , (p , q') , r')

weakenTy₁ : ∀ {Θ₂ Γ₁ Γ₂} (Θ₁ : TyCtx) (Γ : RawCtx) →
            PreType (Θ₁ ++ Θ₂) Γ₁ Γ₂ →
            PreType (Θ₁ ++ Γ ∷ Θ₂) Γ₁ Γ₂
weakenTy₁ Θ₁ Γ (A , p) = weakenTy'₁ Θ₁ Γ A p

weakenTyCtxMor₁ : ∀ {Θ₁ Θ₂} →
                  (Γ : RawCtx) → TyCtxMorP Θ₂ Θ₁ → TyCtxMorP (Γ ∷ Θ₂) Θ₁
weakenTyCtxMor₁ {Ø} Γ tt = tt
weakenTyCtxMor₁ {Γ₁ ∷ Θ₁} Γ (A , f) = (weakenTy₁ Ø Γ A , weakenTyCtxMor₁ Γ f)

getTy : ∀ {Θ₁ Θ₂ Γ₁ Γ₂} → TyCtxMorP Θ₁ Θ₂ → TyVar Θ₂ Γ₂ → PreType Θ₁ Γ₁ Γ₂
getTy {Θ₂ = Ø} tt ()
getTy {Θ₁} {Θ₂ = Γ ∷ Θ₂} {Γ₁} (B , f) zero =
  subst (λ Γ' → PreType Θ₁ Γ' Γ) (proj₂ identity Γ₁) (weakenPT' Γ₁ B)
getTy {Θ₂ = Γ ∷ Θ₂} (B , f) (succ Γ₂ X) = getTy f X

extendTy : ∀ {Θ₁ Θ₂} →
           TyCtxMorP Θ₁ Θ₂ → (Γ : RawCtx) → TyCtxMorP (Γ ∷ Θ₁) (Γ ∷ Θ₂)
extendTy f Γ = (tyVarPT Ø zero , weakenTyCtxMor₁ Γ f)

substTyFpData' : ∀ {Θ₁ Θ₂ Γ} →
                 (D : FpData Raw Θ₂ Γ) → DecentFpData D →
                 TyCtxMorP Θ₁ Θ₂ → FpDataP Θ₁ Γ

-- | Substitution for type variables, auxilary version to have a clearly
-- terminating definition.
substTy' : ∀ {Θ₁ Θ₂ Γ₁ Γ₂} →
            (A : Raw Θ₂ Γ₁ Γ₂) → DecentType A → TyCtxMorP Θ₁ Θ₂ →
            PreType Θ₁ Γ₁ Γ₂

substTy' {Θ₁} ._ (DT-⊤ Θ Γ)               f = ⊤-PT Θ₁ _
substTy' {Θ₁} ._ (DT-tyVar Γ₁ X)          f = getTy f X
substTy' {Θ₁} ._ (DT-inst B t p q)        f =
  (substTy' B p f) ⊙ (t , q)
substTy' {Θ₁} ._ (DT-paramAbstr Γ₁ {A} p) f =
  paramAbstrPT Γ₁ (substTy' A p f)
substTy' {Θ₁} ._ (DT-fp Γ₁ ρ D p)         f =
  fpPT Γ₁ ρ (substTyFpData' D p f)

substTyFpData' {Γ = Γ} [ Γ₁ , g , A ] (p , q) f =
  [ Γ₁ , mkCtxMorP p , substTy' A q (extendTy f Γ) ]
substTyFpData' {Γ = Γ} ((Γ₁ , g , A) ∷ D) ((p , q) , r) f =
  (Γ₁ , mkCtxMorP p , substTy' A q (extendTy f Γ))
  ∷ substTyFpData' D r f

-- | Substitution for type variables
substTy : ∀ {Θ₁ Θ₂ Γ₁ Γ₂} →
          PreType Θ₂ Γ₁ Γ₂ → TyCtxMorP Θ₁ Θ₂ → PreType Θ₁ Γ₁ Γ₂
substTy (A , p) = substTy' A p

{-
weakenTy : {Θ₁ : TyCtx} {Γ₁ Γ₂ : RawCtx}
           (Θ₂ : TyCtx) → Raw Θ₁ Γ₁ Γ₂ → Raw (Θ₂ ++ Θ₁) Γ₁ Γ₂
weakenTy = {!!}
-}

-----------------------------------------------
--- Other operations
----------------------------------------------
Λ : ∀ {Θ Γ₁ Γ₂} → PreType Θ Γ₁ Γ₂ → PreType Θ Ø (Γ₂ ++ Γ₁)
Λ {Γ₁ = Ø}           A =
  subst (λ Γ → PreType _ Ø Γ) (PE.sym (proj₂ identity _)) A
Λ {Γ₁ = B ∷ Γ₁} {Γ₂} A =
  let A' = Λ (paramAbstrPT Γ₁ A)
  in subst (λ Γ → PreType _ Ø Γ) (assoc Γ₂ (B ∷ Ø) Γ₁) A'

--------------------------------------------------
-- Examples
--------------------------------------------------

-- We could prove the following
-- DT-Prod : (Γ : RawCtx) → DecentType (ProdRaw Γ)
-- However, it is easier to construct the product directly as pretype.

Prod : (Γ : RawCtx) → PreType (Γ ︵ Γ) Ø Γ
Prod Γ = fpPT Ø ν D
  where
    Δ = Γ ︵ Γ

    A : TyVar (Γ ∷ Δ) Γ
    A = succ Γ zero

    B : TyVar (Γ ∷ Δ) Γ
    B = succ Γ (succ Γ zero)

    D₁ = (Γ , ctxidP Γ , instTyWCtxMorP (tyVarPT Γ A) (ctxidP Γ))

    D₂ = (Γ , ctxidP Γ , instTyWCtxMorP (tyVarPT Γ B) (ctxidP Γ))

    D : FpDataP Δ Γ
    D = D₁ ∷ [ D₂ ]

max_stars_repo_name: StillerHarpo/CoindDepTypes

max_issues_repo_name: StillerHarpo/CoindDepTypes

max_forks_repo_name: StillerHarpo/CoindDepTypes


text:
module Structure.Operator.Vector.FiniteDimensional.LinearMaps.ChangeOfBasis where

open import Functional
import      Lvl
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Structure.Function.Multi
open import Structure.Operator.Properties
open import Structure.Operator.Vector.FiniteDimensional
open import Structure.Operator.Vector.LinearCombination
open import Structure.Operator.Vector.LinearMap
open import Structure.Operator.Vector.Proofs
open import Structure.Operator.Vector
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ : Lvl.Level
private variable V Vₗ Vᵣ S : Type{ℓ}
private variable _+ᵥ_ : V → V → V
private variable _⋅ₛᵥ_ : S → V → V
private variable _+ₛ_ _⋅ₛ_ : S → S → S
private variable n : ℕ
private variable i j k : 𝕟(n)
private variable vf : Vec(n)(V)

module _
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (vectorSpace : VectorSpace{V = V}{S = S}(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_))
  where

  open VectorSpace(vectorSpace)

  -- changeBasis : LinearOperator(vectorSpace)(linearCombination )

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:
open import Common.Prelude hiding (tt)

instance
  tt : ⊤
  tt = record{}

_<_ : Nat → Nat → Set
m < zero = ⊥
zero < suc n = ⊤
suc m < suc n = m < n

instance
  <-suc : ∀ {m n} {{_ : m < n}} → m < suc n
  <-suc {zero} = tt
  <-suc {suc m} {zero} {{}}
  <-suc {suc m} {suc n} = <-suc {m} {n}


text:
S : Set
S = S


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid where

open import Cubical.Algebra.CommMonoid.Base public
open import Cubical.Algebra.CommMonoid.Properties public

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Equivalence
open import HoTT.Equivalence.Sigma
open import HoTT.Identity.Sigma
open import HoTT.Identity.Pi
open import HoTT.Transport.Identity
open import HoTT.HLevel
open import HoTT.Exercises.Chapter2.Exercise11 using (module Square ; pullback)

module HoTT.Exercises.Chapter2.Exercise12
  {i} {A B C D E F : 𝒰 i}
  {ac : A → C} {ab : A → B} {cd : C → D} {bd : B → D}
  {ce : C → E} {ef : E → F}              {df : D → F} where

module Squareₗ = Square ac ab cd bd
module Squareᵣ = Square ce cd ef df
module Squareₒ = Square (ce ∘ ac) ab ef (df ∘ bd)

module _ {commₗ : Squareₗ.IsCommutative} {commᵣ : Squareᵣ.IsCommutative}
         {pullbackᵣ : Squareᵣ.IsPullback commᵣ {i}}
  where
  commₒ : Squareₒ.IsCommutative
  commₒ = commᵣ ∘ ac ∙ₕ ap df ∘ commₗ

  open Squareₗ.Commutative commₗ using () renaming (inducedMap to fₗ)
  open Squareᵣ.Commutative commᵣ using () renaming (inducedMap to fᵣ)
  open Squareₒ.Commutative commₒ using () renaming (inducedMap to fₒ)

  -- Solution based on https://pcapriotti.github.io/hott-exercises/chapter2.ex12.core.html
  equiv : (X : 𝒰 i) →
          pullback (X → C) (X → B) (cd ∘_) (bd ∘_) ≃
          pullback (X → E) (X → B) (ef ∘_) ((df ∘ bd) ∘_)
  equiv X =
    -- Use pullbackᵣ to expand X → C to pullback (X → E) (X → D) (ef ∘_) (df ∘_)
    pullback (X → C) (X → B) (cd ∘_) (bd ∘_)
      ≃⟨ Σ-equiv₁ (fᵣ , pullbackᵣ X) ⟩
    -- Reassociate pairs
    Σ[ (_ , xd , _) ∶ pullback (X → E) (X → D) (ef ∘_) (df ∘_) ] Σ[ xb ∶ (X → B) ] (xd == bd ∘ xb)
      ≃⟨ (λ{((xe , xd , pᵣ) , xb , pₗ) → xe , xb , xd , pₗ , pᵣ}) , qinv→isequiv
       ( (λ{(xe , xb , xd , pₗ , pᵣ) → (xe , xd , pᵣ) , xb , pₗ})
       , (λ{((xe , xd , pᵣ) , xb , refl) → refl})
       , (λ{(xe , xb , xd , pₗ , pᵣ) → refl}) ) ⟩
    Σ[ xe ∶ (X → E) ] Σ[ xb ∶ (X → B) ] Σ[ xd ∶ (X → D) ] (xd == bd ∘ xb) × (ef ∘ xe == df ∘ xd)
      ≃⟨ Σ-equiv₂ (λ xe → Σ-equiv₂ λ xb →
        -- Use pₗ to rewrite ef ∘ xe == df ∘ xd as df ∘ bd ∘ xb,
        -- removing the dependency on xd
        Σ[ xd ∶ (X → D) ] (xd == bd ∘ xb) × (ef ∘ xe == df ∘ xd)
          ≃⟨ Σ-equiv₂ (λ xd → Σ-equiv₂ (idtoeqv ∘ ap (λ xf → ef ∘ xe == df ∘ xf))) ⟩
        -- Associate pₗ with xd
        Σ[ xd ∶ (X → D) ] (xd == bd ∘ xb) × (ef ∘ xe == df ∘ bd ∘ xb)
          ≃⟨ Σ-assoc ⟩
        -- Use Lemmas 3.11.8 and 3.11.9 (ii) to contract xd to bd ∘ xb
        (Σ[ xd ∶ (X → D) ] (xd == bd ∘ xb)) × (ef ∘ xe == df ∘ bd ∘ xb)
          ≃⟨ Σ-contr₁ ⦃ =-contrᵣ (bd ∘ xb) ⦄ ⟩
        ef ∘ xe == df ∘ bd ∘ xb
          ∎) ⟩
    pullback (X → E) (X → B) (ef ∘_) ((df ∘ bd) ∘_)
      ∎
    where
    open ≃-Reasoning

  -- Proves that we compose the above equivalence with fₗ, we get out fₒ
  equiv-fₗ→fₒ : {X : 𝒰 i} (xa : X → A) → pr₁ (equiv X) (fₗ xa) == fₒ xa
  equiv-fₗ→fₒ {X = X} xa = pair⁼ (refl , pair⁼ (refl , p))
    where
    xe = ce ∘ ac ∘ xa
    q : (cd ∘ ac ∘ xa , _) == (bd ∘ ab ∘ xa , _)
    q = pair⁼ (funext (commₗ ∘ xa) ⁻¹ , _) ⁻¹
    p : pr₂ (pr₂ (pr₁ (equiv X) (fₗ xa))) == funext (commᵣ ∘ ac ∘ xa ∙ₕ ap df ∘ commₗ ∘ xa)
    p =
      -- Simplify the constant transport
      transport _ q _
        =⟨ transportconst q  _ ⟩
      -- Move the ap function into the transport
      transport id (ap (λ xd → ef ∘ xe == df ∘ xd) (funext (commₗ ∘ xa))) (funext (commᵣ ∘ ac ∘ xa))
        =⟨ transport-ap id (λ xd → ef ∘ xe == df ∘ xd) (funext (commₗ ∘ xa)) (funext (commᵣ ∘ ac ∘ xa)) ⟩
      -- Apply Theorem 2.11.3 to eliminate the transport
      transport (λ xf → ef ∘ xe == df ∘ xf) (funext (commₗ ∘ xa)) (funext (commᵣ ∘ ac ∘ xa))
        =⟨ transport=-constₗ (ef ∘ xe) (df ∘_) (funext (commₗ ∘ xa)) (funext (commᵣ ∘ ac ∘ xa)) ⟩
      -- Combine the ap df into the funext on the right
      funext (commᵣ ∘ ac ∘ xa) ∙ ap (df ∘_) (funext (commₗ ∘ xa))
        =⟨ _ ∙ₗ funext-ap df (commₗ ∘ xa) ⁻¹ ⟩
      -- Combine the two funext
      funext (commᵣ ∘ ac ∘ xa) ∙ funext (ap df ∘ commₗ ∘ xa)
        =⟨ funext-∙ₕ (commᵣ ∘ ac ∘ xa) (ap df ∘ commₗ ∘ xa) ⁻¹ ⟩
      funext (commᵣ ∘ ac ∘ xa ∙ₕ ap df ∘ commₗ ∘ xa)
        ∎
      where open =-Reasoning

  prop₁ : Squareₗ.IsPullback commₗ → Squareₒ.IsPullback commₒ
  prop₁ pullbackₗ X = transport isequiv (funext equiv-fₗ→fₒ) (pr₂ ((fₗ , pullbackₗ X) ∙ₑ equiv X))

  equiv-fₒ→fₗ : {X : 𝒰 i} (xa : X → A) → pr₁ (equiv X ⁻¹ₑ) (fₒ xa) == fₗ xa
  equiv-fₒ→fₗ {X = X} xa = ap g (equiv-fₗ→fₒ xa ⁻¹) ∙ η (fₗ xa)
    where
    open qinv (isequiv→qinv (pr₂ (equiv X)))

  prop₂ : Squareₒ.IsPullback commₒ {i} → Squareₗ.IsPullback commₗ {i}
  prop₂ pullbackₒ X = transport isequiv (funext equiv-fₒ→fₗ) (pr₂ ((fₒ , pullbackₒ X) ∙ₑ equiv X ⁻¹ₑ))

  -- I tried quite hard to come up with the equivalences directly,
  -- but was only able to find one of the four necessary homotopies.
  -- The other three quickly spiraled out of control.

  =pullback-intro : {A B C : 𝒰 i} {ac : A → C} {bc : B → C}
                    {x@(a₁ , b₁ , p) y@(a₂ , b₂ , q) : pullback A B ac bc} →
                    Σ[ p₁ ∶ a₁ == a₂ ] Σ[ p₂ ∶ b₁ == b₂ ] (p ∙ ap bc p₂ == ap ac p₁ ∙ q) → x == y
  =pullback-intro {x = _ , _ , _} {y = _ , _ , _} (refl , refl , p) rewrite unitᵣ ∙ p ∙ unitₗ ⁻¹ = refl

  =pullback-elim : {A B C : 𝒰 i} {ac : A → C} {bc : B → C}
                   {x@(a₁ , b₁ , p) y@(a₂ , b₂ , q) : pullback A B ac bc} →
                   x == y → Σ[ p₁ ∶ a₁ == a₂ ] Σ[ p₂ ∶ b₁ == b₂ ] (p ∙ ap bc p₂ == ap ac p₁ ∙ q)
  =pullback-elim {x = _ , _ , _} {y = _ , _ , _} refl = refl , refl , unitᵣ ⁻¹ ∙ unitₗ

  prop₁' : Squareₗ.IsPullback commₗ → Squareₒ.IsPullback commₒ
  prop₁' pullbackₗ X with isequiv→qinv (pullbackᵣ X) | isequiv→qinv (pullbackₗ X)
  ... | (gᵣ , ηᵣ , εᵣ) | (gₗ , ηₗ , εₗ) = qinv→isequiv (gₒ , ηₒ , εₒ)
    where
    gₒ : pullback (X → E) (X → B) (ef ∘_) ((df ∘ bd) ∘_) → (X → A)
    gₒ (xe , xb , p) = gₗ (gᵣ xc' , xb , ap (pr₁ ∘ pr₂) (εᵣ xc'))
      where
      xc' = (xe , bd ∘ xb , p)

    ηₒ : gₒ ∘ fₒ ~ id
    ηₒ xa = ap gₗ (=pullback-intro (p-xc , refl , p-pₗ)) ∙ ηₗ xa
      where
      pᵣ = funext (commᵣ ∘ ac ∘ xa ∙ₕ ap df ∘ commₗ ∘ xa)
      xc' = ce ∘ ac ∘ xa , bd ∘ ab ∘ xa , pᵣ
      p-xd = funext (commₗ ∘ xa) ⁻¹
      p-pᵣ : pᵣ ∙ ap (df ∘_) p-xd == refl ∙ funext (commᵣ ∘ ac ∘ xa)
      p-pᵣ =
        pᵣ ∙ ap (df ∘_) p-xd                  =⟨ _ ∙ₗ ap-inv (df ∘_) (funext (commₗ ∘ xa)) ⟩
        _ ∙ p ⁻¹                              =⟨ funext-∙ₕ (commᵣ ∘ ac ∘ xa) (ap df ∘ commₗ ∘ xa) ∙ᵣ _  ⟩
        _ ∙ funext (ap df ∘ commₗ ∘ xa) ∙ _   =⟨ _ ∙ₗ funext-ap df (commₗ ∘ xa) ∙ᵣ _ ⟩
        funext (commᵣ ∘ ac ∘ xa) ∙ p ∙ p ⁻¹   =⟨ assoc ⁻¹ ⟩
        funext (commᵣ ∘ ac ∘ xa) ∙ (p ∙ p ⁻¹) =⟨ _ ∙ₗ invᵣ ⟩
        funext (commᵣ ∘ ac ∘ xa) ∙ refl       =⟨ unitᵣ ⁻¹ ⟩
        funext (commᵣ ∘ ac ∘ xa)              =⟨ unitₗ ⟩
        refl ∙ funext (commᵣ ∘ ac ∘ xa)       ∎
        where
        open =-Reasoning
        p = ap (df ∘_) (funext (commₗ ∘ xa))
      p-xc : gᵣ xc' == ac ∘ xa
      p-xc = ap gᵣ (=pullback-intro (refl , p-xd , p-pᵣ)) ∙ ηᵣ (ac ∘ xa)

      -- TODO
      postulate
        p-pₗ : ap (pr₁ ∘ pr₂) (εᵣ xc') ∙ refl == ap (cd ∘_) p-xc ∙ funext (commₗ ∘ xa)

    -- TODO
    postulate
      εₒ : fₒ ∘ gₒ ~ id

  prop₂' : Squareₒ.IsPullback commₒ → Squareₗ.IsPullback commₗ
  prop₂' sₒ-pullback X = qinv→isequiv (gₗ , ηₗ , εₗ)
    where
    open qinv (isequiv→qinv (sₒ-pullback X)) renaming (g to gₒ ; η to ηₒ ; ε to εₒ)
    open qinv (isequiv→qinv (pullbackᵣ X)) renaming (g to gᵣ ; η to ηᵣ ; ε to εᵣ)

    gₗ : pullback (X → C) (X → B) (cd ∘_) (bd ∘_) → (X → A)
    gₗ (xc , xb , pₗ) = gₒ (ce ∘ xc , xb , funext (commᵣ ∘ xc) ∙ ap (df ∘_) pₗ)

    ηₗ : gₗ ∘ fₗ ~ id
    ηₗ xa = ap gₒ (pair⁼ (refl , pair⁼ (refl ,
      _ ∙ₗ funext-ap df (commₗ ∘ xa) ⁻¹ ∙
      funext-∙ₕ (commᵣ ∘ ac ∘ xa) (ap df ∘ commₗ ∘ xa) ⁻¹))) ∙ ηₒ xa

    εₗ : fₗ ∘ gₗ ~ id
    εₗ (xc , xb , pₗ) = =pullback-intro (p-xc , p-xb , p-pₗ)
      where
      xa = gₗ (xc , xb , pₗ)
      xa' = ce ∘ xc , xb , funext (commᵣ ∘ xc) ∙ ap (df ∘_) pₗ
      p-xa' = =pullback-elim (εₒ xa')
      p-xe = pr₁ p-xa'
      p-xb = pr₁ (pr₂ p-xa')
      p-pₒ = pr₂ (pr₂ p-xa')
      p-xd = funext (commₗ ∘ xa) ∙ ap (bd ∘_) p-xb ∙ pₗ ⁻¹
      -- TODO
      postulate
        p-pᵣ : funext (commᵣ ∘ ac ∘ xa) ∙ ap (df ∘_) p-xd == ap (ef ∘_) p-xe ∙ funext (commᵣ ∘ xc)
      p-xc : ac ∘ xa == xc
      p-xc = ηᵣ (ac ∘ xa) ⁻¹ ∙ ap gᵣ (=pullback-intro (p-xe , p-xd , p-pᵣ)) ∙ ηᵣ xc
      -- TODO
      postulate
        p-pₗ : funext (commₗ ∘ xa) ∙ ap (bd ∘_) p-xb == ap (cd ∘_) p-xc ∙ pₗ

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
-- {-# OPTIONS -v tc.constr.findInScope:15 -v tc.meta.new:50 #-}
-- Andreas, 2012-10-20 issue raised by d.starosud
-- solved by dropping UnBlock constraints during trial candidate assignment
module Fail.Issue723 where

import Common.Level
open import Common.Prelude using (Bool; false; zero) renaming (Nat to ℕ)

record Default {ℓ} (A : Set ℓ) : Set ℓ where
  constructor create
  field default : A

open Default {{...}} using (default)

instance
  defBool : Default Bool
  defBool = create false

  defSet  : Default Set
  defSet  = create Bool

  defNat : Default ℕ
  defNat = create zero

  defDef : Default (Default ℕ)
  defDef = create defNat

  defFunc : ∀ {ℓ} {A : Set ℓ} → Default (A → A)
  defFunc = create (λ x → x)

-- these lines are compiled successfully

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

syntax id A x = x ∶ A

n₁ = default ∶ ℕ
f₁ = default ∶ (ℕ → ℕ)

-- WAS: but this one hangs on "Checking"
n₂ = default (5 ∶ ℕ) ∶ ℕ
-- n₂ = id ℕ (default (id ℕ 5))

n : ℕ
n = default 5
-- now we get unsolved metas
-- that's kind of ok

n₃ = (default ∶ (_ → _)) 5
-- this one works again (before: also unsolved metas (worked before switching of the occurs-error (Issue 795)))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------------
-- Testing the translation of function, predicates and variables names
------------------------------------------------------------------------------

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

-- From the technical manual of TPTP
-- (http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml)

-- ... variables start with upper case letters, ... predicates and
-- functors either start with lower case and contain alphanumerics and
-- underscore ...

module Names where

infix 4 _≡_

------------------------------------------------------------------------------
-- Testing funny names

postulate
  D     : Set
  _≡_   : D → D → Set
  FUN!  : D → D   -- A funny function name.
  PRED! : D → Set -- A funny predicate name.

-- Using a funny function and variable name.
postulate funnyFV  : (nx∎ : D) → FUN! nx∎ ≡ nx∎
{-# ATP axiom funnyFV #-}

-- Using a funny predicate name.
postulate funnyP : (n : D) → PRED! n
{-# ATP axiom funnyP #-}

-- We need to have at least one conjecture to generate a TPTP file.
postulate refl : ∀ d → d ≡ d
{-# ATP prove refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia