text:
module DeclSN where

open import Data.Sum
open import Library
open import Terms
open import Substitution
open import TermShape
open import SN
open import Reduction

-- SN as accessibility

data sn {Γ} {a} (t : Tm Γ a) : Set where
  acc : (∀ {t'} → t ⇒β t' → sn t') → sn t

sn⇒β :  ∀ {Γ} {a} {t t' : Tm Γ a} → sn t → t ⇒β t' → sn t'
sn⇒β (acc h) r = h r

varsn : ∀ {Γ} {a} (x : Var Γ a) → sn (var x)
varsn x = acc λ { (cong () _ _) }

abssn : ∀ {Γ} {a b} {t : Tm (a ∷ Γ) b} → sn t → sn (abs t)
abssn (acc f) = acc (λ { {._} (cong abs abs x)  → abssn (f x) })

subsn : ∀ {Γ Δ} {a b} {f : Tm Γ a -> Tm Δ b} →
        (g : ∀ {t t' : Tm Γ a} → t ⇒β t' → f t ⇒β f t') →
        ∀ {t} → sn (f t) → sn t
subsn g (acc ft) = acc λ t⇒ → subsn g (ft (g t⇒))

-- Goal here: prove that sne is closed under application.

appsn : ∀ {Γ a b} {t : Tm Γ (a →̂ b)} {u} → sn t → sn u → SNe t →
        ∀ {r : Tm Γ b} → app t u ⇒β r → sn r
appsn (acc 𝒕) 𝒖       𝒏           (cong (appl u) (appl .u) t⇒) = acc (appsn (𝒕 t⇒) 𝒖      (mapβSNe t⇒ 𝒏 ))
appsn 𝒕       (acc u) 𝒏           (cong (appr t) (appr .t) t⇒) = acc (appsn 𝒕      (u t⇒) 𝒏)
appsn 𝒕       u       (elim 𝒏 ()) β

elimsn : ∀ {Γ a b}{E : ECxt Γ a b}{t : Tm Γ a}{Et : Tm Γ b} → sn t → PCxt sn Et E t → SNe t →
         ∀ {Et' : Tm Γ b} → Et ⇒β Et' → sn Et'
elimsn 𝒕 (appl 𝒖) 𝒏 t⇒ = appsn 𝒕 𝒖 𝒏 t⇒

substβsn : ∀ {i m vt a Γ} {Δ} {σ ρ : RenSub {m} vt Γ Δ} → (∀ {b} (x : Var Γ b) → vt2tm _ (σ x) ⇒β* vt2tm _ (ρ x))
             → (t : Tm Γ a) → SN {i} (subst σ t) → SN {i} (subst ρ t)
substβsn f t =  mapβ*SN (subst⇒β* f t)

antiSubst : ∀ {Γ a b} {t : Tm (a ∷ Γ) b}{u : Tm Γ a} → sn (subst (sgs u) t) → sn t
antiSubst {t = t} = subsn (λ x → subst⇒β (sgs _) x)

_[_]⇒β : ∀ {Γ} {a b} (E : ECxt Γ a b) {t₁ t₂ : Tm Γ a} →  t₁ ⇒β t₂ → E [ t₁ ] ⇒β E [ t₂ ]
appl u [ t⇒ ]⇒β = cong (appl u) (appl u) t⇒

_[_]⇒β* : ∀ {Γ} {a b} (E : ECxt* Γ a b) {t₁ t₂ : Tm Γ a} → t₁ ⇒β t₂ → E [ t₁ ]* ⇒β E [ t₂ ]*
[]       [ t⇒ ]⇒β* = t⇒
(E ∷ Es) [ t⇒ ]⇒β* = Es [ E [ t⇒ ]⇒β ]⇒β*

cong*2 : ∀ {Γ a b t t'}(E : ECxt* Γ a b)
          → (t⇒ : t ⇒β t')
          → E [ t ]* ⇒β E [ t' ]*
cong*2 E t⇒ =  E [ t⇒ ]⇒β*

subexpsn : ∀ {Γ a b} (E : ECxt* Γ a b) {t : Tm Γ a} → sn (E [ t ]*) -> sn t
subexpsn E = subsn (cong*3 E)

data _Redex {Γ} : ∀ {a} → Tm Γ a → Set where

  β     : ∀ {a b}{t : Tm (a ∷ Γ) b}{u}
          → (app (abs t) u) Redex

mkHole2 : ∀ {Γ} {a b} (E : ECxt Γ a b) {t : Tm Γ a} → βEhole (E [ t ]) (EC→βEC E) t
mkHole2 (appl u) = appl u

mkHole3 : ∀ {Γ} {a b c} (E : ECxt Γ a b) {Es : ECxt* Γ _ _} {t : Tm Γ c} → βEhole ((Es ∷r E) [ t ]*) (EC→βEC E) (Es [ t ]*)
mkHole3 E {Es} {t} rewrite ≡.sym (lemma {t = t} Es {E = E}) = mkHole2 E {Es [ t ]*}

≡subst⇒β : ∀ {a Γ} {t t1 t' t'1 : Tm Γ a} → t ≡ t1 → t' ≡ t'1 → t ⇒β t' → t1 ⇒β t'1
≡subst⇒β ≡.refl ≡.refl x = x

split : ∀ {Γ} {a b} (E : ECxt* Γ a b) {t₁ : Tm Γ a}{t₂ Et₁ : Tm Γ b} →
         Ehole* Et₁ E t₁ → t₁ Redex →
         Et₁ ⇒β t₂ → (∃ λ t₃ → Ehole* t₂ E t₃ × t₁ ⇒β t₃)
         ⊎ (∃ λ E₁ → Ehole* t₂ E₁ t₁ × (∀ t → E [ t ]* ⇒β E₁ [ t ]*))
split ._ [] r t⇒ = inj₁ (_ , [] , t⇒)
split .(appl u ∷ []) (appl u ∷ []) () β
split ._ (appl u ∷ (() ∷ eq)) r β
split ._ (appl u ∷ eq) r (cong (appl .u) (appl .u) t⇒) with split _ eq r t⇒
split ._ (appl u ∷ eq) r (cong (appl .u) (appl .u) t⇒) | inj₁ (x , eq0 , t⇒') = inj₁ (_ , ((appl u) ∷ eq0) , t⇒')
split ._ (_∷_ {Es = Es} (appl u) eq) r (cong (appl .u) (appl .u) t⇒) | inj₂ (Es' , eq0 , f) = inj₂ (_ , ((appl u ∷ eq0) ,
                                                        (λ t → cong (mkHole3 (appl u) {Es}) (mkHole3 (appl u) {Es'}) (f t))))
split ._ (_∷_ {Es = Es} (appl t) eq) r (cong (appr Est) (appr .Est) t⇒) = inj₂ (_ , ((appl _ ∷ eq) ,
      (λ t₁ → ≡subst⇒β (lemma Es {E = appl t}) (lemma Es {E = appl _}) (_⇒β_.cong {E = (appr (Es [ t₁ ]*))} (βEhole.appr (Es [ t₁ ]*)) (appr (Es [ t₁ ]*)) t⇒))))

mutual

-- it seems possible to use sn (Es [ subst (sgs u) t ]*) instead of SN {i} (Es [ subst (sgs u) t ]*) ? - bp
  appsn₃ : ∀ {i a b c Γ} {u : Tm Γ a} {t : Tm (a ∷ Γ) b}{Es : ECxt* Γ b c}{x}
    → sn (Es [ x ]*)
    → sn t
    → SN {i} (Es [ subst (sgs u) t ]*)  -- TODO: use sn here?
    → sn u
    → sn (Es [ app (abs t) u ]*)
  appsn₃ {Es = Es} x t t[u] u = acc (λ t⇒ → help {Es = Es} x t t[u] u (mkEhole* Es) t⇒)
    where
    help : ∀ {i a b c Γ} {u : Tm Γ a} {t : Tm (a ∷ Γ) b} {t' : Tm Γ c} {x}  {z}{Es : ECxt* Γ b c} → sn (Es [ x ]*) → sn t →
         SN {i} (Es [ subst (u ∷s var) t ]*) →
         sn u → Ehole* z Es (app (abs t) u) → z ⇒β t' → sn t'

    help {Es = Es} x t t[u]∈sn u∈sn eq t⇒ with split Es eq β t⇒
    help x t₂ t[u]∈sn u∈sn eq t⇒ | inj₁ (._ , a₁ , β) rewrite hole*→≡ a₁ = fromSN t[u]∈sn
    help {Es = Es} x (acc t₃) t[u]∈sn u∈sn eq t⇒ | inj₁ (._ , a₁ , cong (appl u₁) (appl .u₁) (cong abs abs b₁)) rewrite hole*→≡ a₁
      = appsn₃ {Es = Es} x (t₃ b₁) (mapβSN (cong*3 Es (subst⇒β (sgs u₁) b₁)) t[u]∈sn) u∈sn
    help {t = t} {Es = Es} x t₃ t[u]∈sn (acc u∈sn) eq t⇒ | inj₁ (._ , a₁ , cong (appr ._) (appr ._) b₁) rewrite hole*→≡ a₁
      = appsn₃ {Es = Es} x t₃ (mapβ*SN (cong*4 Es
                                          (subst⇒β* (λ { {._} zero → b₁ ∷ [] ; (suc n) → [] }) t)) t[u]∈sn) (u∈sn b₁)
    help {x = x} (acc f) t₂ t[u]∈sn u∈sn eq t⇒ | inj₂ (Es' , a , g) rewrite hole*→≡ a
         = appsn₃ {Es = Es'} (f (g x)) t₂ (mapβSN (g _) t[u]∈sn) u∈sn

  helperCxt : ∀ {i j Γ a b} {t th to : Tm Γ a}  → (Es : ECxt* Γ a b)
              →       t ⟨ i ⟩⇒ th → SN {j} (Es [ th ]*) → sn (Es [ th ]*) -> t ⇒β to → sn (Es [ to ]*)

  helperCxt E (β 𝒖)    𝒕h 𝑡h β    = 𝑡h

  helperCxt E (β         𝒖) 𝒕h 𝑡h (cong (appl  u) (appl .u) (cong abs abs t⇒))
    = appsn₃ {Es = E} 𝑡h (sn⇒β (antiSubst (subexpsn E 𝑡h)) t⇒)
              (mapβSN (cong*3 E (subst⇒β (sgs u) t⇒)) 𝒕h)
              (fromSN 𝒖)
  helperCxt E (β {t = t} 𝒖) 𝒕h 𝑡h (cong (appr ._) (appr ._) t⇒)
    = appsn₃ {Es = E} 𝑡h (antiSubst (subexpsn E 𝑡h))
              (mapβ*SN (cong*4 E (subst⇒β* (λ { zero → t⇒ ∷ [] ; (suc _) → [] }) t)) 𝒕h)
              (sn⇒β (fromSN 𝒖) t⇒)

  helperCxt E (cong (appl u) (appl .u) (cong () 𝑬𝒕' th⇒)) 𝒕h 𝑡h β

  helperCxt E (cong (appl u) (appl .u) th⇒) 𝒕h 𝑡h       (cong (appl .u) (appl .u) t⇒) = helperCxt (appl u ∷ E) th⇒ 𝒕h 𝑡h t⇒

  helperCxt E (cong (appl u) (appl .u) th⇒) 𝒕h (acc 𝑡h) (cong (appr t)  (appr .t) t⇒)
            = acc (helperCxt [] (E [ cong (appl _) (appl _) th⇒ ]⇒*) (mapβSN t⇒' 𝒕h) (𝑡h t⇒'))
               where
               t⇒' =  E [ cong (appr _) (appr _) t⇒  ]⇒β*

  fromSN : ∀ {i} {Γ} {a} {t : Tm Γ a} → SN {i} t → sn t
  fromSN (ne 𝒏)       = fromSNe 𝒏
  fromSN (abs t₁)     = abssn (fromSN t₁)
  fromSN (exp t⇒ t₁)  = acc (helperCxt [] t⇒ t₁ (fromSN t₁))

  fromSNe : ∀ {i Γ a} {t : Tm Γ a} → SNe {i} t → sn t
  fromSNe (elim 𝒏 E) = acc (elimsn (fromSNe 𝒏) (mapPCxt fromSN E) 𝒏)
  fromSNe (var x)    = varsn x

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


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

module Definition.Typed.Consequences.TypeUnicity where

open import Definition.Untyped hiding (U≢ℕ; U≢Π; U≢ne; ℕ≢Π; ℕ≢ne; Π≢ne; U≢Empty; ℕ≢Empty; Empty≢Π; Empty≢ne)
open import Definition.Untyped.Properties using (subst-Univ-either)
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Equality
import Definition.Typed.Consequences.Inequality as Ineq
open import Definition.Typed.Consequences.Inversion
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.PiNorm
open import Definition.Typed.Consequences.Substitution
open import Definition.Conversion.Stability

open import Tools.Product
open import Tools.Empty
open import Tools.Sum using (_⊎_; inj₁; inj₂)
import Tools.PropositionalEquality as PE

type-uniq : ∀ {Γ t T₁ T₂ r₁ r₂ l₁ l₂} → Γ ⊢ t ∷ T₁ ^ [ r₁ , l₁ ] → Γ ⊢ t ∷ T₂ ^ [ r₂ , l₂ ] →
                 r₁ PE.≡ r₂ × l₁ PE.≡ l₂ × Γ ⊢ T₁ ≡ T₂ ^ [ r₁ , l₁ ]
type-uniq (univ 0<1 x) (univ 0<1 x') = PE.refl , PE.refl , refl (Ugenⱼ x)
type-uniq (ℕⱼ x) (ℕⱼ x₁) = PE.refl , PE.refl , refl (Ugenⱼ x)
type-uniq (Emptyⱼ x) (Emptyⱼ x₁) = PE.refl , PE.refl , refl (Ugenⱼ x)
type-uniq (Πⱼ x ▹ x₁ ▹ X ▹ X₁) (Πⱼ x₂ ▹ x₃ ▹ Y ▹ Y₁) =
    let _ , _ , eU = type-uniq X₁ Y₁
        er , el = Uinjectivity eU
    in PE.refl , PE.refl , PE.subst (λ r → _ ⊢ _ ≡ Univ r _ ^ _ ) er (refl ((Ugenⱼ (wfTerm Y))) )
type-uniq (∃ⱼ X ▹ X₁) (∃ⱼ Y ▹ Y₁) =
    let _ , enextl , eU = type-uniq X Y
        el = next-inj enextl
    in PE.refl , enextl , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _ ) el (refl ((Ugenⱼ (wfTerm Y))) )
type-uniq (var xx x) (var _ y) =
    let T≡T , e = varTypeEq′ x y
        er , el = typelevel-injectivity e
    in er , el , PE.subst (λ A → _ ⊢ _ ≡ A ^ _ ) T≡T (refl (syntacticTerm (var xx x)))
type-uniq (lamⱼ x x₁ x₂ X) (lamⱼ y y₁ y₂ Y) =
    let _ , _ , F≡F = type-uniq (un-univ x₂) (un-univ y₂)
        erF , elF = Uinjectivity F≡F
        erG , elG , G≡G = type-uniq X (PE.subst₂ (λ r l → _ ∙ _ ^ [ r , ι l ] ⊢ _ ∷ _ ^ _) (PE.sym erF) (PE.sym elF) Y)
    in erG , PE.refl , PE.subst₃ (λ rF lF lG → _ ⊢ _ ≡  Π _ ^ rF ° lF ▹ _ ° lG ° _ ^ _) erF elF (ιinj elG)
                                 (univ (Π-cong x x₁ x₂ (refl (un-univ x₂)) (un-univ≡ G≡G)))
type-uniq (X ∘ⱼ X₁) (Y ∘ⱼ Y₁) =
    let er , _ , Π≡Π = type-uniq X Y
        F≡F , erF , elF , elG , G≡G = injectivity Π≡Π
    in er , PE.cong _ elG , (substitutionEq G≡G (substRefl (singleSubst X₁)) (wfTerm X₁))
type-uniq {Γ} ⦅ x , x₁ , X , X₁ ⦆ⱼ (⦅_,_,_,_⦆ⱼ {F = F} {G = G} y y₁ Y Y₁)  =
    let _ , el , F≡F = type-uniq X Y
        _ , el' , G≡G = type-uniq (un-univ x₁) (un-univ (stability (reflConEq (wf x) ∙ sym F≡F)
                                                         (PE.subst (λ l → Γ ∙ F ^ [ % , l ] ⊢ G ^ [ % , l ]) (PE.sym el) y₁)))
    in PE.refl , el , univ (∃-cong x (un-univ≡ F≡F) (un-univ≡ (refl x₁)))
type-uniq (fstⱼ X X₁ X₂) (fstⱼ Y Y₁ Y₂) =
    let er , el , ∃≡∃ = type-uniq X₂ Y₂
        F≡F , _ = ∃injectivity ∃≡∃
    in PE.refl , el , F≡F
type-uniq (sndⱼ X X₁ X₂) (sndⱼ Y Y₁ Y₂) =
    let er , el , ∃≡∃ = type-uniq X₂ Y₂
        F≡F , G≡G = ∃injectivity ∃≡∃
    in PE.refl , el , substitutionEq G≡G (substRefl (singleSubst (fstⱼ X X₁ X₂))) (wfTerm X)
type-uniq (zeroⱼ x) (zeroⱼ x₁) = PE.refl , PE.refl , refl (univ (ℕⱼ x))
type-uniq (sucⱼ X) (sucⱼ Y) = PE.refl , PE.refl , refl (univ (ℕⱼ (wfTerm X)))
type-uniq (natrecⱼ x X X₁ X₂) (natrecⱼ y Y Y₁ Y₂) =
    let _ , _ , U≡U = type-uniq (un-univ x) (un-univ y)
        er , _ = Uinjectivity U≡U
    in er , PE.refl , refl (substitution x (singleSubst X₂) (wfTerm X) )
type-uniq (Emptyrecⱼ x X) (Emptyrecⱼ y Y) =
    let _ , _ , U≡U = type-uniq (un-univ x) (un-univ y)
        er , _ = Uinjectivity U≡U
    in er , PE.refl , refl x
type-uniq (Idⱼ X X₁ X₂) (Idⱼ Y Y₁ Y₂) =
    let _ , enl , U≡U = type-uniq X Y
        el = next-inj enl
    in PE.refl , enl , PE.subst (λ l → _ ⊢ _ ≡ SProp l ^ _) el (refl (Ugenⱼ (wfTerm X)))
type-uniq (Idreflⱼ X) (Idreflⱼ Y) =
    let _ , el , _ = type-uniq X Y
    in PE.refl , el , refl (syntacticTerm (Idreflⱼ X))
type-uniq (transpⱼ x x₁ X X₁ X₂ X₃) (transpⱼ x₂ x₃ Y Y₁ Y₂ Y₃) =
    let _ , el , _ = type-uniq X Y
    in PE.refl , el , refl (substitution x₁ (singleSubst X₂) (wfTerm X))
type-uniq (castⱼ X X₁ X₂ X₃) (castⱼ Y Y₁ Y₂ Y₃) =
    let er , _ , _ = type-uniq X₃ Y₃
    in er , PE.refl , refl (univ X₁)
type-uniq (castreflⱼ X X₁) (castreflⱼ Y Y₁) = PE.refl , PE.refl , refl (syntacticTerm (castreflⱼ X X₁))
type-uniq (conv X x) Y = let er , el , eA = type-uniq X Y in er , el , trans (sym x) eA
type-uniq X (conv Y y) =
    let er , el , eA = type-uniq X Y
    in er , el , trans eA (PE.subst₂ (λ r l → _ ⊢ _ ≡ _ ^ [ r , l ]) (PE.sym er) (PE.sym el) y)

ext: agda

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
import Data.Empty
import Data.Unit
import Data.Bool
import Data.Nat
import Data.Fin

module SecondOrder.Arity where

  -- A notion of arity is given by a set of possible arities, and a mapping which to each arity assings a set of
  -- argument positions.

  record Arity : Set₁ where
    field
      arity : Set -- the set of permissible arities, e.g., ℕ for finitary arities
      arg : arity → Set -- every arity gives a set of argument (position), e.g. Fin

  -- finitary arities
  arity-finite : Arity
  arity-finite = record { arity = Data.Nat.ℕ ; arg = Data.Fin.Fin }

  module Arity012 where
    -- For example, in algebra we quite often only consider constants, unary and binary
    -- operations. Thus we would only need three arities.

    data arity012 : Set where
      Constant Unary Binary : arity012

    arg012 : arity012 → Set
    arg012 Constant = Data.Empty.⊥
    arg012 Unary = Data.Unit.⊤
    arg012 Binary = Data.Bool.Bool

    arity-012 : Arity
    arity-012 = record { arity =  arity012 ; arg = arg012 }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------------
-- Paradoxical combinator properties
------------------------------------------------------------------------------

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

-- See (Barendregt 2004, corollary 6.1.3).

module FOT.LTC-PCF.Y.Properties where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOT.LTC-PCF.Y

open import LTC-PCF.Base hiding ( fix ; fix-eq )
open import LTC-PCF.Base.Properties

------------------------------------------------------------------------------
-- The conversion rule for Y.
Y-eq : ∀ f → Y · f ≡ f · (Y · f)
Y-eq f = Y · f             ≡⟨ beta helper f ⟩
         lamW · lamW       ≡⟨ beta W lamW ⟩
         W lamW            ≡⟨ refl ⟩
         f · (lamW · lamW) ≡⟨ ·-rightCong (sym (beta helper f)) ⟩
         f · (Y · f)       ∎
  where
  helper : D → D
  helper = λ f → lam (λ x → f · (x · x)) · lam (λ x → f · (x · x))

  W : D → D
  W = λ x → f · (x · x)

  lamW : D
  lamW = lam W

-- The conversion rule for the higher-order Y₁.
Y₁-eq : (f : D → D) → Y₁ f ≡ f (Y₁ f)
Y₁-eq f = Y₁ f                ≡⟨ refl ⟩
          Y · lam f           ≡⟨ Y-eq (lam f) ⟩
          lam f · (Y · lam f) ≡⟨ ·-rightCong refl ⟩
          lam f · Y₁ f        ≡⟨ beta f (Y₁ f) ⟩
          f (Y₁ f)            ∎

------------------------------------------------------------------------------
-- References
--
-- Barendregt, Henk (2004). The Lambda Calculus. Its Syntax and
-- Semantics. 2nd ed. Vol. 103. Studies in Logic and the Foundations
-- of Mathematics. 6th impression. Elsevier.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
--------------------------------------------------------------------------------
-- Strings with markers, used for parsing
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module Parse.MarkedString where

open import Data.String using (fromList; fromChar; toList)

open import Prelude

data Marker : Set where
  NonTerminalBracket : Bool → Marker
  NameDivider : Marker
  WildcardBracket : Bool → Marker
  WildcardSeparator : Marker

instance
  Marker-Show : Show Marker
  Marker-Show = record { show = λ where
    (NonTerminalBracket true)  → "NonTerminalBracket"
    (NonTerminalBracket false) → "IgnoredNonTerminalBracket"
    NameDivider                → "NameDivider"
    (WildcardBracket true)     → "BlacklistWildcardBracket"
    (WildcardBracket false)    → "WhitelistWildcardBracket"
    WildcardSeparator          → "WildcardSeparator" }

  Marker-Eq : Eq Marker
  Marker-Eq = record { _≟_ = λ where
    (NonTerminalBracket x) (NonTerminalBracket x₁) →
      case x ≟ x₁ of λ { (yes refl) → yes refl ; (no ¬p) → no (λ { refl → ¬p refl }) }
    (NonTerminalBracket x) NameDivider → no (λ ())
    (NonTerminalBracket x) (WildcardBracket x₁) → no (λ ())
    (NonTerminalBracket x) WildcardSeparator → no (λ ())
    NameDivider (NonTerminalBracket x) → no (λ ())
    NameDivider NameDivider → yes refl
    NameDivider (WildcardBracket x) → no (λ ())
    NameDivider WildcardSeparator → no (λ ())
    (WildcardBracket x) (NonTerminalBracket x₁) → no (λ ())
    (WildcardBracket x) NameDivider → no (λ ())
    (WildcardBracket x) (WildcardBracket x₁) →
      case x ≟ x₁ of λ { (yes refl) → yes refl ; (no ¬p) → no (λ { refl → ¬p refl }) }
    (WildcardBracket x) WildcardSeparator → no (λ ())
    WildcardSeparator (NonTerminalBracket x) → no (λ ())
    WildcardSeparator NameDivider → no (λ ())
    WildcardSeparator (WildcardBracket x) → no (λ ())
    WildcardSeparator WildcardSeparator → yes refl }

  Marker-EqB = Eq→EqB {{Marker-Eq}}

enumerateMarkers : List Marker
enumerateMarkers =
  NonTerminalBracket true  ∷
  NonTerminalBracket false ∷
  NameDivider              ∷
  WildcardBracket true     ∷
  WildcardBracket false    ∷
  WildcardSeparator        ∷ []

markerRepresentation : Marker → Char
markerRepresentation (NonTerminalBracket true)  = '_'
markerRepresentation (NonTerminalBracket false) = '^'
markerRepresentation NameDivider                = '$'
markerRepresentation (WildcardBracket true)     = '!'
markerRepresentation (WildcardBracket false)    = '@'
markerRepresentation WildcardSeparator          = '&'
-- other good candidates: &*#~%

escapeMarker = '\\'

MarkedChar = Char ⊎ Marker
MarkedString = List MarkedChar

markedStringToString : MarkedString → String
markedStringToString [] = ""
markedStringToString (inj₁ x ∷ s) =
  fromList (decCase x of
    map (λ x → (x , escapeMarker ∷ [ x ])) $
      -- if we find anything in this list, escape it
      escapeMarker ∷ map markerRepresentation enumerateMarkers
    default [ x ])
    + markedStringToString s
markedStringToString (inj₂ x ∷ s) = (fromChar $ markerRepresentation x) + markedStringToString s

convertToMarked : String → MarkedString
convertToMarked s = helper false (toList s)
  where
    -- first argument is whether the current character is escaped
    helper : Bool → List Char → MarkedString
    helper _     []      = []
    helper false (x ∷ l) =
      decCase x of
        (escapeMarker , helper true l) ∷
        map (λ y → (markerRepresentation y , inj₂ y ∷ helper false l)) enumerateMarkers
        default (inj₁ x ∷ helper false l)
    helper true  (x ∷ l) = inj₁ x ∷ helper false l

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax where

infixl 2 _▻_
infixl 3 _‘’_
infixl 3 _‘’₁_
infixl 3 _‘’₂_
infixl 3 _‘’₃_
infixl 3 _‘’ₐ_
infixr 1 _‘→’_
infixl 3 _‘‘’’_
infixl 3 _w‘‘’’_
infixr 1 _‘‘→'’’_
infixr 1 _w‘‘→'’’_

mutual
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Typ Γ → Context

  data Typ : Context → Set where
    _‘’_ : ∀ {Γ A} → Typ (Γ ▻ A) → Term {Γ} A → Typ Γ
    _‘’₁_ : ∀ {Γ A B} → (C : Typ (Γ ▻ A ▻ B)) → (a : Term {Γ} A) → Typ (Γ ▻ B ‘’ a)
    _‘’₂_ : ∀ {Γ A B C} → (D : Typ (Γ ▻ A ▻ B ▻ C)) → (a : Term {Γ} A) → Typ (Γ ▻ B ‘’ a ▻ C ‘’₁ a)
    _‘’₃_ : ∀ {Γ A B C D} → (E : Typ (Γ ▻ A ▻ B ▻ C ▻ D)) → (a : Term {Γ} A) → Typ (Γ ▻ B ‘’ a ▻ C ‘’₁ a ▻ D ‘’₂ a)
    W : ∀ {Γ A} → Typ Γ → Typ (Γ ▻ A)
    W1 : ∀ {Γ A B} → Typ (Γ ▻ B) → Typ (Γ ▻ A ▻ (W {Γ = Γ} {A = A} B))
    W2 : ∀ {Γ A B C} → Typ (Γ ▻ B ▻ C) → Typ (Γ ▻ A ▻ W B ▻ W1 C)
    _‘→’_ : ∀ {Γ} (A : Typ Γ) → Typ (Γ ▻ A) → Typ Γ
    ‘Σ’ : ∀ {Γ} (T : Typ Γ) → Typ (Γ ▻ T) → Typ Γ
    ‘Context’ : ∀ {Γ} → Typ Γ
    ‘Typ’ : ∀ {Γ} → Typ (Γ ▻ ‘Context’)
    ‘Term’ : ∀ {Γ} → Typ (Γ ▻ ‘Context’ ▻ ‘Typ’)

  data Term : ∀ {Γ} → Typ Γ → Set where
    w : ∀ {Γ A B} → Term {Γ} B → Term {Γ = Γ ▻ A} (W {Γ = Γ} {A = A} B)
    ‘λ∙’ : ∀ {Γ A B} → Term {Γ = (Γ ▻ A)} B → Term {Γ} (A ‘→’ B)
    _‘’ₐ_ : ∀ {Γ A B} → (f : Term {Γ} (A ‘→’ B)) → (x : Term {Γ} A) → Term {Γ} (B ‘’ x)
    ‘VAR₀’ : ∀ {Γ T} → Term {Γ = Γ ▻ T} (W T)
    ⌜_⌝c : ∀ {Γ} → Context → Term {Γ} ‘Context’
    ⌜_⌝T : ∀ {Γ Γ'} → Typ Γ' → Term {Γ} (‘Typ’ ‘’ ⌜ Γ' ⌝c)
    ⌜_⌝t : ∀ {Γ Γ'} {T : Typ Γ'} → Term T → Term {Γ} (‘Term’ ‘’₁ ⌜ Γ' ⌝c ‘’ ⌜ T ⌝T)
    ‘quote-term’ : ∀ {Γ Γ'} {A : Typ Γ'} → Term {Γ} (‘Term’ ‘’₁ ⌜ Γ' ⌝c ‘’ ⌜ A ⌝T ‘→’ W (‘Term’ ‘’₁ ⌜ Γ ⌝c ‘’ ⌜ ‘Term’ ‘’₁ ⌜ Γ' ⌝c ‘’ ⌜ A ⌝T ⌝T))
    ‘quote-sigma’ : ∀ {Γ Γ'} → Term {Γ} (‘Σ’ ‘Context’ ‘Typ’ ‘→’ W (‘Term’ ‘’₁ ⌜ Γ' ⌝c ‘’ ⌜ ‘Σ’ ‘Context’ ‘Typ’ ⌝T))
    {-‘substTyp’ : ∀ {Γ' Γ} {A : Typ Γ}
      → Term {Γ'} (‘Typ’ ‘’ ⌜ Γ ▻ A ⌝c
                  ‘→’ W (‘Term’ ‘’₁ ⌜ Γ ⌝c ‘’ ⌜ A ⌝T
                  ‘→’ W (‘Typ’ ‘’ ⌜ Γ ⌝c)))-}
    ‘cast’ : Term {ε} (‘Σ’ ‘Context’ ‘Typ’ ‘→’ W (‘Typ’ ‘’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c))
    SW : ∀ {Γ A B} {a : Term {Γ} A} → Term {Γ} (W B ‘’ a) → Term {Γ} B
    weakenTyp-substTyp-tProd : ∀ {Γ T T' A B} {a : Term {Γ} T} → Term {Γ = Γ ▻ T'} (W ((A ‘→’ B) ‘’ a)) → Term {Γ ▻ T'} (W ((A ‘’ a) ‘→’ (B ‘’₁ a)))
    substTyp-weakenTyp1-VAR₀ : ∀ {Γ A T} → Term {Γ ▻ A} (W1 T ‘’ ‘VAR₀’) → Term {Γ ▻ A} T
    weakenTyp-tProd : ∀ {Γ A B C} → Term {Γ = Γ ▻ C} (W (A ‘→’ B)) → Term {Γ = Γ ▻ C} (W A ‘→’ W1 B)
    weakenTyp-tProd-inv : ∀ {Γ A B C} → Term {Γ = Γ ▻ C} (W A ‘→’ W1 B) → Term {Γ = Γ ▻ C} (W (A ‘→’ B))
    weakenTyp-weakenTyp-tProd : ∀ {Γ A B C D} → Term {Γ ▻ C ▻ D} (W (W (A ‘→’ B))) → Term {Γ ▻ C ▻ D} (W (W A ‘→’ W1 B))
    substTyp1-tProd : ∀ {Γ T T' A B} {a : Term {Γ} T} → Term {Γ ▻ T' ‘’ a} ((A ‘→’ B) ‘’₁ a) → Term {Γ ▻ T' ‘’ a} ((A ‘’₁ a) ‘→’ (B ‘’₂ a))
    weakenTyp1-tProd : ∀ {Γ C D A B} → Term {Γ ▻ C ▻ W D} (W1 (A ‘→’ B)) → Term {Γ ▻ C ▻ W D} (W1 A ‘→’ W2 B)
    substTyp2-tProd : ∀ {Γ T T' T'' A B} {a : Term {Γ} T} → Term {Γ ▻ T' ‘’ a ▻ T'' ‘’₁ a} ((A ‘→’ B) ‘’₂ a) → Term {Γ ▻ T' ‘’ a ▻ T'' ‘’₁ a} ((A ‘’₂ a) ‘→’ (B ‘’₃ a))
    substTyp1-substTyp-weakenTyp-inv : ∀ {Γ C T A} {a : Term {Γ} C} {b : Term {Γ} (T ‘’ a)} → Term {Γ} (A ‘’ a) → Term {Γ} (W A ‘’₁ a ‘’ b)
    substTyp1-substTyp-weakenTyp : ∀ {Γ C T A} {a : Term {Γ} C} {b : Term {Γ} (T ‘’ a)} → Term {Γ} (W A ‘’₁ a ‘’ b) → Term {Γ} (A ‘’ a)
    weakenTyp-weakenTyp-substTyp1-substTyp-weakenTyp : ∀ {Γ C T A D E} {a : Term {Γ} C} {b : Term {Γ} (T ‘’ a)} → Term {Γ ▻ D ▻ E} (W (W (W A ‘’₁ a ‘’ b))) → Term {Γ ▻ D ▻ E} (W (W (A ‘’ a)))
    weakenTyp-substTyp2-substTyp1-substTyp-weakenTyp-inv : ∀ {Γ A B C T T'} {a : Term {Γ} A} {b : Term {Γ} (B ‘’ a)} {c : Term {Γ} (C ‘’₁ a ‘’ b)}
      → Term {Γ ▻ T'} (W (T ‘’₁ a ‘’ b))
      → Term {Γ ▻ T'} (W (W T ‘’₂ a ‘’₁ b ‘’ c))
    substTyp2-substTyp1-substTyp-weakenTyp : ∀ {Γ A B C T} {a : Term {Γ} A} {b : Term {Γ} (B ‘’ a)} {c : Term {Γ} (C ‘’₁ a ‘’ b)}
      → Term {Γ} (W T ‘’₂ a ‘’₁ b ‘’ c)
      → Term {Γ} (T ‘’₁ a ‘’ b)
    weakenTyp-substTyp2-substTyp1-substTyp-tProd : ∀ {Γ T T' T'' T''' A B} {a : Term {Γ} T} {b : Term {Γ} (T' ‘’ a)} {c : Term {Γ} (T'' ‘’₁ a ‘’ b)}
      → Term {Γ ▻ T'''} (W ((A ‘→’ B) ‘’₂ a ‘’₁ b ‘’ c))
      → Term {Γ ▻ T'''} ((W (A ‘’₂ a ‘’₁ b ‘’ c)) ‘→’ (W1 (B ‘’₃ a ‘’₂ b ‘’₁ c)))
    weakenTyp2-weakenTyp1 : ∀ {Γ A B C D} → Term {Γ ▻ A ▻ W B ▻ W1 C} (W2 (W D)) → Term {Γ ▻ A ▻ W B ▻ W1 C} (W (W1 D))
    weakenTyp1-weakenTyp : ∀ {Γ A B C} → Term {Γ ▻ A ▻ W B} (W1 (W C)) → Term {Γ ▻ A ▻ W B} (W (W C))
    weakenTyp1-weakenTyp-inv : ∀ {Γ A B C} → Term {Γ ▻ A ▻ W B} (W (W C)) → Term {Γ ▻ A ▻ W B} (W1 (W C))
    weakenTyp1-weakenTyp1-weakenTyp : ∀ {Γ A B C T} → Term {Γ ▻ A ▻ B ▻ W (W C)} (W1 (W1 (W T))) → Term {Γ ▻ A ▻ B ▻ W (W C)} (W1 (W (W T)))
    substTyp1-weakenTyp1 : ∀ {Γ A B C} {a : Term {Γ} A} → Term {Γ ▻ W B ‘’ a} (W1 C ‘’₁ a) → Term {Γ ▻ B} C
    weakenTyp1-substTyp-weakenTyp1-inv : ∀ {Γ A T'' T' T} {a : Term {Γ} A}
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W (T ‘’ a)))
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W T ‘’₁ a))
    weakenTyp1-substTyp-weakenTyp1 : ∀ {Γ A T'' T' T} {a : Term {Γ} A}
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W T ‘’₁ a))
      → Term {Γ ▻ T'' ▻ W (T' ‘’ a)} (W1 (W (T ‘’ a)))
    weakenTyp-substTyp-substTyp-weakenTyp1 : ∀ {Γ T' B A} {b : Term {Γ} B} {a : Term {Γ ▻ B} (W A)} {T : Typ (Γ ▻ A)}
      → Term {Γ ▻ T'} (W (W1 T ‘’ a ‘’ b))
      → Term {Γ ▻ T'} (W (T ‘’ (SW ((‘λ∙’ a) ‘’ₐ b))))
    weakenTyp-substTyp-substTyp-weakenTyp1-inv : ∀ {Γ T' B A} {b : Term {Γ} B} {a : Term {Γ ▻ B} (W A)} {T : Typ (Γ ▻ A)}
      → Term {Γ ▻ T'} (W (T ‘’ (SW ((‘λ∙’ a) ‘’ₐ b))))
      → Term {Γ ▻ T'} (W (W1 T ‘’ a ‘’ b))
    substTyp-weakenTyp1-weakenTyp : ∀ {Γ T} {A : Typ Γ} {B : Typ Γ}
      → {a : Term {Γ = Γ ▻ T} (W {Γ = Γ} {A = T} B)}
      → Term {Γ = Γ ▻ T} (W1 (W A) ‘’ a)
      → Term {Γ = Γ ▻ T} (W A)
    substTyp3-substTyp2-substTyp1-substTyp-weakenTyp : ∀ {Γ A B C D T T'} {a : Term {Γ} A} {b : Term {Γ} (B ‘’ a)} {c : Term {Γ} (C ‘’₁ a ‘’ b)}
         {d : Term {Γ = (Γ ▻ T')} (W (D ‘’₂ a ‘’₁ b ‘’ c))}
         → Term {Γ = (Γ ▻ T')} (W1 (W T ‘’₃ a ‘’₂ b ‘’₁ c) ‘’ d)
         → Term {Γ = (Γ ▻ T')} (W (T ‘’₂ a ‘’₁ b ‘’ c))
    weakenTyp-substTyp2-substTyp1-substTyp-weakenTyp1 : ∀ {Γ A B C T T'} {a : Term {Γ} A} {b : Term (B ‘’ a)} {c : Term (C ‘’ a)}
      → Term {Γ = (Γ ▻ T')} (W (W1 T ‘’₂ a ‘’₁ b ‘’ substTyp1-substTyp-weakenTyp-inv c))
      → Term {Γ = (Γ ▻ T')} (W (T ‘’₁ a ‘’ c))
    substTyp1-substTyp-tProd : ∀ {Γ T T' A B a b} → Term ((_‘→’_ {Γ = Γ ▻ T ▻ T'} A B) ‘’₁ a ‘’ b) → Term (_‘→’_ {Γ = Γ} (A ‘’₁ a ‘’ b) (B ‘’₂ a ‘’₁ b))
    substTyp2-substTyp-substTyp-weakenTyp1-weakenTyp-weakenTyp : ∀ {Γ A} {T : Typ (Γ ▻ A)} {T' C B} {a : Term {Γ} A} {b : Term {Γ = (Γ ▻ C ‘’ a)} (B ‘’₁ a)}
         {c : Term {Γ = (Γ ▻ T')} (W (C ‘’ a))}
         → Term {Γ = (Γ ▻ T')} (W1 (W (W T) ‘’₂ a ‘’ b) ‘’ c)
         → Term {Γ = (Γ ▻ T')} (W (T ‘’ a))
    substTyp1-substTyp-weakenTyp2-weakenTyp : ∀ {Γ T' A B T} {a : Term {Γ ▻ T'} (W A)} {b : Term {Γ ▻ T'} (W1 B ‘’ a)}
      → Term {Γ ▻ T'} (W2 (W T) ‘’₁ a ‘’ b)
      → Term {Γ ▻ T'} (W1 T ‘’ a)
    weakenTyp-weakenTyp1-weakenTyp : ∀ {Γ A B C D} → Term {Γ ▻ A ▻ W B ▻ W1 C} (W (W1 (W D))) → Term {Γ ▻ A ▻ W B ▻ W1 C} (W (W (W D)))
    beta-under-subst : ∀ {Γ A B B'} {g : Term {Γ} (A ‘→’ W B)} {x : Term {Γ} A}
      → Term (B' ‘’ SW (‘λ∙’ (SW (‘λ∙’ (weakenTyp1-weakenTyp (substTyp-weakenTyp1-VAR₀ (weakenTyp-tProd (w (weakenTyp-tProd (w g))) ‘’ₐ ‘VAR₀’))) ‘’ₐ ‘VAR₀’)) ‘’ₐ x))
      → Term (B' ‘’ SW (g ‘’ₐ x))
    ‘proj₁'’ : ∀ {Γ} {T : Typ Γ} {P : Typ (Γ ▻ T)} → Term (‘Σ’ T P ‘→’ W T)
    ‘proj₂'’ : ∀ {Γ} {T : Typ Γ} {P : Typ (Γ ▻ T)} → Term {Γ ▻ ‘Σ’ T P} (W1 P ‘’ SW (‘λ∙’ (weakenTyp1-weakenTyp (substTyp-weakenTyp1-VAR₀ (weakenTyp-tProd (w (weakenTyp-tProd (w ‘proj₁'’))) ‘’ₐ ‘VAR₀’))) ‘’ₐ ‘VAR₀’))
    ‘existT’ : ∀ {Γ T P} (x : Term {Γ} T) (p : Term (P ‘’ x)) → Term (‘Σ’ T P)
    {- these are redundant, but useful for not having to normalize the subsequent ones -}
    _‘‘’’_ : ∀ {Γ} {A : Typ Γ}
      → Term {ε} (‘Typ’ ‘’ ⌜ Γ ▻ A ⌝c)
      → Term {ε} (‘Term’ ‘’₁ ⌜ Γ ⌝c ‘’ ⌜ A ⌝T)
      → Term {ε} (‘Typ’ ‘’ ⌜ Γ ⌝c)
    _w‘‘’’_ : ∀ {X Γ} {A : Typ Γ}
      → Term {ε ▻ X} (W (‘Typ’ ‘’ ⌜ Γ ▻ A ⌝c))
      → Term {ε ▻ X} (W (‘Term’ ‘’₁ ⌜ Γ ⌝c ‘’ ⌜ A ⌝T))
      → Term {ε ▻ X} (W (‘Typ’ ‘’ ⌜ Γ ⌝c))
    _‘‘→'’’_ : ∀ {Γ}
      → Term {ε} (‘Typ’ ‘’ Γ)
      → Term {ε} (‘Typ’ ‘’ Γ)
      → Term {ε} (‘Typ’ ‘’ Γ)
    _w‘‘→'’’_ : ∀ {X Γ}
      → Term {ε ▻ X} (W (‘Typ’ ‘’ Γ))
      → Term {ε ▻ X} (W (‘Typ’ ‘’ Γ))
      → Term {ε ▻ X} (W (‘Typ’ ‘’ Γ))
    w→ : ∀ {Γ A B C} → Term (A ‘→’ W B) → Term {Γ = Γ ▻ C} (W A ‘→’ W (W B))
    {- things that were postulates, but are no longer -}
    ‘‘→'’’→w‘‘→'’’ : ∀ {T'}
         {b : Term {ε} (‘Typ’ ‘’ ⌜ ε ⌝c)}
         {c : Term {ε ▻ T'} (W (‘Typ’ ‘’ ⌜ ε ⌝c))}
         {e : Term {ε} T'}
         → Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (SW (‘λ∙’ (c w‘‘→'’’ w b) ‘’ₐ e))
                    ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (SW (‘λ∙’ c ‘’ₐ e) ‘‘→'’’ b)))
    w‘‘→'’’→‘‘→'’’ : ∀ {T'}
         {b : Term {ε} (‘Typ’ ‘’ ⌜ ε ⌝c)}
         {c : Term {ε ▻ T'} (W (‘Typ’ ‘’ ⌜ ε ⌝c))}
         {e : Term {ε} T'}
         → Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (SW (‘λ∙’ c ‘’ₐ e) ‘‘→'’’ b)
                    ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (SW (‘λ∙’ (c w‘‘→'’’ w b) ‘’ₐ e))))
    ‘tApp-nd’ : ∀ {Γ} {A : Term {ε} (‘Typ’ ‘’ Γ)} {B : Term {ε} (‘Typ’ ‘’ Γ)} →
      Term {ε} (‘Term’ ‘’₁ Γ ‘’ (A ‘‘→'’’ B)
           ‘→’ W (‘Term’ ‘’₁ Γ ‘’ A
           ‘→’ W (‘Term’ ‘’₁ Γ ‘’ B)))
    ⌜←'⌝ : ∀ {H X} →
      Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (⌜ H ⌝T ‘‘→'’’ ⌜ X ⌝T)
           ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ ⌜ H ‘→’ W X ⌝T))
    ⌜→'⌝ : ∀ {H X} →
      Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ ⌜ H ‘→’ W X ⌝T
           ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (⌜ H ⌝T ‘‘→'’’ ⌜ X ⌝T)))
    ‘‘fcomp-nd’’ : ∀ {A B C} →
      Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (A ‘‘→'’’ C)
           ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (C ‘‘→'’’ B)
           ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ (A ‘‘→'’’ B))))
    ⌜‘’⌝ : ∀ {B A} {b : Term {ε} B} →
        Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’
            (⌜ A ‘’ b ⌝T ‘‘→'’’ ⌜ A ⌝T ‘‘’’ ⌜ b ⌝t))
    ⌜‘’⌝' : ∀ {B A} {b : Term {ε} B} →
        Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’
            (⌜ A ⌝T ‘‘’’ ⌜ b ⌝t ‘‘→'’’ ⌜ A ‘’ b ⌝T))
    ‘cast-refl’ : ∀ {T : Typ (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)} →
        Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’
            ((⌜ T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T ⌝T)
               ‘‘→'’’
               (SW (‘cast’ ‘’ₐ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T)
                 ‘‘’’ SW (‘quote-sigma’ ‘’ₐ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T))))
    ‘cast-refl'’ : ∀ {T : Typ (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)} →
        Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’
            ((SW (‘cast’ ‘’ₐ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T)
                 ‘‘’’ SW (‘quote-sigma’ ‘’ₐ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T))
               ‘‘→'’’
               (⌜ T ‘’ ‘existT’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c ⌜ T ⌝T ⌝T)))
    ‘s→→’ : ∀ {T B}
           {b : Term {ε} (T ‘→’ W (‘Typ’ ‘’ ⌜ ε ▻ B ⌝c))}
           {c : Term {ε} (T ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ ⌜ B ⌝T))}
           {v : Term {ε} T} →
      (Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c
           ‘’ ((SW (((‘λ∙’ (SW (w→ b ‘’ₐ ‘VAR₀’) w‘‘’’ SW (w→ c ‘’ₐ ‘VAR₀’)) ‘’ₐ v))))
                 ‘‘→'’’ (SW (b ‘’ₐ v) ‘‘’’ SW (c ‘’ₐ v)))))
    ‘s←←’ : ∀ {T B}
           {b : Term {ε} (T ‘→’ W (‘Typ’ ‘’ ⌜ ε ▻ B ⌝c))}
           {c : Term {ε} (T ‘→’ W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ ⌜ B ⌝T))}
           {v : Term {ε} T} →
      (Term {ε} (‘Term’ ‘’₁ ⌜ ε ⌝c
           ‘’ ((SW (b ‘’ₐ v) ‘‘’’ SW (c ‘’ₐ v))
                 ‘‘→'’’ (SW (((‘λ∙’ (SW (w→ b ‘’ₐ ‘VAR₀’) w‘‘’’ SW (w→ c ‘’ₐ ‘VAR₀’)) ‘’ₐ v)))))))

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


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

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.FinData

open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.QuotientRing renaming (_/_ to _/Ring_) hiding (asRing)

private
  variable
    ℓ ℓ' : Level

_/_ : (R : CommRing ℓ) → (I : IdealsIn R) → CommRing ℓ
R / I =
  fst asRing , commringstr _ _ _ _ _
                 (iscommring (RingStr.isRing (snd asRing))
                             (elimProp2 (λ _ _ → squash/ _ _)
                                        commEq))
   where
       asRing = (CommRing→Ring R) /Ring (CommIdeal→Ideal I)
       _·/_ : fst asRing → fst asRing → fst asRing
       _·/_ = RingStr._·_ (snd asRing)
       commEq : (x y : fst R) → ([ x ] ·/ [ y ]) ≡ ([ y ] ·/ [ x ])
       commEq x y i = [ CommRingStr.·Comm (snd R) x y i ]

[_]/ : {R : CommRing ℓ} {I : IdealsIn R} → (a : fst R) → fst (R / I)
[ a ]/ = [ a ]

--

module Quotient-FGideal-CommRing-Ring
  (A'@(A , Ar) : CommRing ℓ)
  (B'@(B , Br) : Ring ℓ')
  (g'@(g , gr) : RingHom (CommRing→Ring A') B')
  where

  open CommRingStr Ar using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_ )

  open RingStr Br using ()
    renaming
    ( 0r        to 0B
    ; 1r        to 1B
    ; _+_       to _+B_
    ; -_        to -B_
    ; _·_       to _·B_
    ; +Lid     to +BIdL
    ; is-set    to isSetB)

  open CommRingStr
  open IsRingHom

  module _
    {n : ℕ}
    (v : FinVec A n)
    (gnull : (k : Fin n) → g ( v k) ≡ 0B)
    where

    f : RingHom (CommRing→Ring (A' / (generatedIdeal _ v))) B'
    fst f = SQ.rec (isSetB)
            g
            λ a b → PT.rec (isSetB _ _)
                     λ x → g a                                   ≡⟨ cong g (sym (+Rid Ar a)) ⟩
                     g (a +A 0A)                                  ≡⟨ cong (λ X → g (a +A X)) (sym (snd (+Inv Ar b))) ⟩
                     g (a +A ((-A b) +A b))                       ≡⟨ cong g (+Assoc Ar a (-A b) b) ⟩
                     g ((a +A -A b) +A b)                         ≡⟨ pres+ gr (a +A -A b) b ⟩
                     (g(a +A -A b) +B g b)                        ≡⟨ cong (λ X → g X +B g b) (snd x) ⟩
                     (g (linearCombination A' (fst x) v) +B g b)  ≡⟨ cong (λ X → X +B g b) (cancelLinearCombination A' B' g' n (fst x) v gnull) ⟩
                     0B +B g b                                    ≡⟨ +BIdL (g b) ⟩
                     g b ∎
    snd f = makeIsRingHom
            (pres1 gr)
            (elimProp (λ x p q i y j → isSetB _ _ (p y) (q y) i j)
                      λ a → elimProp (λ _ → isSetB _ _)
                             λ a' → pres+ gr a a')
            (elimProp (λ x p q i y j → isSetB _ _ (p y) (q y) i j)
                      λ a → elimProp (λ _ → isSetB _ _)
                             λ a' → pres· gr a a')

module Quotient-FGideal-CommRing-CommRing
  (A'@(A , Ar) : CommRing ℓ)
  (B'@(B , Br) : CommRing ℓ')
  (g'@(g , gr) : CommRingHom A' B')
  {n : ℕ}
  (v : FinVec A n)
  (gnull : (k : Fin n) → g ( v k) ≡ CommRingStr.0r (snd B'))
  where

  f : CommRingHom (A' / (generatedIdeal _ v)) B'
  f = Quotient-FGideal-CommRing-Ring.f A' (CommRing→Ring B') g' v gnull

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


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

module Cubical.Foundations.Logic where

import Cubical.Data.Empty as D
import Cubical.Data.Prod  as D
import Cubical.Data.Sum   as D
import Cubical.Data.Unit  as D

open import Cubical.Foundations.Prelude

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Foundations.HLevels  using (hProp; ΣProp≡; isPropIsProp; propPi) public
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Relation.Nullary hiding (¬_)

infix 10 ¬_
infixr 8 _⊔_
infixr 8 _⊔′_
infixr 8 _⊓_
infixr 8 _⊓′_
infixr 6 _⇒_
infixr 4 _⇔_
infix 30 _≡ₚ_
infix 30 _≢ₚ_

infix 2 ∃[]-syntax
infix 2 ∃[∶]-syntax

infix 2 ∀[∶]-syntax
infix 2 ∀[]-syntax

infix 2 ⇒∶_⇐∶_
infix 2 ⇐∶_⇒∶_

--------------------------------------------------------------------------------
-- The type hProp of mere propositions
-- the definition hProp is given in Foundations.HLevels
-- hProp {ℓ} = Σ (Type ℓ) isProp

private
  variable
    ℓ ℓ' ℓ'' : Level
    P Q R : hProp {ℓ}
    A B C : Type ℓ

[_] : hProp → Type ℓ
[_] = fst

∥_∥ₚ : Type ℓ → hProp
∥ A ∥ₚ = ∥ A ∥ , propTruncIsProp

_≡ₚ_ : (x y : A) → hProp
x ≡ₚ y = ∥ x ≡ y ∥ₚ

hProp≡ : [ P ] ≡ [ Q ] → P ≡ Q
hProp≡ p = ΣProp≡ (\ _ → isPropIsProp) p

--------------------------------------------------------------------------------
-- Logical implication of mere propositions

_⇒_ : (A : hProp {ℓ}) → (B : hProp {ℓ'}) → hProp
A ⇒ B = ([ A ] → [ B ]) , propPi λ _ → B .snd

⇔toPath : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇔toPath {P = P} {Q = Q} P⇒Q Q⇒P = hProp≡ (isoToPath
  (iso P⇒Q Q⇒P (λ b → Q .snd (P⇒Q (Q⇒P b)) b) λ a → P .snd (Q⇒P (P⇒Q a)) a))

pathTo⇒ : P ≡ Q → [ P ⇒ Q ]
pathTo⇒ p x = subst fst  p x

pathTo⇐ : P ≡ Q → [ Q ⇒ P ]
pathTo⇐ p x = subst fst (sym p) x

substₚ : {x y : A} (B : A → hProp {ℓ}) → [ x ≡ₚ y ⇒ B x ⇒ B y ]
substₚ {x = x} {y = y} B = elimPropTrunc (λ _ → propPi λ _ → B y .snd) (subst (fst ∘ B))

--------------------------------------------------------------------------------
-- Mixfix notations for ⇔-toPath
-- see ⊔-identityˡ and ⊔-identityʳ for the difference

⇒∶_⇐∶_ : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇒∶_⇐∶_ = ⇔toPath

⇐∶_⇒∶_ : [ Q ⇒ P ] → [ P ⇒ Q ] → P ≡ Q
⇐∶ g ⇒∶ f  = ⇔toPath f g
--------------------------------------------------------------------------------
-- False and True

⊥ : hProp
⊥ = D.⊥ , λ ()

⊤ : hProp
⊤ = D.Unit , (λ _ _ _ → D.tt)

--------------------------------------------------------------------------------
-- Pseudo-complement of mere propositions

¬_ : hProp {ℓ} → hProp
¬ A = ([ A ] → D.⊥) , propPi λ _ → D.isProp⊥

_≢ₚ_ : (x y : A) → hProp
x ≢ₚ y = ¬ x ≡ₚ y

--------------------------------------------------------------------------------
-- Disjunction of mere propositions

_⊔′_ : Type ℓ → Type ℓ' → Type _
A ⊔′ B = ∥ A D.⊎ B ∥

_⊔_ : hProp {ℓ} → hProp {ℓ'} → hProp
P ⊔ Q = ∥ [ P ] D.⊎ [ Q ] ∥ₚ

inl : A → A ⊔′ B
inl x = ∣ D.inl x ∣

inr : B → A ⊔′ B
inr x = ∣ D.inr x ∣

⊔-elim : (P : hProp {ℓ}) (Q : hProp {ℓ'}) (R : [ P ⊔ Q ] → hProp {ℓ''})
  → (∀ x → [ R (inl x) ]) → (∀ y → [ R (inr y) ]) → (∀ z → [ R z ])
⊔-elim _ _ R P⇒R Q⇒R = elimPropTrunc (snd ∘ R) (D.elim-⊎ P⇒R Q⇒R)

--------------------------------------------------------------------------------
-- Conjunction of mere propositions
_⊓′_ : Type ℓ → Type ℓ' → Type _
A ⊓′ B = A D.× B

_⊓_ : hProp {ℓ} → hProp {ℓ'} → hProp
A ⊓ B = [ A ] ⊓′ [ B ] , D.hLevelProd 1 (A .snd) (B .snd)

⊓-intro : (P : hProp {ℓ}) (Q : [ P ] → hProp {ℓ'}) (R : [ P ] → hProp {ℓ''})
       → (∀ a → [ Q a ]) → (∀ a → [ R a ]) → (∀ (a : [ P ]) → [ Q a ⊓ R a ] )
⊓-intro _ _ _ = D.intro-×

--------------------------------------------------------------------------------
-- Logical bi-implication of mere propositions

_⇔_ : hProp {ℓ} → hProp {ℓ'} → hProp
A ⇔ B = (A ⇒ B) ⊓ (B ⇒ A)

--------------------------------------------------------------------------------
-- Universal Quantifier

∀[∶]-syntax : (A → hProp {ℓ}) → hProp
∀[∶]-syntax {A = A} P = (∀ x → [ P x ]) , propPi (snd ∘ P)

∀[]-syntax : (A → hProp {ℓ}) → hProp
∀[]-syntax {A = A} P = (∀ x → [ P x ]) , propPi (snd ∘ P)

syntax ∀[∶]-syntax {A = A} (λ a → P) = ∀[ a ∶ A ] P
syntax ∀[]-syntax (λ a → P)          = ∀[ a ] P
--------------------------------------------------------------------------------
-- Existential Quantifier

∃[]-syntax : (A → hProp {ℓ}) → hProp
∃[]-syntax {A = A} P = ∥ Σ A (fst ∘ P) ∥ₚ

∃[∶]-syntax : (A → hProp {ℓ}) → hProp
∃[∶]-syntax {A = A} P = ∥ Σ A (fst ∘ P) ∥ₚ

syntax ∃[]-syntax {A = A} (λ x → P) = ∃[ x ∶ A ] P
syntax ∃[∶]-syntax (λ x → P) = ∃[ x ] P
--------------------------------------------------------------------------------
-- Decidable mere proposition

Decₚ : (P : hProp {ℓ}) → hProp {ℓ}
Decₚ P = Dec [ P ] , isPropDec (snd P)

--------------------------------------------------------------------------------
-- Negation commutes with truncation

∥¬A∥≡¬∥A∥ : (A : Type ℓ) → ∥ (A → D.⊥) ∥ₚ ≡ (¬ ∥ A ∥ₚ)
∥¬A∥≡¬∥A∥ _ =
  ⇒∶ (λ ¬A A → elimPropTrunc (λ _ → D.isProp⊥)
    (elimPropTrunc (λ _ → propPi λ _ → D.isProp⊥) (λ ¬p p → ¬p p) ¬A) A)
  ⇐∶ λ ¬p → ∣ (λ p → ¬p ∣ p ∣) ∣

--------------------------------------------------------------------------------
-- (hProp, ⊔, ⊥) is a bounded ⊔-semilattice

⊔-assoc : (P : hProp {ℓ}) (Q : hProp {ℓ'}) (R : hProp {ℓ''})
  → P ⊔ (Q ⊔ R) ≡ (P ⊔ Q) ⊔ R
⊔-assoc P Q R =
  ⇒∶ ⊔-elim P (Q ⊔ R) (λ _ → (P ⊔ Q) ⊔ R)
    (inl ∘ inl)
    (⊔-elim Q R (λ _ → (P ⊔ Q) ⊔ R) (inl ∘ inr) inr)

  ⇐∶ assoc2
  where
    assoc2 : (A ⊔′ B) ⊔′ C → A ⊔′ (B ⊔′ C)
    assoc2 ∣ D.inr a ∣ = ∣ D.inr ∣ D.inr a ∣ ∣
    assoc2 ∣ D.inl ∣ D.inr b ∣ ∣ = ∣ D.inr ∣ D.inl b ∣ ∣
    assoc2 ∣ D.inl ∣ D.inl c ∣ ∣ = ∣ D.inl c ∣
    assoc2 ∣ D.inl (squash x y i) ∣ = propTruncIsProp (assoc2 ∣ D.inl x ∣) (assoc2 ∣ D.inl y ∣) i
    assoc2 (squash x y i)           = propTruncIsProp (assoc2 x) (assoc2 y) i

⊔-idem : (P : hProp {ℓ}) → P ⊔ P ≡ P
⊔-idem P =
  ⇒∶ (⊔-elim P P (\ _ → P) (\ x → x) (\ x → x))
  ⇐∶ inl

⊔-comm : (P : hProp {ℓ}) (Q : hProp {ℓ'}) → P ⊔ Q ≡ Q ⊔ P
⊔-comm P Q =
  ⇒∶ (⊔-elim P Q (\ _ → (Q ⊔ P)) inr inl)
  ⇐∶ (⊔-elim Q P (\ _ → (P ⊔ Q)) inr inl)

⊔-identityˡ : (P : hProp {ℓ}) → ⊥ ⊔ P ≡ P
⊔-identityˡ P =
  ⇒∶ (⊔-elim ⊥ P (λ _ → P) (λ ()) (λ x → x))
  ⇐∶ inr

⊔-identityʳ : (P : hProp {ℓ}) → P ⊔ ⊥ ≡ P
⊔-identityʳ P = ⇔toPath (⊔-elim P ⊥ (λ _ → P) (λ x → x) λ ()) inl

--------------------------------------------------------------------------------
-- (hProp, ⊓, ⊤) is a bounded ⊓-lattice

⊓-assoc : (P : hProp {ℓ}) (Q : hProp {ℓ'}) (R : hProp {ℓ''})
  → P ⊓ Q ⊓ R ≡ (P ⊓ Q) ⊓ R
⊓-assoc _ _ _ =
  ⇒∶ (λ {(x D., (y D., z)) →  (x D., y) D., z})
  ⇐∶ (λ {((x D., y) D., z) → x D., (y D., z) })

⊓-comm : (P : hProp {ℓ}) (Q : hProp {ℓ'}) → P ⊓ Q ≡ Q ⊓ P
⊓-comm _ _ = ⇔toPath D.swap D.swap

⊓-idem : (P : hProp {ℓ}) → P ⊓ P ≡ P
⊓-idem _ = ⇔toPath D.proj₁ (λ x → x D., x)

⊓-identityˡ : (P : hProp {ℓ}) → ⊤ ⊓ P ≡ P
⊓-identityˡ _ = ⇔toPath D.proj₂ λ x → D.tt D., x

⊓-identityʳ : (P : hProp {ℓ}) → P ⊓ ⊤ ≡ P
⊓-identityʳ _ = ⇔toPath D.proj₁ λ x → x D., D.tt

--------------------------------------------------------------------------------
-- Distributive laws

⇒-⊓-distrib : (P : hProp {ℓ}) (Q : hProp {ℓ'})(R : hProp {ℓ''})
  → P ⇒ (Q ⊓ R) ≡ (P ⇒ Q) ⊓ (P ⇒ R)
⇒-⊓-distrib _ _ _ =
  ⇒∶ (λ f → (D.proj₁ ∘ f) D., (D.proj₂ ∘ f))
  ⇐∶ (λ { (f D., g) x → f x D., g x})

⊓-⊔-distribˡ : (P : hProp {ℓ}) (Q : hProp {ℓ'})(R : hProp {ℓ''})
  → P ⊓ (Q ⊔ R) ≡ (P ⊓ Q) ⊔ (P ⊓ R)
⊓-⊔-distribˡ P Q R =
  ⇒∶ (λ { (x D., a) → ⊔-elim Q R (λ _ → (P ⊓ Q) ⊔ (P ⊓ R))
        (λ y → ∣ D.inl (x D., y) ∣ )
        (λ z → ∣ D.inr (x D., z) ∣ ) a })

  ⇐∶ ⊔-elim (P ⊓ Q) (P ⊓ R) (λ _ → P ⊓ Q ⊔ R)
       (λ y → D.proj₁ y D., inl (D.proj₂ y))
       (λ z → D.proj₁ z D., inr (D.proj₂ z))

⊔-⊓-distribˡ : (P : hProp {ℓ}) (Q : hProp {ℓ'})(R : hProp {ℓ''})
  → P ⊔ (Q ⊓ R) ≡ (P ⊔ Q) ⊓ (P ⊔ R)
⊔-⊓-distribˡ P Q R =
  ⇒∶ ⊔-elim P (Q ⊓ R) (λ _ → (P ⊔ Q) ⊓ (P ⊔ R) )
    (D.intro-× inl inl) (D.map-× inr inr)

  ⇐∶ (λ { (x D., y) → ⊔-elim P R (λ _ → P ⊔ Q ⊓ R) inl
      (λ z → ⊔-elim P Q (λ _ → P ⊔ Q ⊓ R) inl (λ y → inr (y D., z)) x) y })

⊓-∀-distrib :  (P : A → hProp {ℓ}) (Q : A → hProp {ℓ'})
  → (∀[ a ∶ A ] P a) ⊓ (∀[ a ∶ A ] Q a) ≡ (∀[ a ∶ A ] (P a ⊓ Q a))
⊓-∀-distrib P Q =
  ⇒∶ (λ {(p D., q) a → p a D., q a})
  ⇐∶ λ pq → (D.proj₁ ∘ pq ) D., (D.proj₂ ∘ pq)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------

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

module Equality.Propositional where

open import Equality
open import Logical-equivalence hiding (_∘_)
open import Prelude

------------------------------------------------------------------------
-- Equality

open import Agda.Builtin.Equality public using (_≡_; refl)

private

  refl′ : ∀ {a} {A : Type a} (x : A) → x ≡ x
  refl′ x = refl

  elim : ∀ {a p} {A : Type a} {x y}
         (P : {x y : A} → x ≡ y → Type p) →
         (∀ x → P (refl′ x)) →
         (x≡y : x ≡ y) → P x≡y
  elim P r refl = r _

  elim-refl : ∀ {a p} {A : Type a} {x}
              (P : {x y : A} → x ≡ y → Type p)
              (r : ∀ x → P (refl′ x)) →
              elim P r (refl′ x) ≡ r x
  elim-refl P r = refl

------------------------------------------------------------------------
-- Various derived definitions and properties

reflexive-relation : ∀ ℓ → Reflexive-relation ℓ
Reflexive-relation._≡_  (reflexive-relation _) = _≡_
Reflexive-relation.refl (reflexive-relation _) = refl′

equality-with-J₀ : ∀ {a p} → Equality-with-J₀ a p reflexive-relation
Equality-with-J₀.elim      equality-with-J₀ = elim
Equality-with-J₀.elim-refl equality-with-J₀ = elim-refl

equivalence-relation⁺ : ∀ ℓ → Equivalence-relation⁺ ℓ
equivalence-relation⁺ _ = J₀⇒Equivalence-relation⁺ equality-with-J₀

-- The following definition has been expanded in order to ensure that
-- it does not reduce (unless a projection is applied to it).

equality-with-J : ∀ {a p} → Equality-with-J a p equivalence-relation⁺
equality-with-J .Equality-with-J.equality-with-J₀ = J₀⇒J equality-with-J₀ .Equality-with-J.equality-with-J₀
equality-with-J .Equality-with-J.cong             = J₀⇒J equality-with-J₀ .Equality-with-J.cong
equality-with-J .Equality-with-J.cong-refl        = J₀⇒J equality-with-J₀ .Equality-with-J.cong-refl
equality-with-J .Equality-with-J.subst            = J₀⇒J equality-with-J₀ .Equality-with-J.subst
equality-with-J .Equality-with-J.subst-refl       = J₀⇒J equality-with-J₀ .Equality-with-J.subst-refl
equality-with-J .Equality-with-J.dcong            = J₀⇒J equality-with-J₀ .Equality-with-J.dcong
equality-with-J .Equality-with-J.dcong-refl       = J₀⇒J equality-with-J₀ .Equality-with-J.dcong-refl

open Derived-definitions-and-properties equality-with-J public
  hiding (_≡_; refl; reflexive-relation; equality-with-J₀)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2011-04-11
-- taken from test/succeed/HereditarilySingletonRecord.agda

module FrozenMVar where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

one : ℕ
one = _

force : one ≡ suc zero
force = refl
-- this tries to instantiate the frozen metavar for one

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT

module groups.KernelCstImage {i j k}
  {G : Group i} {H : Group j} (K : Group k)
  (φ : G →ᴳ H) (H-ab : is-abelian H) where

  open import groups.KernelImage {K = K} cst-hom φ H-ab
  open import groups.Cokernel φ H-ab

  Ker-cst-quot-Im : Ker/Im ≃ᴳ Coker
  Ker-cst-quot-Im = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
    to : Ker/Im.El → Coker.El
    to = SetQuot-rec SetQuot-level to' quot-rel where
      to' : Ker.El (cst-hom {G = H} {H = K}) → Coker.El
      to' ker = q[ fst ker ]

    from : Coker.El → Ker/Im.El
    from = SetQuot-rec SetQuot-level from' quot-rel where
      from' : Group.El H → Ker/Im.El
      from' h = q[ h , idp ]

    abstract
      to-from : ∀ cok → to (from cok) == cok
      to-from = SetQuot-elim (λ _ → =-preserves-set SetQuot-level)
        (λ _ → idp)
        (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

      from-to : ∀ ker → from (to ker) == ker
      from-to = SetQuot-elim (λ _ → =-preserves-set SetQuot-level)
        (λ _ → ap q[_] $ ker-El=-out idp)
        (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

      to-pres-comp : preserves-comp Ker/Im.comp Coker.comp to
      to-pres-comp = SetQuot-elim
        (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
        (λ _ → SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ _ → idp)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _)))
        (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-

Pointed structure: X ↦ X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Pointed where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Univalence
open import Cubical.Relation.ZigZag.Base
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Structures.Pointed

private
  variable
    ℓ : Level

-- Structured relations

preservesSetsPointed : preservesSets {ℓ = ℓ} PointedStructure
preservesSetsPointed setX = setX

PointedRelStr : StrRel PointedStructure ℓ
PointedRelStr R = R

open SuitableStrRel
open isQuasiEquivRel

pointedSuitableRel : SuitableStrRel {ℓ = ℓ} PointedStructure PointedRelStr
pointedSuitableRel .quo _ _ _ = isContrSingl _
pointedSuitableRel .symmetric _ r = r
pointedSuitableRel .transitive _ _ r r' = ∣ _ , r , r' ∣
pointedSuitableRel .prop propR = propR

pointedRelMatchesEquiv : StrRelMatchesEquiv {ℓ = ℓ} PointedRelStr PointedEquivStr
pointedRelMatchesEquiv _ _ _ = idEquiv _

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Data.𝟙

module Oscar.Class.Unit where

module Unit {𝔞} (𝔄 : Ø 𝔞) = ℭLASS 𝟙 𝔄

module _ {𝔞} {𝔄 : Ø 𝔞} where ‼ = Unit.method 𝔄


text:
------------------------------------------------------------------------
-- A proof of univalence
------------------------------------------------------------------------

-- The code is based on code by Anders Mörtberg from Agda's reference
-- manual or the cubical library.

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

module Equality.Path.Univalence where

open import Agda.Builtin.Cubical.Glue as Glue hiding (_≃_)

open import Equality.Path
open import Prelude

open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence.Contractible-preimages equality-with-J as CP
import Equivalence.Half-adjoint equality-with-J as HA
open import Function-universe equality-with-J hiding (id)
open import Preimage equality-with-J
open import Univalence-axiom equality-with-J hiding (≃⇒≡)

private
  variable
    a b ℓ : Level
    A     : Type a

private

  -- Conversions between CP._≃_ and Glue._≃_.

  ≃-CP⇒≃-Glue : {B : Type b} → A CP.≃ B → A Glue.≃ B
  ≃-CP⇒≃-Glue = Σ-map id (λ eq → record { equiv-proof = eq })

  ≃-Glue⇒≃-CP : {B : Type b} → A Glue.≃ B → A CP.≃ B
  ≃-Glue⇒≃-CP = Σ-map id Glue.isEquiv.equiv-proof

  -- Equivalences can be converted to equalities (if the two types live
  -- in the same universe).

  ≃-CP⇒≡ : {A B : Type ℓ} → A CP.≃ B → A ≡ B
  ≃-CP⇒≡ {A = A} {B = B} A≃B = λ i → primGlue B
    (λ { (i = 0̲) → A
       ; (i = 1̲) → B
    })
    (λ { (i = 0̲) → ≃-CP⇒≃-Glue A≃B
       ; (i = 1̲) → ≃-CP⇒≃-Glue CP.id
    })

  -- If ≃-CP⇒≡ is applied to the identity equivalence, then the result
  -- is equal to CP.id.

  ≃-CP⇒≡-id : ≃-CP⇒≡ CP.id ≡ refl {x = A}
  ≃-CP⇒≡-id {A = A} = λ i j → primGlue A
    {φ = max i (max j (- j))}
    (λ _ → A)
    (λ _ → ≃-CP⇒≃-Glue CP.id)

  -- ≃-CP⇒≡ is a left inverse of CP.≡⇒≃.

  ≃-CP⇒≡∘≡⇒≃ :
    {A B : Type ℓ} (A≡B : A ≡ B) →
    ≃-CP⇒≡ (CP.≡⇒≃ A≡B) ≡ A≡B
  ≃-CP⇒≡∘≡⇒≃ = elim
    (λ A≡B → ≃-CP⇒≡ (CP.≡⇒≃ A≡B) ≡ A≡B)
    (λ A →
       ≃-CP⇒≡ (CP.≡⇒≃ refl)  ≡⟨ cong ≃-CP⇒≡ CP.≡⇒≃-refl ⟩
       ≃-CP⇒≡ CP.id          ≡⟨ ≃-CP⇒≡-id ⟩∎
       refl                  ∎)

  -- ≃-CP⇒≡ is a right inverse of CP.≡⇒≃.

  ≡⇒≃∘≃-CP⇒≡ :
    {A B : Type ℓ} (A≃B : A CP.≃ B) →
    CP.≡⇒≃ (≃-CP⇒≡ A≃B) ≡ A≃B
  ≡⇒≃∘≃-CP⇒≡ {A = A} {B = B} A≃B =
    Σ-≡,≡→≡
      (proj₁ (CP.≡⇒≃ (≃-CP⇒≡ A≃B))                            ≡⟨⟩
       proj₁ (transport (λ i → A CP.≃ ≃-CP⇒≡ A≃B i) 0̲ CP.id)  ≡⟨⟩
       transport (λ i → A → ≃-CP⇒≡ A≃B i) 0̲ id                ≡⟨⟩
       transport (λ _ → A → B) 0̲ (proj₁ A≃B)                  ≡⟨ cong (_$ proj₁ A≃B) $ transport-refl 0̲ ⟩∎
       proj₁ A≃B                                              ∎)
      (CP.propositional ext _ _ _)

  -- Univalence for CP._≃_.

  univ-CP : CP.Univalence ℓ
  univ-CP =
    Is-equivalence≃Is-equivalence-CP _ $
    _≃_.is-equivalence $
    Eq.↔→≃ _ ≃-CP⇒≡ ≡⇒≃∘≃-CP⇒≡ ≃-CP⇒≡∘≡⇒≃

-- Univalence.

univ : ∀ {ℓ} → Univalence ℓ
univ {A = A} {B = B} = record
  { univalence = from , proofs
  }
  where
  univ′ : Univalence′ A B
  univ′ = _≃_.from (Univalence≃Univalence-CP ext) univ-CP

  from : A ≃ B → A ≡ B
  from = proj₁ (Univalence′.univalence univ′)

  abstract

    proofs : HA.Proofs ≡⇒≃ from
    proofs = proj₂ (Univalence′.univalence univ′)

-- Equivalences can be converted to equalities (if the two types live
-- in the same universe).

≃⇒≡ : {A B : Type ℓ} → A ≃ B → A ≡ B
≃⇒≡ = _≃_.from Eq.⟨ _ , Univalence′.univalence univ ⟩

private

  -- The type primGlue A B f is equivalent to A.

  primGlue≃-CP :
    (φ : I)
    (B : Partial φ (Type ℓ))
    (f : PartialP φ (λ x → B x Glue.≃ A)) →
    primGlue A B f CP.≃ A
  primGlue≃-CP {A = A} φ B f =
      prim^unglue {φ = φ}
    , λ x →
          ( prim^glue
              (λ p → CP.inverse (proj₂ (f-CP p)) x)
              (hcomp (lemma₁ x) x)
          , (hcomp (lemma₁ x) x  ≡⟨ sym $ hfill (lemma₁ x) (inˢ x) ⟩∎
             x                   ∎)
          )
        , λ y i →
              prim^glue (λ { (φ = 1̲) → proj₁ (lemma₂ is-one y i) })
                        (hcomp (lemma₃ y i) x)
            , (hcomp (lemma₃ y i) x  ≡⟨ sym $ hfill (lemma₃ y i) (inˢ x) ⟩∎
               x                     ∎)
    where
    f-CP : PartialP φ (λ x → B x CP.≃ A)
    f-CP p = ≃-Glue⇒≃-CP (f p)

    lemma₁ : A → ∀ i → Partial φ A
    lemma₁ x i (φ = 1̲) = (
      x                                               ≡⟨ sym (CP.right-inverse-of (proj₂ (f-CP is-one)) x) ⟩∎
      proj₁ (f-CP _) (CP.inverse (proj₂ (f-CP _)) x)  ∎) i

    lemma₂ :
      ∀ {x} p (y : proj₁ (f-CP p) ⁻¹ x) →
      ( CP.inverse (proj₂ (f-CP p)) x
      , CP.right-inverse-of (proj₂ (f-CP p)) x
      ) ≡
      y
    lemma₂ {x} p = CP.irrelevance (proj₂ (f-CP p)) x

    lemma₃ : ∀ {x} → prim^unglue {e = f} ⁻¹ x →
             ∀ i → I → Partial (max φ (max i (- i))) A
    lemma₃     y i j (φ = 1̲) = sym (proj₂ (lemma₂ is-one y i)) j
    lemma₃ {x} _ i j (i = 0̲) = hfill (lemma₁ x) (inˢ x) j
    lemma₃     y i j (i = 1̲) = sym (proj₂ y) j

-- An alternative formulation of univalence.

other-univ : Other-univalence ℓ
other-univ {ℓ = ℓ} {B = B} =                  $⟨ other-univ-CP ⟩
  Contractible (∃ λ (A : Type ℓ) → A CP.≃ B)  ↝⟨ (H-level-cong _ 0 $
                                                  ∃-cong λ _ → inverse $
                                                  ≃≃≃-CP {k = equivalence} ext) ⦂ (_ → _) ⟩□
  Contractible (∃ λ (A : Type ℓ) → A ≃ B)     □
  where
  other-univ-CP : Contractible (∃ λ (A : Type ℓ) → A CP.≃ B)
  other-univ-CP =
      (B , CP.id)
    , λ (A , A≃B) i →
          let C : ∀ i → Partial (max i (- i)) (Type ℓ)
              C = λ { i (i = 0̲) → B
                    ; i (i = 1̲) → A
                    }

              f : ∀ i → PartialP (max i (- i)) (λ j → C i j Glue.≃ B)
              f = λ { i (i = 0̲) → ≃-CP⇒≃-Glue CP.id
                    ; i (i = 1̲) → ≃-CP⇒≃-Glue A≃B
                    }
          in
            primGlue     _ _ (f i)
          , primGlue≃-CP _ _ (f i)


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℝ using () renaming (ℚ to ℝ)

module andGate-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

andGate : ℝ → (ℝ → ℝ)
andGate = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

Truthy : ℝ → Set
Truthy x = x ℝ.≥ ℤ.+ 1 ℝ./ 2

Falsey : ℝ → Set
Falsey x = x ℝ.≤ ℤ.+ 1 ℝ./ 2

ValidInput : ℝ → Set
ValidInput x = ℤ.+ 0 ℝ./ 1 ℝ.≤ x × x ℝ.≤ ℤ.+ 1 ℝ./ 1

CorrectOutput : ℝ → (ℝ → Set)
CorrectOutput x1 x2 = let y = andGate x1 x2 in (Truthy x1 × Truthy x2 → Truthy y) × ((Truthy x1 × Falsey x2 → Falsey y) × ((Falsey x1 × Truthy x2 → Falsey y) × (Falsey x1 × Falsey x2 → Falsey y)))

abstract
  andGateCorrect : ∀ (x1 : ℝ) → ∀ (x2 : ℝ) → ValidInput x1 × ValidInput x2 → CorrectOutput x1 x2
  andGateCorrect = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


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

module VecHelpers where

open import Data.Nat
import Data.Fin as F

open import Data.Vec
open import Function renaming (_∘_ to _○_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

infixl 10 _∘̬_     -- vector composition

------------------------------------------------------------------
-- VECTOR LEMMAS AND HELPERS

vmap : {n : ℕ} → {A B : Set} → (A → B) → Vec A n → Vec B n
vmap f [] = []
vmap f (x ∷ xs) = (f x) ∷ (vmap f xs)

-- Syntactic sugar for lookup that's a lot nicer
_!!_ : {A : Set} → {n : ℕ} → Vec A n → F.Fin n → A
_!!_ v i = lookup i v

-- XXX: is this in the right order?
_∘̬_ : {m n : ℕ} {A : Set} → Vec (F.Fin n) m → Vec A n → Vec A m
v₁ ∘̬ v₂ = tabulate (λ i → v₂ !! (v₁ !! i))

_∘̬′_ : {m n : ℕ} {A : Set} → Vec (F.Fin n) m → Vec A n → Vec A m
[] ∘̬′ v₂ = []
(i ∷ is) ∘̬′  v₂ = (v₂ !! i) ∷ (is ∘̬′ v₂)

∘̬≡∘̬′ : {m n : ℕ} {A : Set} (v₁ : Vec (F.Fin n) m) (v₂ : Vec A n) →
       (v₁ ∘̬ v₂) ≡ (v₁ ∘̬′ v₂)
∘̬≡∘̬′ [] v₂ = refl
∘̬≡∘̬′ (x ∷ v₁) v₂ = cong (_∷_ (v₂ !! x)) (∘̬≡∘̬′ v₁ v₂)

ntimes : {A : Set} → ℕ → (f : A → A) → A → A
ntimes zero f a = a
ntimes (suc n) f a = f (ntimes n f a)

ntimesD : {A : Set} → {B : A → Set} → {g : A → A} → (n : ℕ) →
          (f : {a : A} → B a → B (g a)) →
          {a : A} →
          B a → B (ntimes n g a)
ntimesD zero f b = b
ntimesD {g = g} (suc n) f {a = a} b =
  f {ntimes n g a} (ntimesD {g = g} n (λ {a} → f {a}) {a = a} b)

ntails : {A : Set} → {n k : ℕ} → Vec A (ntimes k suc n) → Vec A n
ntails {k = zero} v = v
ntails {k = suc n} (x ∷ xs) = ntails {k = n} xs

ntails₀ : {A : Set} → {k : ℕ} → (v : Vec A (ntimes k suc zero)) →
          [] ≡ ntails {k = k} v
ntails₀ {k = zero} [] = refl
ntails₀ {k = suc k} (x ∷ v) = ntails₀ {k = k} v

-- Important lemma about lookup; for some reason it doesn't seem to be in the
-- library even though it's in the main agda tutorial, iirc
map!! : {n : ℕ} → {A B : Set} → (f : A → B) → (v : Vec A n) → (i : F.Fin n) →
        (vmap f v) !! i ≡ f (v !! i)
map!! {zero}  f  [] ()
map!! {suc n} f (x ∷ xs) F.zero    = refl
map!! {suc n} f (x ∷ xs) (F.suc i) = map!! f xs i

lookupTab : {A : Set} {n : ℕ} {f : F.Fin n → A} →  (i : F.Fin n) →
            (tabulate f) !! i ≡ (f i)
lookupTab {f = f} F.zero   = refl
lookupTab        (F.suc i) = lookupTab i

mapTab : {A B : Set} → {n : ℕ} → (f : A → B) → (g : F.Fin n → A) →
         vmap f (tabulate g) ≡ tabulate (f ○ g)
mapTab {n = zero}  f g = refl
mapTab {n = suc n} f g =
  cong (_∷_ (f (g F.zero))) (mapTab {n = n} f (g ○ F.suc))

-- Lemma for proving that two vectors are equal if their tabulates agree
-- on all inputs.
tabf∼g : {n : ℕ} → {A : Set} → (f g : F.Fin n → A) → (∀ x → f x ≡ g x) →
         tabulate f ≡ tabulate g
tabf∼g {zero} f g p = refl
tabf∼g {suc n} f g p with f F.zero | g F.zero | p F.zero
tabf∼g {suc n} f g p | x | .x | refl =
  cong (_∷_ x) (tabf∼g {n} (f ○ F.suc) (g ○ F.suc) (p ○ F.suc))

lookup∼vec : {n : ℕ} → {A : Set} →
             (v₁ v₂ : Vec A n) → (∀ i → v₁ !! i ≡ v₂ !! i) → v₁ ≡ v₂
lookup∼vec []          []           p = refl
lookup∼vec (x ∷ v₁) (x₁ ∷ v₂) p with p F.zero
lookup∼vec (x ∷ v₁) (.x ∷ v₂) p | refl =
  cong (_∷_ x) (lookup∼vec v₁ v₂ (p ○ F.suc))

∘̬id : {A : Set} → {n : ℕ} → (k : ℕ) → (v : Vec A (ntimes k suc n)) →
       (tabulate {n} (ntimesD {ℕ} {F.Fin} {suc} k F.suc)) ∘̬ v ≡
       (tabulate (λ i → v !! (ntimesD {ℕ} {F.Fin} {suc} k F.suc i)))
∘̬id {n = n} k v = begin
       (tabulate {n} (ntimesD {ℕ} {F.Fin} {suc} k F.suc)) ∘̬ v
         ≡⟨ refl ⟩
       (tabulate
         (λ i → v !! (tabulate (ntimesD {ℕ} {F.Fin} {suc} k F.suc) !! i)))
         ≡⟨ tabf∼g
              (λ i → v !! (tabulate (ntimesD {ℕ} {F.Fin} {suc} k F.suc) !! i))
              (λ i → v !! ntimesD {ℕ} {F.Fin} {suc} k F.suc i)
              (λ i → cong (_!!_ v) (lookupTab i)) ⟩
       (tabulate (λ i → v !! (ntimesD {ℕ} {F.Fin} {suc} k F.suc i))) ∎

map2+id : {m n : ℕ} → (v : Vec (F.Fin n) m) → {x y : F.Fin (suc (suc n))} →
          (vmap F.suc (vmap F.suc v)) ∘̬′
            (x ∷ y ∷ tabulate {n} (F.suc ○ F.suc)) ≡
          (vmap F.suc (vmap F.suc v))
map2+id [] = refl
map2+id {suc m} {n} (i ∷ v) {x} {y} =
  begin
  (vmap F.suc (vmap F.suc (i ∷ v))) ∘̬′ (x ∷ y ∷ tabulate (F.suc ○ F.suc))
    ≡⟨ refl ⟩
  (tabulate (F.suc ○ F.suc) !! i) ∷
    (vmap F.suc (vmap F.suc v)) ∘̬′ (x ∷ y ∷ tabulate (F.suc ○ F.suc))
    ≡⟨ cong (λ z → z ∷ ((vmap F.suc (vmap F.suc v))) ∘̬′ (x ∷ y ∷ tabulate (F.suc ○ F.suc)))
            (lookupTab i) ⟩
  F.suc (F.suc i) ∷ (vmap F.suc (vmap F.suc v) ∘̬′ (x ∷ y ∷ tabulate (F.suc ○ F.suc)))
    ≡⟨ cong (_∷_ (F.suc (F.suc i))) (map2+id v) ⟩
  F.suc (F.suc i) ∷ (vmap F.suc (vmap F.suc v))
    ≡⟨ refl ⟩
  (vmap F.suc (vmap F.suc (i ∷ v))) ∎

head!!0 : {n : ℕ} {A : Set} (v : Vec A (suc n)) → v !! F.zero ≡ head v
head!!0 (x ∷ v) = refl

headmap : {n : ℕ} {A B : Set} {f : A → B} (v : Vec A (suc n)) →
          head (vmap f v) ≡ f (head v)
headmap (x ∷ v) = refl

tailmap : {n : ℕ} {A B : Set} {f : A → B} (v : Vec A (suc n)) →
          tail (vmap f v) ≡ vmap f (tail v)
tailmap (x ∷ v) = refl

2suc∘̬2tail : {n : ℕ} {A : Set} (v : Vec A (suc (suc n))) →
             (tabulate (F.suc ○ F.suc)) ∘̬ v ≡ (tail (tail v))
2suc∘̬2tail (x ∷ x₁ ∷ v) =
  begin
  (tabulate (F.suc ○ F.suc)) ∘̬ (x ∷ x₁ ∷ v)
    ≡⟨ refl ⟩
  tabulate (λ i → (x ∷ x₁ ∷ v) !! (tabulate (F.suc ○ F.suc) !! i))
    ≡⟨ lookup∼vec
         (tabulate (λ i → (x ∷ x₁ ∷ v) !! (tabulate (F.suc ○ F.suc) !! i)))
         v
         (λ i →
           begin
           tabulate (λ j → (x ∷ x₁ ∷ v) !! (tabulate (F.suc ○ F.suc) !! j)) !! i
             ≡⟨ lookupTab i ⟩
           (x ∷ x₁ ∷ v) !! (tabulate (F.suc ○ F.suc) !! i)
             ≡⟨ cong (λ q → (x ∷ x₁ ∷ v) !! q) (lookupTab i) ⟩
           v !! i ∎) ⟩
  v ∎

-- upTo n returns [0, 1, ..., n-1] as Fins
upTo : (n : ℕ) → Vec (F.Fin n) n
upTo n = tabulate {n} id

upToTail : (n : ℕ) → (tail (tail (upTo (suc (suc n))))) ≡ (vmap F.suc (tail (upTo (suc n))))
upToTail n =
  begin
  tail (tail (upTo (suc (suc n))))
    ≡⟨ refl ⟩
  tabulate (F.suc ○ F.suc)
    ≡⟨ sym (mapTab F.suc F.suc) ⟩
  vmap F.suc (tabulate F.suc) ∎

sidfn : {A : Set} {n : ℕ} (v : Vec A n) (i : F.Fin n) →
        ((upTo n) ∘̬ v) !! i ≡ v !! i
sidfn {n = n} v i =
  begin
  ((upTo n) ∘̬ v) !! i
    ≡⟨ lookupTab {f = λ x → v !! ((upTo n) !! x)} i ⟩
  v !! ((upTo n) !! i)
    ≡⟨ cong (_!!_ v) (lookupTab {f = id} i) ⟩
  v !! i ∎

∘̬simpleid : {A : Set} {n : ℕ} (v : Vec A n) → (upTo n) ∘̬ v ≡ v
∘̬simpleid {n = n} v = lookup∼vec (upTo n ∘̬ v) v (sidfn v)

lookupMap : {A B : Set} → {n : ℕ} → {f : A → B} →
            (i : F.Fin n) → (v : Vec A n) →
            lookup i (vmap f v) ≡ f (lookup i v)
lookupMap F.zero    (x ∷ _)      = refl
lookupMap (F.suc i) (_ ∷ v) = lookupMap i v

lookup∘tabulate : ∀ {a n} → {A : Set a} →
                  (i : F.Fin n) → (f : F.Fin n → A) →
                  lookup i (tabulate f) ≡ f i
lookup∘tabulate F.zero    f = refl
lookup∘tabulate (F.suc i) f = lookup∘tabulate i (f ○ F.suc)

vmap∘vmap : {n : ℕ} {A B C : Set} (f : B → C) (g : A → B) (v : Vec A n) →
    vmap f (vmap g v) ≡ vmap (f ○ g) v
vmap∘vmap {zero} f g [] = refl
vmap∘vmap {suc n} f g (x ∷ v) = cong (λ y → f (g x) ∷ y) (vmap∘vmap f g v)

vmap∘id : {n : ℕ} {A : Set} {v : Vec A n} {f : A → A } → (∀ {x} → f x ≡ x) → vmap f v ≡ v
vmap∘id {zero} {v = []} eq = refl
vmap∘id {suc n} {v = (x ∷ v)} {f} eq = cong₂ _∷_  eq (vmap∘id {v = v} eq)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality
module Spire.Examples.ComputationalDesc where

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

data Desc (I : Set) : Set₁ where
  `⊤ : Desc I
  `X : (i : I) → Desc I
  `Σ `Π : (A : Set) (B : A → Desc I) → Desc I

El : (I : Set) (D : Desc I) (X : I → Set) → Set
El I `⊤ X = ⊤
El I (`X i) X = X i
El I (`Σ A B) X = Σ A (λ a → El I (B a) X)
El I (`Π A B) X = (a : A) → El I (B a) X

data μ (I : Set) (R : I → Desc I) (i : I) : Set where
  con : El I (R i) (μ I R) → μ I R i

All : (I : Set) (X : I → Set) (D : Desc I) (xs : El I D X) (P : (i : I) → X i → Set) → Set
All I X `⊤ tt P = ⊤
All I X (`X i) x P = P i x
All I X (`Σ A B) (a , b) P = All I X (B a) b P
All I X (`Π A B) f P = (a : A) → All I X (B a) (f a) P

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

ind :
  (I : Set)
  (R : I → Desc I)
  (P : (i : I) → μ I R i → Set)
  (pcon : (i : I) (xs : El I (R i) (μ I R)) → All I (μ I R) (R i) xs P → P i (con xs))
  (i : I)
  (x : μ I R i)
  → P i x

hyps :
  (I : Set)
  (R : I → Desc I)
  (P : (i : I) → μ I R i → Set)
  (pcon : (i : I) (xs : El I (R i) (μ I R)) → All I (μ I R) (R i) xs P → P i (con xs))
  (D : Desc I)
  (xs : El I D (μ I R))
  → All I (μ I R) D xs P

ind I R P pcon i (con xs) = pcon i xs (hyps I R P pcon (R i) xs)

hyps I R P pcon `⊤ tt = tt
hyps I R P pcon (`X i) xs = ind I R P pcon i xs
hyps I R P pcon (`Σ A B) (a , b) = hyps I R P pcon (B a) b
hyps I R P pcon (`Π A B) f = λ a → hyps I R P pcon (B a) (f a)

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

data ℕT : Set where `zero `suc : ℕT
data VecT : Set where `nil `cons : VecT

ℕD : ⊤ → Desc ⊤
ℕD tt = `Σ ℕT λ
  { `zero → `⊤
  ; `suc → `X tt
  }

ℕ : ⊤ → Set
ℕ = μ ⊤ ℕD

-- zero : ℕ tt
pattern zero = con (`zero , tt)

-- suc : ℕ tt → ℕ tt
pattern suc n = con (`suc , n)

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

VecD : (A : Set) (n : ℕ tt) → Desc (ℕ tt)
VecD A zero = `⊤
VecD A (suc n) = `Σ A λ _ → `X n

Vec : (A : Set) (n : ℕ tt) → Set
Vec A n = μ (ℕ tt) (VecD A) n

nil : (A : Set) → Vec A zero
nil A = con tt

cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
cons A n x xs = con (x , xs)

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

add : ℕ tt → ℕ tt → ℕ tt
add = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
  (λ
    { tt (`zero , tt) tt n → n
    ; tt (`suc , m) ih n → suc (ih n)
    }
  )
  tt

mult : ℕ tt → ℕ tt → ℕ tt
mult = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
  (λ
    { tt (`zero , tt) tt n → zero
    ; tt (`suc , m) ih n → add n (ih n)
    }
  )
  tt

append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
append A = ind (ℕ tt) (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
  (λ
    { zero tt tt n ys → ys
    ; (suc m) (x , xs) ih n ys → cons A (add m n) x (ih n ys)
    }
  )

concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
concat A m = ind (ℕ tt) (VecD (Vec A m)) (λ n xss → Vec A (mult n m))
  (λ
    { zero tt tt → nil A
    ; (suc n) (xs , xss) ih → append A m xs (mult n m) ih
    }
  )

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module BBHeap.Height.Log {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_ ) where

open import BBHeap _≤_ hiding (#)
open import BBHeap.Height _≤_
open import BBHeap.Properties _≤_
open import Bound.Lower A
open import Data.Sum renaming (_⊎_ to _∨_)
open import SNat
open import SNat.Log
open import SNat.Order
open import SNat.Order.Properties
open import SNat.Properties
open import SNat.Sum
open import Relation.Binary.PropositionalEquality

lemma-height-≃ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ≃ r → height l ≡ height r
lemma-height-≃ ≃lf = refl
lemma-height-≃ (≃nd _ _ _ _ _ _ l≃l') rewrite lemma-height-≃ l≃l' = refl

lemma-height'-≃ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ≃ r → height' l ≡ height' r
lemma-height'-≃ ≃lf = refl
lemma-height'-≃ (≃nd _ _ _ _ l≃r l'≃r' l≃l') rewrite lemma-height'-≃ (trans≃ (trans≃ (sym≃ l≃r) l≃l') l'≃r') = refl

lemma-height-height'-⋗ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋗ r → height l ≡ succ (height' r)
lemma-height-height'-⋗ (⋗lf _) = refl
lemma-height-height'-⋗ (⋗nd _ _ _ _ _ l'≃r' l⋗l') rewrite lemma-height-height'-⋗ l⋗l' | lemma-height'-≃ l'≃r' = refl

lemma-height-height'-⋘ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋘ r → height l ≡ height' r ∨ height l ≡ succ (height' r)
lemma-height-height'-⋘ lf⋘ = inj₁ refl
lemma-height-height'-⋘ (ll⋘ _ _ l⋘r _ l'≃r' r≃l')
    with lemma-height-height'-⋘ l⋘r
... | inj₁ hl≡h'r rewrite hl≡h'r | lemma-height'-≃ (trans≃ r≃l' l'≃r') = inj₁ refl
... | inj₂ hl≡h'r+1 rewrite hl≡h'r+1 | lemma-height'-≃ (trans≃ r≃l' l'≃r') = inj₂ refl
lemma-height-height'-⋘ (lr⋘ _ _ _  _ l'≃r' l⋗l') rewrite lemma-height-height'-⋗ (lemma⋗≃ l⋗l' l'≃r')= inj₂ refl

lemma-height-height'-⋙ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋙ r → height l ≡ height' r ∨ height l ≡ succ (height' r)
lemma-height-height'-⋙ (⋙lf _) = inj₂ refl
lemma-height-height'-⋙ (⋙rl _ _ _ _ _ l⋗r')  rewrite lemma-height-height'-⋗ l⋗r' = inj₂ refl
lemma-height-height'-⋙ (⋙rr _ _ _ _ l'⋙r' l≃l')
    with lemma-height-height'-⋙ l'⋙r'
... | inj₁ hl'≡h'r' rewrite lemma-height-≃ l≃l' | hl'≡h'r' = inj₁ refl
... | inj₂ hl'≡h'r'+1  rewrite lemma-height-≃ l≃l' | hl'≡h'r'+1 = inj₂ refl

lemma-height-height' : {b : Bound}(h : BBHeap b) → height h ≡ height' h ∨ height h ≡ succ (height' h)
lemma-height-height' leaf = inj₁ refl
lemma-height-height' (left _ l⋘r)
    with lemma-height-height'-⋘ l⋘r
... | inj₁ hl≡h'r rewrite hl≡h'r = inj₁ refl
... | inj₂ hl≡h'r+1 rewrite hl≡h'r+1 = inj₂ refl
lemma-height-height' (right _ l⋙r)
    with lemma-height-height'-⋙ l⋙r
... | inj₁ hl≡h'r rewrite hl≡h'r = inj₁ refl
... | inj₂ hl≡h'r+1 rewrite hl≡h'r+1 = inj₂ refl

lemma-#-≃ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ≃ r → # l ≡ # r
lemma-#-≃ ≃lf = refl
lemma-#-≃ (≃nd _ _ _ _ l≃r l'≃r' l≃l')
                   rewrite lemma-#-≃ (sym≃ l≃r)
                            | lemma-#-≃ l≃l'
                            | lemma-#-≃ l'≃r' = refl

lemma-#-⋗ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋗ r → # l ≡ succ (# r + # r)
lemma-#-⋗ (⋗lf _) = refl
lemma-#-⋗ (⋗nd _ _ _ _ l≃r l'≃r' l⋗l')
                   rewrite  lemma-#-≃ (sym≃ l≃r)
                            | lemma-#-⋗ l⋗l'
                            | lemma-#-≃ l'≃r' = refl

lemma-⋘-# : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋘ r → # r ≤′ # l
lemma-⋘-# lf⋘ = refl≤′
lemma-⋘-# (ll⋘ {r' = r'} _ _ l⋘r _ l'≃r' r≃l')
                   rewrite lemma-#-≃ r≃l'
                             | lemma-#-≃ l'≃r' = lemma-s≤′s (+-right-monotony-≤′ (# r') (lemma-≡-≤′ (lemma-#-≃ (sym≃ (trans≃ r≃l' l'≃r'))) (lemma-⋘-# l⋘r)))
lemma-⋘-# (lr⋘ {r = r} {r' = r'} _ _ _ _ l'≃r' l⋗l')
                   rewrite lemma-#-⋗ l⋗l'
                             | lemma-#-≃ l'≃r' = lemma-s≤′s (≤′-step (lemma-m≤′m+n (# r' + # r') (# r)))

lemma-#-⋙ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋙ r → # l ≤′ succ (# r + # r)
lemma-#-⋙ (⋙lf _) = refl≤′
lemma-#-⋙ (⋙rl {l' = l'}{r' = r'} _ _ _ l≃r l'⋘r' l⋗r')
                   rewrite lemma-#-≃ (sym≃ l≃r)
                             | lemma-#-⋗ l⋗r'
                             | +-assoc-succ (# r' + # r') (# r' + # r')
                             | +-assoc-succ (# l' + # r') (# l' + # r') = lemma-s≤′s (lemma-s≤′s (lemma-s≤′s (lemma-4m≤′n+m+n+m (lemma-⋘-# l'⋘r'))))
lemma-#-⋙ (⋙rr {l' = l'} {r' = r'} _ _ _ l≃r _ l≃l')
                   rewrite lemma-#-≃ (sym≃ l≃r)
                             | lemma-#-≃ l≃l'
                             | +-assoc-succ (# l' + # r') (# l' + # r') = lemma-s≤′s (≤′-step (≤′-step (lemma-2m≤′m+n+m+n (# l') (# r'))))

mutual
  lemma-⋙-# : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋙ r → # r ≤′ # l
  lemma-⋙-# (⋙lf _) = ≤′-step refl≤′
  lemma-⋙-# (⋙rl {r' = r'} _ _ _ l≃r l'⋘r' l⋗r')
                   rewrite lemma-#-≃ (sym≃ l≃r)
                             | lemma-#-⋗ l⋗r' = lemma-s≤′s (trans≤′ (+-right-monotony-≤′ (# r') (lemma-#-⋘ l'⋘r')) (lemma-s≤′s (+-left-monotony-≤′ (# r' + # r') (≤′-step (lemma-n≤′2n (# r'))))))
  lemma-⋙-# (⋙rr {l' = l'} {r' = r'} _ _ _ l≃r l'⋙r' l≃l')
                   rewrite lemma-#-≃ (sym≃ l≃r)
                             | lemma-#-≃ l≃l'
                             | +-comm (# l') (# r') = lemma-s≤′s (+-right-monotony-≤′ (# l') (lemma-⋙-# l'⋙r'))

  lemma-#-⋘ : {b b' : Bound}{l : BBHeap b}{r : BBHeap b'} → l ⋘ r → # l ≤′ succ (# r + # r)
  lemma-#-⋘ lf⋘ = ≤′-step refl≤′
  lemma-#-⋘ (ll⋘ {r = r} _ _ l⋘r _ l'≃r' r≃l')
                   rewrite lemma-#-≃ (sym≃ l'≃r')
                             | lemma-#-≃ (sym≃ r≃l')
                             | +-assoc-succ (# r + # r) (# r + # r)
                             | +-assoc-left (# r + # r) (# r) (# r) = lemma-s≤′s (≤′-step (trans≤′ (+-right-monotony-≤′ (# r) (lemma-#-⋘ l⋘r)) (lemma-s≤′s (lemma-m≤′m+n ((# r + # r) + # r) (# r)))))
  lemma-#-⋘ (lr⋘ {r' = r'} _ _ l⋙r _ l'≃r' l⋗l')
                   rewrite lemma-#-⋗ l⋗l'
                             | lemma-#-≃ l'≃r' = lemma-s≤′s (lemma-s≤′s (+-left-monotony-≤′ (# r' + # r') (trans≤′ (lemma-⋙-# l⋙r) (lemma-≡-≤′ (lemma-#-⋗ (lemma⋗≃ l⋗l' l'≃r')) refl≤′))))

lemma-#-#' : {b : Bound}(h : BBHeap b) → #' h ≤′ # h
lemma-#-#' leaf = refl≤′
lemma-#-#' (left {r = r} _ l⋘r) = lemma-s≤′s (trans≤′ (lemma-2m≤′2n (lemma-#-#' r)) (+-right-monotony-≤′ (# r) (lemma-⋘-# l⋘r)))
lemma-#-#' (right {r = r} _ l⋙r) = lemma-s≤′s (trans≤′ (lemma-2m≤′2n (lemma-#-#' r)) (+-right-monotony-≤′ (# r) (lemma-⋙-# l⋙r)))

lemma-height'-#' : {b : Bound}(h : BBHeap b) → height' h ≤′ log₂ (#' h + #' h)
lemma-height'-#' leaf = refl≤′
lemma-height'-#' (left {r = r} _ _) = trans≤′ (lemma-s≤′s (trans≤′ (lemma-height'-#' r) (lemma-≤′-log (≤′-step (refl≤′ {#' r + #' r}))))) (lemma-1+logn≤′log2n (#' r + #' r))
lemma-height'-#' (right {r = r} _ _) = trans≤′ (lemma-s≤′s (trans≤′ (lemma-height'-#' r) (lemma-≤′-log (≤′-step (refl≤′ {#' r + #' r}))))) (lemma-1+logn≤′log2n (#' r + #' r))

lemma-height'-# : {b : Bound}(h : BBHeap b) → height' h ≤′ succ (log₂ (# h))
lemma-height'-# h = trans≤′ (trans≤′ (lemma-height'-#' h) (lemma-log2n≤′1+logn (#' h))) (lemma-s≤′s (lemma-≤′-log (lemma-#-#' h)))

theorem-height-# : {b : Bound}(h : BBHeap b) → height h ≤′ succ (succ (log₂ (# h)))
theorem-height-# h
    with lemma-height-height' h
... | inj₁ hh≡h'h rewrite hh≡h'h = ≤′-step (lemma-height'-# h)
... | inj₂  hh≡h'h+1 rewrite hh≡h'h+1 = lemma-s≤′s (lemma-height'-# h)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Paths
open import lib.types.Unit
open import lib.types.Empty

module lib.Equivalence2 where

{- Pre- and post- composition with equivalences are equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         {h : A → B} (e : is-equiv h) where

  pre∘-is-equiv : is-equiv (λ (k : B → C) → k ∘ h)
  pre∘-is-equiv = is-eq f g f-g g-f
    where f = _∘ h
          g = _∘ is-equiv.g e
          f-g = λ k → ap (k ∘_) (λ= $ is-equiv.g-f e)
          g-f = λ k → ap (k ∘_) (λ= $ is-equiv.f-g e)

  post∘-is-equiv : is-equiv (λ (k : C → A) → h ∘ k)
  post∘-is-equiv = is-eq f g f-g g-f
    where f = h ∘_
          g = is-equiv.g e ∘_
          f-g = λ k → ap (_∘ k) (λ= $ is-equiv.f-g e)
          g-f = λ k → ap (_∘ k) (λ= $ is-equiv.g-f e)

{- The same thing on the abstraction level of equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         (e : A ≃ B) where

  pre∘-equiv : (B → C) ≃ (A → C)
  pre∘-equiv = (_ , pre∘-is-equiv (snd e))

  post∘-equiv : (C → A) ≃ (C → B)
  post∘-equiv = (_ , post∘-is-equiv (snd e))

is-contr-map : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  → Type (lmax i j)
is-contr-map {A = A} {B = B} f = (y : B) → is-contr (hfiber f y)

equiv-is-contr-map : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  → (is-equiv f → is-contr-map f)
equiv-is-contr-map e y =
   equiv-preserves-level (Σ-emap-l (_== y) (_ , e) ⁻¹) (pathto-is-contr y)

contr-map-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  → (is-contr-map f → is-equiv f)
contr-map-is-equiv {f = f} cm = is-eq _
  (λ b → fst (fst (cm b)))
  (λ b → snd (fst (cm b)))
  (λ a → ap fst (snd (cm (f a)) (a , idp)))

fiber=-econv : ∀ {i j} {A : Type i} {B : Type j} {h : A → B} {y : B}
  (r s : Σ A (λ x → h x == y))
  → (r == s) ≃ Σ (fst r == fst s) (λ γ → ap h γ ∙ snd s == snd r)
fiber=-econv r s = Σ-emap-r (λ γ → !-equiv ∘e (↓-app=cst-econv ⁻¹)) ∘e ((=Σ-econv r s)⁻¹)

module _ {i j} {A : Type i} {B : Type j} where

  linv : (A → B) → Type (lmax i j)
  linv f = Σ (B → A) (λ g → (∀ x → g (f x) == x))

  rinv : (A → B) → Type (lmax i j)
  rinv f = Σ (B → A) (λ g → (∀ y → f (g y) == y))

  lcoh : (f : A → B) → linv f → Type (lmax i j)
  lcoh f (g , g-f) = Σ (∀ y → f (g y) == y)
                       (λ f-g → ∀ y → ap g (f-g y) == g-f (g y))

  rcoh : (f : A → B) → rinv f → Type (lmax i j)
  rcoh f (g , f-g) = Σ (∀ x → g (f x) == x)
                       (λ g-f → ∀ x → ap f (g-f x) == f-g (f x))

module _ {i j} {A : Type i} {B : Type j} {f : A → B} (e : is-equiv f) where

  equiv-linv-is-contr : is-contr (linv f)
  equiv-linv-is-contr = equiv-preserves-level (Σ-emap-r λ _ → λ=-equiv ⁻¹)
                          (equiv-is-contr-map (pre∘-is-equiv e) (idf A))

  equiv-rinv-is-contr : is-contr (rinv f)
  equiv-rinv-is-contr = equiv-preserves-level (Σ-emap-r λ _ → λ=-equiv ⁻¹)
                          (equiv-is-contr-map (post∘-is-equiv e) (idf B))

module _ {i j} {A : Type i} {B : Type j} {f : A → B} where

  rcoh-econv : (v : rinv f)
    → rcoh f v ≃ Π A (λ x → (fst v (f x) , snd v (f x)) == (x , idp {a = f x}))
  rcoh-econv v = Π-emap-r (λ x → ((fiber=-econv {h = f} _ _)⁻¹) ∘e apply-unit-r x) ∘e choice ⁻¹
    where
      apply-unit-r : ∀ x → Σ _ (λ γ → ap f γ == _) ≃ Σ _ (λ γ → ap f γ ∙ idp == _)
      apply-unit-r x = Σ-emap-r λ γ
        → coe-equiv (ap (λ q → q == snd v (f x)) (! (∙-unit-r _)))

  lcoh-econv : (v : linv f)
    → lcoh f v ≃ Π B (λ y → (f (fst v y) , snd v (fst v y)) == (y , idp))
  lcoh-econv v = Π-emap-r (λ y → ((fiber=-econv {h = fst v} _ _)⁻¹) ∘e apply-unit-r y) ∘e choice ⁻¹
    where
      apply-unit-r : ∀ y → Σ _ (λ γ → ap (fst v) γ == _) ≃ Σ _ (λ γ → ap (fst v) γ ∙ idp == _)
      apply-unit-r y = Σ-emap-r λ γ
        → coe-equiv (ap (λ q → q == snd v (fst v y)) (! (∙-unit-r _)))

equiv-rcoh-is-contr : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
                      (e : is-equiv f) → (v : rinv f) → is-contr (rcoh f v)
equiv-rcoh-is-contr {f = f} e v = equiv-preserves-level ((rcoh-econv v)⁻¹)
  (Π-level (λ x → =-preserves-level (equiv-is-contr-map e (f x))))

rinv-and-rcoh-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {h : A → B}
  → Σ (rinv h) (rcoh h) ≃ is-equiv h
rinv-and-rcoh-is-equiv {h = h} = equiv f g (λ _ → idp) (λ _ → idp)
  where f : Σ (rinv h) (rcoh h) → is-equiv h
        f s = record {g = fst (fst s); f-g = snd (fst s);
                      g-f = fst (snd s); adj = snd (snd s)}
        g : is-equiv h → Σ (rinv h) (rcoh h)
        g t = ((is-equiv.g t , is-equiv.f-g t) , (is-equiv.g-f t , is-equiv.adj t))

is-equiv-is-prop : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  → is-prop (is-equiv f)
is-equiv-is-prop = inhab-to-contr-is-prop λ e →
  equiv-preserves-level rinv-and-rcoh-is-equiv
    (Σ-level (equiv-rinv-is-contr e) (equiv-rcoh-is-contr e))

is-equiv-prop : ∀ {i j} {A : Type i} {B : Type j}
  → SubtypeProp (A → B) (lmax i j)
is-equiv-prop = is-equiv , λ f → is-equiv-is-prop

∘e-unit-r : ∀ {i} {A B : Type i} (e : A ≃ B) → (e ∘e ide A) == e
∘e-unit-r e = pair= idp (prop-has-all-paths is-equiv-is-prop _ _)

ua-∘e : ∀ {i} {A B : Type i}
  (e₁ : A ≃ B) {C : Type i} (e₂ : B ≃ C) → ua (e₂ ∘e e₁) == ua e₁ ∙ ua e₂
ua-∘e =
  equiv-induction
    (λ {A} {B} e₁ → ∀ {C} → ∀ (e₂ : B ≃ C) → ua (e₂ ∘e e₁) == ua e₁ ∙ ua e₂)
    (λ A → λ e₂ → ap ua (∘e-unit-r e₂) ∙ ap (λ w → (w ∙ ua e₂)) (! (ua-η idp)))

{- Not sure about the interface.

{- Adjointion where hom = path -}

module _ {i j} {A : Type i} {B : Type j} (e : A ≃ B) where

  =-adjunct : ∀ {a b} → (–> e a == b) → (a == <– e b)
  =-adjunct p = ! (<–-inv-l e _) ∙ ap (<– e) p

  =-adjunct' : ∀ {a b} → (a == <– e b) → (–> e a == b)
  =-adjunct' p = ap (–> e) p ∙ (<–-inv-r e _)
-}

{- Type former equivalences involving Empty may require λ=. -}
module _ {j} {B : Empty → Type j} where
  Σ₁-Empty : Σ Empty B ≃ Empty
  Σ₁-Empty = equiv (⊥-rec ∘ fst) ⊥-rec ⊥-elim (⊥-rec ∘ fst)

  Π₁-Empty : Π Empty B ≃ Unit
  Π₁-Empty = equiv (cst tt) (cst ⊥-elim) (λ _ → contr-has-all-paths Unit-is-contr _ _) (λ _ → λ= ⊥-elim)

Σ₂-Empty : ∀ {i} {A : Type i} → Σ A (λ _ → Empty) ≃ Empty
Σ₂-Empty = equiv (⊥-rec ∘ snd) ⊥-rec ⊥-elim (⊥-rec ∘ snd)

{- Fiberwise equivalence -}
module _ {i j k} {A : Type i} {P : A → Type j} {Q : A → Type k}
  (f : ∀ x → P x → Q x) where

  private
    f-tot : Σ A P → Σ A Q
    f-tot (x , y) = x , f x y

  fiber-equiv-is-total-equiv : (∀ x → is-equiv (f x)) → is-equiv f-tot
  fiber-equiv-is-total-equiv f-ise = is-eq _ from to-from from-to
    where
      from : Σ A Q → Σ A P
      from (x , y) = x , is-equiv.g (f-ise x) y

      abstract
        to-from : ∀ q → f-tot (from q) == q
        to-from (x , q) = pair= idp (is-equiv.f-g (f-ise x) q)

        from-to : ∀ p → from (f-tot p) == p
        from-to (x , p) = pair= idp (is-equiv.g-f (f-ise x) p)

  total-equiv-is-fiber-equiv : is-equiv f-tot → (∀ x → is-equiv (f x))
  total-equiv-is-fiber-equiv f-tot-ise x = is-eq _ from to-from from-to
    where
      module f-tot = is-equiv f-tot-ise

      from : Q x → P x
      from q = transport P (fst= (f-tot.f-g (x , q))) (snd (f-tot.g (x , q)))

      abstract
        from-lemma : ∀ q → snd (f-tot.g (x , q)) == from q
          [ P ↓ fst= (f-tot.f-g (x , q)) ]
        from-lemma q = from-transp P (fst= (f-tot.f-g (x , q))) idp

        to-from : ∀ q → f x (from q) == q
        to-from q =
          transport (λ path → f x (from q) == q [ Q ↓ path ])
            (!-inv-l (fst= (f-tot.f-g (x , q))))
            (!ᵈ (ap↓ (λ {x} → f x) (from-lemma q)) ∙ᵈ snd= (f-tot.f-g (x , q)))

        from-to : ∀ p → from (f x p) == p
        from-to p =
          transport (λ path → from (f x p) == p [ P ↓ path ])
            ( ap (λ path → ! path ∙ fst= (f-tot.g-f (x , p)))
                (ap fst= (! (f-tot.adj (x , p))) ∙ ∘-ap fst f-tot (f-tot.g-f (x , p)))
            ∙ !-inv-l (fst= (f-tot.g-f (x , p))))
            (!ᵈ (from-lemma (f x p)) ∙ᵈ snd= (f-tot.g-f (x , p)))


text:
-- This file defines instances for natural numbers and integers to
-- overload various operations.

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

module Instances where

-- imports from stdlib.
import Data.Nat as Nat
import Data.Integer as Int
import Data.Integer.DivMod as IDM
import Data.Nat.DivMod as NDM

-- imports from local.
open import Typeclasses public

-- Natural numbers form a semiring.
instance
  SMℕ : SemiRing Nat.ℕ
  SMℕ ._+_ = Nat._+_
  SMℕ ._*_ = Nat._*_
  SMℕ .0# = 0
  SMℕ .1# = 1

-- Integers form a semiring.
instance
  SMℤ : SemiRing Int.ℤ
  SMℤ ._+_ = Int._+_
  SMℤ ._*_ = Int._*_
  SMℤ .0# = Int.0ℤ
  SMℤ .1# = Int.1ℤ

-- The set of intergers is a ring.
instance
  Ringℤ : Ring Int.ℤ
  Ringℤ .sra = SMℤ
  Ringℤ .-_ = Int.-_

-- The usual order on ℕ is decidable.
instance
  DOℕ : DecOrd Nat.ℕ
  DOℕ ._≤_   = Nat._≤_
  DOℕ ._≤?_  = Nat._≤?_
  DOℕ ._<_   = Nat._<_
  DOℕ ._<?_  = Nat._<?_

-- The usual order on ℤ is decidable.
instance
  DOℤ : DecOrd Int.ℤ
  DOℤ ._≤_   = Int._≤_
  DOℤ ._≤?_  = Int._≤?_
  DOℤ ._<_   = Int._<_
  DOℤ ._<?_  = Int._<?_

-- ℕ has NonZero stucture on it defined in Data.Nat.Base.
instance
  NZTℕ : NonZeroTypeclass Nat.ℕ
  NZTℕ .NonZero = Nat.NonZero

-- ℤ has NonZero stucture on it defined in Data.Integer.Base.
  NZTℤ : NonZeroTypeclass Int.ℤ
  NZTℤ .NonZero = Int.NonZero

-- div and mod function on ℕ. They are defined in Data.Nat.DivMod.
instance
  DMℕ : DivMod Nat.ℕ
  DMℕ .NZT = NZTℕ
  DMℕ ._/_ = NDM._/_
  DMℕ ._%_ = NDM._%_

-- div and mod function on ℤ. They are defined in Data.Integer.DivMod.
instance
  DMℤ : DivMod Int.ℤ
  DMℤ .NZT = NZTℤ
  DMℤ ._/_ = IDM._div_
  DMℤ ._%_ n d = Int.+ (n IDM.mod d)

-- Identity function can be used as the rank function.
instance
  Rankℕ : Rank Nat.ℕ
  Rankℕ .rank x = x

-- Absolute value function can be used as the rank function.
instance
  Rankℤ : Rank Int.ℤ
  Rankℤ .rank = Int.∣_∣

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Unit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Data.Unit renaming (Unit to UnitType)
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.GroupPath

open GroupStr
open IsGroupHom

private
  variable
    ℓ : Level

Unit : Group₀
Unit = UnitType , groupstr tt (λ _ _ → tt) (λ _ → tt)
                      (makeIsGroup isSetUnit (λ _ _ _ → refl) (λ _ → refl) (λ _ → refl)
                                   (λ _ → refl) (λ _ → refl))

open Iso

-- The trivial group is a unit.
lUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd Unit G) G
fun (fst lUnitGroupIso) = snd
inv (fst lUnitGroupIso) g = tt , g
rightInv (fst lUnitGroupIso) _ = refl
leftInv (fst lUnitGroupIso) _ = refl
snd lUnitGroupIso = makeIsGroupHom λ _ _ → refl

rUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd G Unit) G
fun (fst rUnitGroupIso) = fst
inv (fst rUnitGroupIso) g = g , tt
rightInv (fst rUnitGroupIso) _ = refl
leftInv (fst rUnitGroupIso) _ = refl
snd rUnitGroupIso = makeIsGroupHom λ _ _ → refl

lUnitGroupEquiv : {G : Group ℓ} → GroupEquiv (DirProd Unit G) G
lUnitGroupEquiv = GroupIso→GroupEquiv lUnitGroupIso

rUnitGroupEquiv : ∀ {ℓ} {G : Group ℓ} → GroupEquiv (DirProd G Unit) G
rUnitGroupEquiv = GroupIso→GroupEquiv rUnitGroupIso

contrGroupIsoUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupIso G Unit
fun (fst (contrGroupIsoUnit contr)) _ = tt
inv (fst (contrGroupIsoUnit contr)) _ = fst contr
rightInv (fst (contrGroupIsoUnit contr)) _ = refl
leftInv (fst (contrGroupIsoUnit contr)) x = snd contr x
snd (contrGroupIsoUnit contr) = makeIsGroupHom λ _ _ → refl

contrGroupEquivUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupEquiv G Unit
contrGroupEquivUnit contr = GroupIso→GroupEquiv (contrGroupIsoUnit contr)

isContr→≡UnitGroup : {G : Group ℓ-zero} → isContr (fst G) → Unit ≡ G
isContr→≡UnitGroup c =
  fst (GroupPath _ _)
    (invGroupEquiv ((isContr→≃Unit c)
                  , (makeIsGroupHom (λ _ _ → refl))))

GroupIsoUnitGroup→isContr : {G : Group ℓ-zero}
                           → GroupIso Unit G → isContr (fst G)
GroupIsoUnitGroup→isContr is =
  isOfHLevelRetractFromIso 0 (invIso (fst is)) isContrUnit

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


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

open import Categories.Category

module Categories.Diagram.Equalizer.Properties {o ℓ e} (C : Category o ℓ e) where

open import Categories.Diagram.Equalizer C
open import Categories.Morphism C
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  open C

  variable
    X Y Z : Obj

module _ {f g : X ⇒ Y} (equalizer : Equalizer f g) where
  open Equalizer equalizer
  open HomReasoning

  equalizer-≈⇒≈ : ∀ {h} → arr ∘ h ≈ id → f ≈ g
  equalizer-≈⇒≈ {h} eq = begin
    f             ≈⟨ introʳ eq ⟩
    f ∘ arr ∘ h   ≈⟨ pullˡ equality ⟩
    (g ∘ arr) ∘ h ≈⟨ cancelʳ eq ⟩
    g             ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module _ where

open import Common.Size

data Either (A B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

caseEither : ∀{A B C : Set} → Either A B → (A → C) → (B → C) → C
caseEither (left  a) l r = l a
caseEither (right b) l r = r b

data Nat {i : Size} : Set where
  zero : Nat
  suc  : {i' : Size< i} → Nat {i'} → Nat

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

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

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

add : Nat → Nat → Nat
add (zero ) n = n
add (suc m) n = suc (add m n)

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

-- symmetric difference
-- @diff n m@ returns @left (n - m)@ if @n@ is bigger, otherwise @right (m - n)@
diff : ∀{i j} → Nat {i} → Nat {j} → Either (Nat {i}) (Nat {j})
diff zero    m       = right m
diff (suc n) zero    = left (suc n)
diff (suc n) (suc m) = diff n m

module Case where
  gcd : ∀{i j} → Nat {i} → Nat {j} → Nat
  gcd zero    m       = m
  gcd (suc n) zero    = suc n
  gcd (suc n) (suc m) = caseEither (diff n m)
    (λ n' → gcd n' (suc m))
    (λ m' → gcd (suc n) m')

module With where
  gcd : ∀{i j} → Nat {i} → Nat {j} → Nat
  gcd zero    m       = m
  gcd (suc n) zero    = suc n
  gcd (suc n) (suc m) with diff n m
  ... | left  n' = gcd n' (suc m)
  ... | right m' = gcd (suc n) m'

NatInfty = Nat {∞}

{-# BUILTIN NATURAL  NatInfty  #-}
-- {-# BUILTIN NATPLUS     add       #-} -- not accepted

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for exponentiation over polynomials
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Function

open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
open import Data.Product  using (_,_; _×_; proj₁; proj₂)
open import Data.List.Kleene
open import Data.Vec      using (Vec)

import Data.Nat.Properties as ℕ-Prop
import Relation.Binary.PropositionalEquality as ≡

open Homomorphism homo
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication homo
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

import Algebra.Operations.Ring rawRing as RawPow
import Algebra.Operations.Ring (RawCoeff.rawRing from) as CoPow

pow-eval-hom : ∀ x i → ⟦ x CoPow.^ i +1 ⟧ᵣ ≈ ⟦ x ⟧ᵣ RawPow.^ i +1
pow-eval-hom x ℕ.zero = refl
pow-eval-hom x (suc i) = (*-homo _ x) ⟨ trans ⟩ (≪* pow-eval-hom x i)

⊡-mult-hom : ∀ {n} i (xs : Poly n) ρ → ⟦ ⊡-mult i xs ⟧ ρ ≈ ⟦ xs ⟧ ρ RawPow.^ i +1
⊡-mult-hom ℕ.zero xs ρ = refl
⊡-mult-hom (suc i) xs ρ =  ⊠-hom (⊡-mult i xs) xs ρ ⟨ trans ⟩ (≪* ⊡-mult-hom i xs ρ)

⊡-+1-hom : ∀ {n} → (xs : Poly n) → (i : ℕ) → ∀ ρ → ⟦ xs ⊡ i +1 ⟧ ρ ≈ ⟦ xs ⟧ ρ RawPow.^ i +1
⊡-+1-hom (Κ x  ⊐ i≤n) i ρ = pow-eval-hom x i
⊡-+1-hom xs@(⅀ (_ & ∹ _) ⊐ i≤n) i ρ = ⊡-mult-hom i xs ρ
⊡-+1-hom (⅀ (x ≠0 Δ j & []) ⊐ i≤n) i ρ =
  begin
    ⟦ x ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] ⊐↓ i≤n ⟧ ρ
  ≈⟨ ⊐↓-hom (x ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ []) i≤n ρ ⟩
    ⅀?⟦ x ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] ⟧ (drop-1 i≤n ρ)
  ≈⟨ ∷↓-hom (x ⊡ i +1) (j ℕ.+ i ℕ.* j) [] ρ′ Ρ ⟩
    (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * (⟦ x ⊡ i +1 ⟧ Ρ)
  ≈⟨ *≫ (( ⊡-+1-hom x i Ρ) ) ⟩
    (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * (⟦ x ⟧ Ρ RawPow.^ i +1)
  ≈⟨ rearrange j ⟩
    (( ⟦ x ⟧ Ρ) *⟨ ρ′ ⟩^ j) RawPow.^ i +1
  ∎
  where
  ρ′,Ρ = drop-1 i≤n ρ
  ρ′ = proj₁ ρ′,Ρ
  Ρ = proj₂ ρ′,Ρ
  rearrange : ∀ j → (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * (⟦ x ⟧ Ρ RawPow.^ i +1)≈ (( ⟦ x ⟧ Ρ) *⟨ ρ′ ⟩^ j) RawPow.^ i +1
  rearrange zero =
    begin
      (ρ′ RawPow.^ (i ℕ.* 0)) * (⟦ x ⟧ Ρ RawPow.^ i +1)
    ≡⟨ ≡.cong (λ k →  (ρ′ RawPow.^ k) * (⟦ x ⟧ Ρ RawPow.^ i +1)) (ℕ-Prop.*-zeroʳ i) ⟩
      1# * (⟦ x ⟧ Ρ RawPow.^ i +1)
    ≈⟨ *-identityˡ _ ⟩
      ⟦ x ⟧ Ρ RawPow.^ i +1
    ∎
  rearrange j@(suc j′) =
    begin
      (ρ′ RawPow.^ (j ℕ.+ i ℕ.* j)) * (⟦ x ⟧ Ρ RawPow.^ i +1)
    ≈⟨ ≪* sym ( pow-mult-+1 ρ′ j′ i) ⟩
      ((ρ′ RawPow.^ j′ +1) RawPow.^ i +1) * (⟦ x ⟧ Ρ RawPow.^ i +1)
    ≈⟨ sym (pow-distrib-+1 _ (⟦ x ⟧ Ρ) i) ⟩
      ((ρ′ RawPow.^ j′ +1) * ⟦ x ⟧ Ρ) RawPow.^ i +1
    ∎

⊡-hom : ∀ {n} → (xs : Poly n) → (i : ℕ) → ∀ ρ → ⟦ xs ⊡ i ⟧ ρ ≈ ⟦ xs ⟧ ρ RawPow.^ i
⊡-hom xs ℕ.zero ρ = 1-homo
⊡-hom xs (suc i) ρ = ⊡-+1-hom xs i ρ


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

open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst; setoid)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
import Function.Equality
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.Category.Product
import Categories.NaturalTransformation
import Categories.NaturalTransformation.NaturalIsomorphism

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism
import SecondOrder.Instantiation
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli

module SecondOrder.Mslot
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.MRenaming Σ
  -- open SecondOrder.Substitution Σ
  -- open import SecondOrder.RelativeMonadMorphism
  -- open SecondOrder.Instantiation
  open Categories.Category
  open Categories.Functor using (Functor)
  open Categories.NaturalTransformation renaming (id to idNt)
  open Categories.NaturalTransformation.NaturalIsomorphism renaming (refl to reflNt; sym to symNt; trans to transNt)
  open Categories.Category.Construction.Functors
  open Categories.Category.Instance.Setoids
  open Categories.Category.Product
  open Function.Equality using () renaming (setoid to Π-setoid)
  open SecondOrder.IndexedCategory
  -- open import SecondOrder.RelativeKleisli

  MTele = MContexts
  VTele = VContexts

  -- the codomain category of the MSlots functor. It should be equivalent to the
  -- functor category [ MTele x VTele , < Setoid >ₛₒᵣₜ ]
  -- objects are functors, which are really pairs of functions, one on objects
  -- one on morphisms
  -- morphisms in this category are natural transformations

  module _ where
    open Category
    open NaturalTransformation
    open Function.Equality renaming (_∘_ to _∙_)

    ∘ᵥ-resp-≈ : ∀ {o l e o' l' e'} {𝒞 : Category o l e} {𝒟 : Category o' l' e'}
                {F G H : Functor 𝒞 𝒟} {α β : NaturalTransformation F G} {γ δ : NaturalTransformation G H}
              → (∀ {X : Obj 𝒞} → (𝒟 Category.≈ (η α X)) (η β X))
              → (∀ {X : Obj 𝒞} → (𝒟 Category.≈ (η γ X)) (η δ X))
              -------------------------------------------------------------------
              → (∀ {X : Obj 𝒞} → (𝒟 Category.≈ (η (γ ∘ᵥ α) X)) (η (δ ∘ᵥ β) X))
    ∘ᵥ-resp-≈ {𝒟 = 𝒟} α≈β γ≈δ {X = X} = ∘-resp-≈ 𝒟 γ≈δ α≈β

  MCodom : Category (lsuc ℓ) ℓ ℓ
  MCodom =
    let open Category in
    let open Functor in
    let open NaturalTransformation in
    let open Function.Equality using (_⟨$⟩_) renaming (cong to func-cong) in
    let open Category.HomReasoning in
    record
    { Obj = Functor MTele (Functors VTele (Setoids ℓ ℓ))
    ; _⇒_ = NaturalTransformation
    ; _≈_ = λ {F} {G} α β → ∀ (ψ : Obj MTele) (Γ : Obj VTele)
          → (Setoids ℓ ℓ Category.≈ (η ((η α) ψ) Γ)) (η ((η β) ψ) Γ)
    ; id = idNt
    ; _∘_ = _∘ᵥ_
    ; assoc = λ ψ Γ x≈y → Setoid.refl {!!}
    ; sym-assoc = λ ψ Γ x≈y → Setoid.refl {!!}
    ; identityˡ = λ {F} {G} {α} ψ Γ x≈y → Setoid.refl {!!}
    ; identityʳ = λ ψ Γ x → Setoid.refl {!!}
    ; identity² = Setoid.refl {!!}
    ; equiv = record
              { refl = Setoid.refl {!!}
              ; sym = Setoid.sym {!!}
              ; trans = Setoid.trans {!!}
              }
    ; ∘-resp-≈ = λ {F} {G} {H} {α} {β} {γ} {δ} α≈β γ≈δ ψ Γ
      → ∘ᵥ-resp-≈ {α = γ} {δ} {γ = α} {β} (γ≈δ _ _) (α≈β _ _)
    }

  Mslots : Functor MContexts (IndexedCategory sort (MCodom))
  Mslots =
    let open Categories.NaturalTransformation in
    let open NaturalTransformation in
          record
            { F₀ = λ Θ A →
                 record
                 { F₀ = λ ψ → Term-Functor {Θ ,, ψ} {A}
                 ; F₁ = λ ι → MRenaming-NT (ᵐ⇑ᵐ ι)
                 ; identity = λ t≈s → ≈-trans (≈-trans ([]ᵐ-resp-≡ᵐ ᵐ⇑ᵐ-resp-idᵐ) [idᵐ]) t≈s
                 ; homomorphism = λ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) (≈-trans ([]ᵐ-resp-≡ᵐ ᵐ⇑ᵐ-resp-∘ᵐ) [∘ᵐ])
                 ; F-resp-≈ = λ ι≡μ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) ([]ᵐ-resp-≡ᵐ (ᵐ⇑ᵐ-resp-≡ᵐ ι≡μ))
                 }
            ; F₁ = λ {Θ} {Θ'} ι A →
                 record
                 { η = λ Ψ →
                     record { η = λ Γ → η (MRenaming-NT (⇑ᵐ ι)) Γ
                            ; commute = commute (MRenaming-NT (⇑ᵐ ι))
                            ; sym-commute = sym-commute (MRenaming-NT (⇑ᵐ ι))
                            }
                 ; commute = λ ι t≈s
                           → ≈-trans ([]ᵐ-resp-≈ ([]ᵐ-resp-≈ t≈s)) ⇑-resp-+
                 ; sym-commute = λ ι t≈s → ≈-trans (≈-sym ⇑-resp-+) (([]ᵐ-resp-≈ ([]ᵐ-resp-≈ t≈s)))
                 }
            ; identity = λ Θ ψ Γ t≈s
              → ≈-trans ([]ᵐ-resp-≈ t≈s) (≈-trans ([]ᵐ-resp-≡ᵐ ⇑ᵐ-resp-idᵐ) [idᵐ])
            ; homomorphism = λ A ψ Γ t≈s
              → ≈-trans ([]ᵐ-resp-≈ t≈s) ∘ᵐ-resp-⇑-term
            ; F-resp-≈ = λ ι≡μ A ψ Γ t≈s → ≈-trans ([]ᵐ-resp-≈ t≈s) ([]ᵐ-resp-≡ᵐ (⇑ᵐ-resp-≡ᵐ ι≡μ))
            }

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module StateSized.GUI.ShipBitMap where

open import StateSizedIO.GUI.WxBindingsFFI

ship : Bitmap
ship = bitmap "./StateSized/GUI/ship.ico"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda