text:
{-# OPTIONS --rewriting --prop #-}

open import common hiding (_===_)

{- Syntax of term- and type-expressions, using de Bruijn indices -}

variable
  {n} {m} {k} : ℕ

data Expr : SyntaxSort → ℕ → Set

TyExpr = Expr Ty
TmExpr = Expr Tm

data Expr where
  uu : {n : ℕ} → TyExpr n
  el : {n : ℕ} (v : TmExpr n) → TyExpr n
  pi : {n : ℕ} (A : TyExpr n) (B : TyExpr (suc n)) → TyExpr n

  var : {n : ℕ} (x : VarPos n) → TmExpr n
  lam : {n : ℕ} (A : TyExpr n) (B : TyExpr (suc n)) (u : TmExpr (suc n)) → TmExpr n
  app : {n : ℕ} (A : TyExpr n) (B : TyExpr (suc n)) (f : TmExpr n) (a : TmExpr n) → TmExpr n

data Ctx : ℕ → Set where
  ◇ : Ctx 0
  _,_ : {n : ℕ} (Γ : Ctx n) (A : TyExpr n) → Ctx (suc n)

{- The four different forms of (pre)judgments. -}

data Judgment : Set where
  _⊢_ : {n : ℕ} (Γ : Ctx n) → TyExpr n → Judgment
  _⊢_:>_ : {n : ℕ} (Γ : Ctx n) → TmExpr n → TyExpr n → Judgment
  _⊢_==_ : {n : ℕ} (Γ : Ctx n) → TyExpr n → TyExpr n → Judgment
  _⊢_==_:>_ : {n : ℕ} (Γ : Ctx n) → TmExpr n → TmExpr n → TyExpr n → Judgment

-- weakenV : {n : ℕ} (p : WeakPos n) → VarPos n → VarPos (suc n)
-- weakenV last x = prev x
-- weakenV (prev p) last = last
-- weakenV (prev p) (prev x) = prev (weakenV p x)

weaken : {n : ℕ} {k : SyntaxSort} (p : WeakPos n) → Expr k n → Expr k (suc n)
weaken p uu = uu
weaken p (el v) = el (weaken p v)
weaken p (pi A B) = pi (weaken p A) (weaken (prev p) B)
weaken p (var x) = var (weakenV p x)
weaken p (lam A B u) = lam (weaken p A) (weaken (prev p) B) (weaken (prev p) u)
weaken p (app A B f a) = app (weaken p A) (weaken (prev p) B) (weaken p f) (weaken p a)

-- data Mor (n m : ℕ) : ℕ → Set where
--  ◇ : Mor n m 0
--  _,_ : {k : ℕ} (δ : Mor n m k) (u : TmExpr (n + m)) → Mor n m (suc k)

-- weakenMor : Mor n m k → Mor n (suc m) k
-- weakenMor ◇ = ◇
-- weakenMor (δ , u) = (weakenMor δ , weaken last u)

-- weakenMor+ : Mor n m k → Mor n (suc m) (suc k)
-- weakenMor+ δ = weakenMor δ , var last

data Mor (m : ℕ) : ℕ → Set where
 ◇ : Mor m 0
 _,_ : {k : ℕ} (δ : Mor m k) (u : TmExpr m) → Mor m (suc k)

weakenMor : Mor m k → Mor (suc m) k
weakenMor ◇ = ◇
weakenMor (δ , u) = (weakenMor δ , weaken last u)

weakenMor+ : Mor m k → Mor (suc m) (suc k)
weakenMor+ δ = weakenMor δ , var last

weakV : {n m : ℕ} → VarPos n → VarPos (n + m)
weakV {m = zero} x = x
weakV {m = suc m} x = prev (weakV x)

infix 30 _[_]

-- _[_] : {p : SyntaxSort} (A : Expr p (n + k)) (δ : Mor n m k) → Expr p (n + m)
_[_] : {p : SyntaxSort} (A : Expr p k) (δ : Mor m k) → Expr p m

uu [ δ ] = uu
el v [ δ ] = el (v [ δ ])
pi A B [ δ ] = pi (A [ δ ]) (B [ weakenMor+ δ ])

var last [ δ , u ] = u
var (prev x) [ δ , u ] = var x [ δ ]
lam A B u [ δ ] = lam (A [ δ ]) (B [ weakenMor+ δ ]) (u [ weakenMor+ δ ])
app A B f a [ δ ] = app (A [ δ ]) (B [ weakenMor+ δ ]) (f [ δ ]) (a [ δ ])

idMor : Mor n n
idMor {zero} = ◇
idMor {suc n} = (weakenMor idMor , var last)

subst : {n : ℕ} {k : SyntaxSort} → Expr k (suc n) → TmExpr n → Expr k n
subst e a = e [ idMor , a ]

get : {n : ℕ} → VarPos n → Ctx n → TyExpr n
get last (Γ , A) = weaken last A
get (prev k) (Γ , A) = weaken last (get k Γ)

{- Derivability of judgments, the typing rules of the type theory -}

data Derivable : Judgment → Prop where

  -- Variable rules
  Var : {n : ℕ} {Γ : Ctx n} (k : VarPos n)
    → Derivable (Γ ⊢ get k Γ)
    → Derivable (Γ ⊢ var k :> get k Γ)

  -- Symmetry and transitivity for types
  TyRefl : {n : ℕ} {Γ : Ctx n} {A : TyExpr n}
    → Derivable (Γ ⊢ A) → Derivable (Γ ⊢ A == A)
  TySymm : {n : ℕ} {Γ : Ctx n} {A B : TyExpr n}
    → Derivable (Γ ⊢ A == B) → Derivable (Γ ⊢ B == A)
  TyTran : {n : ℕ} {Γ : Ctx n} {A B C : TyExpr n}
    → Derivable (Γ ⊢ A == B)→ Derivable (Γ ⊢ B == C) → Derivable (Γ ⊢ A == C)

  -- Symmetry and transitivity for terms
  TmRefl : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {u : TmExpr n}
    → Derivable (Γ ⊢ u :> A) → Derivable (Γ ⊢ u == u :> A)
  TmSymm : {n : ℕ} {Γ : Ctx n} {u v : TmExpr n} {A : TyExpr n}
    → Derivable (Γ ⊢ u == v :> A) → Derivable (Γ ⊢ v == u :> A)
  TmTran : {n : ℕ} {Γ : Ctx n} {u v w : TmExpr n} {A : TyExpr n}
    → Derivable (Γ ⊢ u == v :> A)→ Derivable (Γ ⊢ v == w :> A) → Derivable (Γ ⊢ u == w :> A)

  -- Conversion rules
  Conv : {n : ℕ} {Γ : Ctx n} {u : TmExpr n} {A B : TyExpr n}
    → Derivable (Γ ⊢ u :> A) → Derivable (Γ ⊢ A == B) → Derivable (Γ ⊢ u :> B)
  ConvEq : {n : ℕ} {Γ : Ctx n} {u u' : TmExpr n} {A B : TyExpr n}
    → Derivable (Γ ⊢ u == u' :> A) → Derivable (Γ ⊢ A == B) → Derivable (Γ ⊢ u == u' :> B)

  -- Rules for UU
  UU : {n : ℕ} {Γ : Ctx n}
    → Derivable (Γ ⊢ uu)
  UUCong : {n : ℕ} {Γ : Ctx n}
    → Derivable (Γ ⊢ uu == uu)

  -- Rules for El
  El : {n : ℕ} {Γ : Ctx n} {v : TmExpr n}
    → Derivable (Γ ⊢ v :> uu) → Derivable (Γ ⊢ el v)
  ElCong : {n : ℕ} {Γ : Ctx n} {v v' : TmExpr n}
    → {- Derivable (Γ ⊢ v :> uu) → Derivable (Γ ⊢ v' :> uu) → -} Derivable (Γ ⊢ v == v' :> uu) → Derivable (Γ ⊢ el v == el v')

  -- Rules for Pi
  Pi : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {B : TyExpr (suc n)}
    → Derivable (Γ ⊢ A) → Derivable ((Γ , A) ⊢ B) → Derivable (Γ ⊢ pi A B)
  PiCong : {n : ℕ} {Γ : Ctx n} {A A' : TyExpr n} {B B' : TyExpr (suc n)}
    → {- Derivable (Γ ⊢ A) → Derivable (Γ ⊢ A') → -} Derivable (Γ ⊢ A == A') → {- Derivable ((Γ , A) ⊢ B) → Derivable ((Γ , A') ⊢ B') → -} Derivable ((Γ , A) ⊢ B == B') → Derivable (Γ ⊢ pi A B == pi A' B')

  -- Rules for lambda
  Lam : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {B : TyExpr (suc n)} {u : TmExpr (suc n)}
    → Derivable (Γ ⊢ A) → Derivable ((Γ , A) ⊢ B) → Derivable ((Γ , A) ⊢ u :> B)
    → Derivable (Γ ⊢ lam A B u :> pi A B)
  LamCong : {n : ℕ} {Γ : Ctx n} {A A' : TyExpr n} {B B' : TyExpr (suc n)} {u u' : TmExpr (suc n)}
    → {- Derivable (Γ ⊢ A) → Derivable (Γ ⊢ A') → -} Derivable (Γ ⊢ A == A')
    → {- Derivable ((Γ , A) ⊢ B) → Derivable ((Γ , A') ⊢ B') → -} Derivable ((Γ , A) ⊢ B == B')
    → {- Derivable ((Γ , A) ⊢ u :> B) → Derivable ((Γ , A') ⊢ u' :> B') → -} Derivable ((Γ , A) ⊢ u == u' :> B)
    → Derivable (Γ ⊢ lam A B u == lam A' B' u' :> pi A B)

  -- Rules for app
  App : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {B : TyExpr (suc n)} {f a : TmExpr n}
    → Derivable (Γ ⊢ A) → Derivable ((Γ , A) ⊢ B) → Derivable (Γ ⊢ f :> pi A B) → Derivable (Γ ⊢ a :> A)
    → Derivable (Γ ⊢ app A B f a :> subst B a)
  AppCong : {n : ℕ} {Γ : Ctx n} {A A' : TyExpr n} {B B' : TyExpr (suc n)} {f f' a a' : TmExpr n}
    → {- Derivable (Γ ⊢ A) → Derivable (Γ ⊢ A') → -} Derivable (Γ ⊢ A == A')
    → {- Derivable ((Γ , A) ⊢ B) → Derivable ((Γ , A') ⊢ B') → -} Derivable ((Γ , A) ⊢ B == B')
    → {- Derivable (Γ ⊢ f :> pi A B) → Derivable (Γ ⊢ f' :> pi A' B') → -} Derivable (Γ ⊢ f == f' :> pi A B)
    → {- Derivable (Γ ⊢ a :> A) → Derivable (Γ ⊢ a' :> A') → -} Derivable (Γ ⊢ a == a' :> A)
    → Derivable (Γ ⊢ app A B f a == app A' B' f' a' :> subst B a)

  -- Equality rules
  BetaPi : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {B : TyExpr (suc n)} {u : TmExpr (suc n)} {a : TmExpr n}
    → Derivable (Γ ⊢ A) → Derivable ((Γ , A) ⊢ B) → Derivable ((Γ , A) ⊢ u :> B) → Derivable (Γ ⊢ a :> A)
    → Derivable (Γ ⊢ app A B (lam A B u) a == subst u a :> subst B a)
  EtaPi : {n : ℕ} {Γ : Ctx n} {A : TyExpr n} {B : TyExpr (suc n)} {f : TmExpr n}
    → Derivable (Γ ⊢ A) → Derivable ((Γ , A) ⊢ B) → Derivable (Γ ⊢ f :> pi A B)
    → Derivable (Γ ⊢ f == lam A B (app (weaken last A) (weaken (prev last) B) (weaken last f) (var last)) :> pi A B)

data DepCtx (n : ℕ) : ℕ → Set where
  ◇ : DepCtx n 0
  _,_ : {m : ℕ} → DepCtx n m → TyExpr (n + m) → DepCtx n (suc m)

_++_ : {n m : ℕ} → Ctx n → DepCtx n m → Ctx (n + m)
Γ ++ ◇ = Γ
Γ ++ (Δ , A) = (Γ ++ Δ) , A

infixl 30 _++_

_-WeakPos_ : (n : ℕ) → WeakPos n → ℕ
n -WeakPos last = n
suc n -WeakPos prev k = n -WeakPos k

weakenCtx : (k : WeakPos n) (Γ : Ctx n) (T : TyExpr (n -WeakPos k)) → Ctx (suc n)
weakenCtx last Γ T = Γ , T
weakenCtx (prev k) (Γ , A) T = weakenCtx k Γ T , weaken k A

-- data _⊢_===_ (Γ : Ctx n) : DepCtx n m → DepCtx n m → Prop where
--   tt : Γ ⊢ ◇ === ◇
--   _,_ : {Δ Δ' : DepCtx n m} {A A' : TyExpr (n + m)} → (Γ ⊢ Δ === Δ') → Derivable ((Γ ++ Δ) ⊢ A == A') → Γ ⊢ (Δ , A) === (Δ' , A')

-- data _⊢_∷>_⇒_ (Γ : Ctx n) : Mor n m k → DepCtx n m → DepCtx n k → Prop where
--   tt : {Δ : DepCtx n m} → Γ ⊢ ◇ ∷> Δ ⇒ ◇
--   _,_ : {Δ : DepCtx n m} {Δ' : DepCtx n k} {δ : Mor n m k} {u : TmExpr (n + m)} {A : TyExpr (n + k)}
--       → Γ ⊢ δ ∷> Δ ⇒ Δ'
--       → Derivable (Γ ++ Δ ⊢ u :> (A [ δ ]))
--       → Γ ⊢ (δ , u) ∷> Δ ⇒ (Δ' , A)

-- WeakTy : {k : WeakPos n} {Γ : Ctx n} {T : TyExpr (n -WeakPos k)} {A : TyExpr n}
--      → Derivable (Γ ⊢ A) → Derivable (weakenCtx k Γ T ⊢ weaken k A)
-- WeakTy= : {k : WeakPos n} {Γ : Ctx n} {T : TyExpr (n -WeakPos k)} {A B : TyExpr n}
--      → Derivable (Γ ⊢ A == B) → Derivable (weakenCtx k Γ T ⊢ weaken k A == weaken k B)
-- WeakTm : {k : WeakPos n} {Γ : Ctx n} {T : TyExpr (n -WeakPos k)} {u : TmExpr n} {A : TyExpr n}
--      → Derivable (Γ ⊢ u :> A) → Derivable (weakenCtx k Γ T ⊢ weaken k u :> weaken k A)
-- WeakTm= : {k : WeakPos n} {Γ : Ctx n} {T : TyExpr (n -WeakPos k)} {u v : TmExpr n} {A : TyExpr n}
--      → Derivable (Γ ⊢ u == v :> A) → Derivable (weakenCtx k Γ T ⊢ weaken k u == weaken k v :> weaken k A)

-- WeakTy UU = UU
-- WeakTy (El dv) = El (WeakTm dv)
-- WeakTy (Pi dA dB) = Pi (WeakTy dA) (WeakTy dB)

-- WeakTy= (TyRefl dA) = TyRefl (WeakTy dA)
-- WeakTy= (TySymm dA=) = TySymm (WeakTy= dA=)
-- WeakTy= (TyTran dA= dB=) = TyTran (WeakTy= dA=) (WeakTy= dB=)
-- WeakTy= UUCong = UUCong
-- WeakTy= (ElCong dv dv' dv=) = ElCong (WeakTm dv) (WeakTm dv') (WeakTm= dv=)
-- WeakTy= (PiCong dA dA' dA= dB dB' dB=) = PiCong (WeakTy dA) (WeakTy dA') (WeakTy= dA=) (WeakTy dB) (WeakTy dB') (WeakTy= dB=)

-- WeakTm (Var k dA) = Conv (Var (weakenV _ k) {!!}) {!!}
-- WeakTm (Conv du dA=) = Conv (WeakTm du) (WeakTy= dA=)
-- WeakTm (Lam dA dB du) = Lam (WeakTy dA) (WeakTy dB) (WeakTm du)
-- WeakTm (App dA dB df da) = Conv (App (WeakTy dA) (WeakTy dB) (WeakTm df) (WeakTm da)) {!!}

-- WeakTm= (TmRefl du) = TmRefl (WeakTm du)
-- WeakTm= (TmSymm du=) = TmSymm (WeakTm= du=)
-- WeakTm= (TmTran du= dv=) = TmTran (WeakTm= du=) (WeakTm= dv=)
-- WeakTm= (ConvEq du= dA=) = ConvEq (WeakTm= du=) (WeakTy= dA=)
-- WeakTm= (LamCong dA dA' dA= dB dB' dB= du du' du=) = LamCong (WeakTy dA) (WeakTy dA') (WeakTy= dA=) (WeakTy dB) (WeakTy dB') (WeakTy= dB=) (WeakTm du) (WeakTm du') (WeakTm= du=)
-- WeakTm= (AppCong dA dA' dA= dB dB' dB= df df' df= da da' da=) = ConvEq (AppCong (WeakTy dA) (WeakTy dA') (WeakTy= dA=) (WeakTy dB) (WeakTy dB') (WeakTy= dB=) (WeakTm df) (WeakTm df') (WeakTm= df=) (WeakTm da) (WeakTm da') (WeakTm= da=)) {!!}
-- WeakTm= (BetaPi dA dB du da) = ConvEq (TmTran (BetaPi (WeakTy dA) (WeakTy dB) (WeakTm du) (WeakTm da)) {!!}) {!!}

-- WeakMor : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {T : TyExpr (n + m)} {δ : Mor n m k} → Γ ⊢ δ ∷> Δ ⇒ Δ' → Γ ⊢ weakenMor δ ∷> (Δ , T) ⇒ Δ'
-- WeakMor tt = tt
-- WeakMor (dδ , du) = WeakMor dδ , Conv (WeakTm du) {!!}

-- SubstTy : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {A : TyExpr (n + k)} {δ : Mor n m k}
--        → Derivable (Γ ++ Δ' ⊢ A) → Γ ⊢ δ ∷> Δ ⇒ Δ' → Derivable (Γ ++ Δ ⊢ A [ δ ])
-- SubstTy= : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {A A' : TyExpr (n + k)} {δ : Mor n m k}
--        → Derivable (Γ ++ Δ' ⊢ A) → Derivable (Γ ++ Δ' ⊢ A == A') → Γ ⊢ δ ∷> Δ ⇒ Δ' → Derivable (Γ ++ Δ ⊢ A [ δ ] == A' [ δ ])
-- SubstTm : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {u : TmExpr (n + k)} {A : TyExpr (n + k)} {δ : Mor n m k}
--        → Derivable (Γ ++ Δ' ⊢ u :> A) → Γ ⊢ δ ∷> Δ ⇒ Δ' → Derivable (Γ ++ Δ ⊢ u [ δ ] :> A [ δ ])
-- SubstTm= : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {u u' : TmExpr (n + k)} {A : TyExpr (n + k)} {δ : Mor n m k}
--        → Derivable (Γ ++ Δ' ⊢ u == u' :> A) → Γ ⊢ δ ∷> Δ ⇒ Δ' → Derivable (Γ ++ Δ ⊢ u [ δ ] == u' [ δ ] :> A [ δ ])

-- WeakMor+ : {Γ : Ctx n} {Δ : DepCtx n m} {Δ' : DepCtx n k} {A : TyExpr (n + k)} {δ : Mor n m k} → Derivable (Γ ++ Δ' ⊢ A) → Γ ⊢ δ ∷> Δ ⇒ Δ' → Γ ⊢ weakenMor+ δ ∷> (Δ , A [ δ ]) ⇒ (Δ' , A)
-- WeakMor+ dA dδ = WeakMor dδ , Conv (Var last (WeakTy (SubstTy dA dδ))) {!syntx!}

-- TyEqTy1 : {Γ : Ctx n} {A B : TyExpr n} → Derivable (Γ ⊢ A == B) → Derivable (Γ ⊢ A)
-- TyEqTy2 : {Γ : Ctx n} {A B : TyExpr n} → Derivable (Γ ⊢ A == B) → Derivable (Γ ⊢ B)
-- TmEqTm1 : {Γ : Ctx n} {u u' : TmExpr n} {A : TyExpr n} → Derivable (Γ ⊢ u == u' :> A) → Derivable (Γ ⊢ u :> A)
-- TmEqTm2 : {Γ : Ctx n} {u u' : TmExpr n} {A : TyExpr n} → Derivable (Γ ⊢ u == u' :> A) → Derivable (Γ ⊢ u' :> A)

-- SubstTy UU dδ = UU
-- SubstTy (El dv) dδ = El (SubstTm dv dδ)
-- SubstTy (Pi dA dB) dδ = Pi (SubstTy dA dδ) (SubstTy dB (WeakMor+ dA dδ))

-- -- SubstTy= _ (TyRefl dA) dδ = TyRefl (SubstTy dA dδ)
-- -- SubstTy= dA (TySymm dA=) dδ = TySymm (SubstTy= {!!} dA= dδ)
-- -- SubstTy= dA (TyTran dA= dB=) dδ = TyTran (SubstTy= dA dA= dδ) (SubstTy= {!!} dB= dδ)
-- -- SubstTy= dA UUCong dδ = UUCong
-- -- SubstTy= dA (ElCong dv=) dδ = ElCong (SubstTm= dv= dδ)
-- -- SubstTy= {Γ = Γ} (Pi dA dB) (PiCong dA= dB=) dδ = PiCong (SubstTy= dA dA= dδ) (SubstTy= dB dB= (WeakMor+ dA dδ))

-- -- SubstTm (Var k du) dδ = {!!}
-- -- SubstTm (Conv du dA=) dδ = Conv (SubstTm du dδ) (SubstTy= dA= dδ)
-- -- SubstTm (Lam dA dB du) dδ = Lam (SubstTy dA dδ) (SubstTy dB (WeakMor+ dA dδ)) (SubstTm du (WeakMor+ dA dδ))
-- -- SubstTm (App dA dB df da) dδ = Conv (App (SubstTy dA dδ) (SubstTy dB (WeakMor+ dA dδ)) (SubstTm df dδ) (SubstTm da dδ)) {!!}

-- -- SubstTm= (TmRefl du) dδ = TmRefl (SubstTm du dδ)
-- -- SubstTm= (TmSymm du=) dδ = TmSymm (SubstTm= du= dδ)
-- -- SubstTm= (TmTran du= dv=) dδ = TmTran (SubstTm= du= dδ) (SubstTm= dv= dδ)
-- -- SubstTm= (ConvEq du= dA=) dδ = ConvEq (SubstTm= du= dδ) (SubstTy= dA= dδ)
-- -- SubstTm= (LamCong dA= dB= du=) dδ = LamCong (SubstTy= dA= dδ) (SubstTy= dB= (WeakMor+ {!TyEqTy1 dA=!} dδ)) (SubstTm= du= (WeakMor+ {!TyEqTy1 dA=!} dδ))
-- -- SubstTm= (AppCong dA= dB= df= da=) dδ = ConvEq (AppCong (SubstTy= dA= dδ) (SubstTy= dB= (WeakMor+ {!TyEqTy1 dA=!} dδ)) (SubstTm= df= dδ) (SubstTm= da= dδ)) {!stx!}
-- -- SubstTm= (BetaPi dA dB du da) dδ = ConvEq (TmTran (BetaPi (SubstTy dA dδ) (SubstTy dB (WeakMor+ dA dδ)) (SubstTm du (WeakMor+ dA dδ)) (SubstTm da dδ)) {!!}) {!!}

-- -- ConvTy  : {n m : ℕ} {Γ : Ctx n} {Δ Δ' : DepCtx n m} {A : TyExpr (n + m)} → Derivable ((Γ ++ Δ) ⊢ A) → (Γ ⊢ Δ === Δ') → Derivable ((Γ ++ Δ') ⊢ A)
-- -- ConvTy= : {n m : ℕ} {Γ : Ctx n} {Δ Δ' : DepCtx n m} {A A' : TyExpr (n + m)} → Derivable ((Γ ++ Δ) ⊢ A == A') → (Γ ⊢ Δ === Δ') → Derivable ((Γ ++ Δ') ⊢ A == A')
-- -- ConvTm  : {n m : ℕ} {Γ : Ctx n} {Δ Δ' : DepCtx n m} {A : TyExpr (n + m)} {u : TmExpr (n + m)} → Derivable ((Γ ++ Δ) ⊢ u :> A) → (Γ ⊢ Δ === Δ') → Derivable ((Γ ++ Δ') ⊢ u :> A)
-- -- ConvTm= : {n m : ℕ} {Γ : Ctx n} {Δ Δ' : DepCtx n m} {A : TyExpr (n + m)} {u u' : TmExpr (n + m)} → Derivable ((Γ ++ Δ) ⊢ u == u' :> A) → (Γ ⊢ Δ === Δ') → Derivable ((Γ ++ Δ') ⊢ u == u' :> A)

-- -- ConvTy UU dΔ= = UU
-- -- ConvTy (El dv) dΔ= = El (ConvTm dv dΔ=)
-- -- ConvTy (Pi dA dB) dΔ= = Pi (ConvTy dA dΔ=) (ConvTy dB (dΔ= , TyRefl dA))

-- -- ConvTy= (TyRefl dA) dΔ= = TyRefl (ConvTy dA dΔ=)
-- -- ConvTy= (TySymm dA=) dΔ= = TySymm (ConvTy= dA= dΔ=)
-- -- ConvTy= (TyTran dA= dB=) dΔ= = TyTran (ConvTy= dA= dΔ=) (ConvTy= dB= dΔ=)
-- -- ConvTy= UUCong dΔ= = UUCong
-- -- ConvTy= (ElCong dv=) dΔ= = ElCong (ConvTm= dv= dΔ=)
-- -- ConvTy= (PiCong dA= dB=) dΔ= = PiCong (ConvTy= dA= dΔ=) (ConvTy= dB= (dΔ= , {!ok!}))

-- -- ConvTm (Var k du) dΔ= = Conv (Var k (ConvTy {!TODO!} dΔ=)) {!TODO!}
-- -- ConvTm (Conv du dA=) dΔ= = Conv (ConvTm du dΔ=) (ConvTy= dA= dΔ=)
-- -- ConvTm (Lam dA dB du) dΔ= = Lam (ConvTy dA dΔ=) (ConvTy dB (dΔ= , TyRefl dA)) (ConvTm du (dΔ= , TyRefl dA))
-- -- ConvTm (App dA dB df da) dΔ= = App (ConvTy dA dΔ=) (ConvTy dB (dΔ= , TyRefl dA)) (ConvTm df dΔ=) (ConvTm da dΔ=)

-- -- ConvTm= (TmRefl du) dΔ= = TmRefl (ConvTm du dΔ=)
-- -- ConvTm= (TmSymm du=) dΔ= = TmSymm (ConvTm= du= dΔ=)
-- -- ConvTm= (TmTran du= dv=) dΔ= = TmTran (ConvTm= du= dΔ=) (ConvTm= dv= dΔ=)
-- -- ConvTm= (ConvEq du= dA=) dΔ= = ConvEq (ConvTm= du= dΔ=) (ConvTy= dA= dΔ=)
-- -- ConvTm= (LamCong dA= dB= du=) dΔ= = LamCong (ConvTy= dA= dΔ=) (ConvTy= dB= (dΔ= , {!ok!})) (ConvTm= du= (dΔ= , {!ok!}))
-- -- ConvTm= (AppCong dA= dB= df= da=) dΔ= = AppCong (ConvTy= dA= dΔ=) (ConvTy= dB= (dΔ= , {!ok!})) (ConvTm= df= dΔ=) (ConvTm= da= dΔ=)
-- -- ConvTm= (BetaPi dA dB du da) dΔ= = BetaPi (ConvTy dA dΔ=) (ConvTy dB (dΔ= , TyRefl dA)) (ConvTm du (dΔ= , TyRefl dA)) (ConvTm da dΔ=)

-- -- TyEqTy1 (TyRefl dA) = dA
-- -- TyEqTy1 (TySymm dA=) = TyEqTy2 dA=
-- -- TyEqTy1 (TyTran dA= dB=) = TyEqTy1 dA=
-- -- TyEqTy1 UUCong = UU
-- -- TyEqTy1 (ElCong du=) = El (TmEqTm1 du=)
-- -- TyEqTy1 (PiCong dA= dB=) = Pi (TyEqTy1 dA=) (TyEqTy1 dB=)

-- -- TyEqTy2 (TyRefl dA) = dA
-- -- TyEqTy2 (TySymm dA=) = TyEqTy1 dA=
-- -- TyEqTy2 (TyTran dA= dB=) = TyEqTy2 dB=
-- -- TyEqTy2 UUCong = UU
-- -- TyEqTy2 (ElCong du=) = El (TmEqTm2 du=)
-- -- TyEqTy2 (PiCong dA= dB=) = Pi (TyEqTy2 dA=) (ConvTy (TyEqTy2 dB=) (tt , dA=))

-- -- TmEqTm1 (TmRefl du) = du
-- -- TmEqTm1 (TmSymm du=) = TmEqTm2 du=
-- -- TmEqTm1 (TmTran du= dv=) = TmEqTm1 du=
-- -- TmEqTm1 (ConvEq du= dA=) = Conv (TmEqTm1 du=) dA=
-- -- TmEqTm1 (LamCong dA= dB= du=) = Lam (TyEqTy1 dA=) (TyEqTy1 dB=) (TmEqTm1 du=)
-- -- TmEqTm1 (AppCong dA= dB= df= da=) = App (TyEqTy1 dA=) (TyEqTy1 dB=) (TmEqTm1 df=) (TmEqTm1 da=)
-- -- TmEqTm1 (BetaPi dA dB du da) = App dA dB (Lam dA dB du) da

-- -- TmEqTm2 (TmRefl du) = du
-- -- TmEqTm2 (TmSymm du=) = TmEqTm1 du=
-- -- TmEqTm2 (TmTran du= dv=) = TmEqTm2 dv=
-- -- TmEqTm2 (ConvEq du= dA=) = Conv (TmEqTm2 du=) dA=
-- -- TmEqTm2 (LamCong dA= dB= du=) = Conv (Lam (TyEqTy2 dA=) (ConvTy (TyEqTy2 dB=) (tt , dA=)) (ConvTm (Conv (TmEqTm2 du=) dB=) (tt , dA=))) (PiCong (TySymm dA=) (ConvTy= (TySymm dB=) (tt , dA=)))
-- -- TmEqTm2 (AppCong dA= dB= df= da=) = Conv (App (TyEqTy2 dA=) (ConvTy (TyEqTy2 dB=) (tt , dA=)) (Conv (TmEqTm2 df=) (PiCong dA= dB=)) (Conv (TmEqTm2 da=) dA=)) {!TySymm (SubstTy= dB= (tt , {!da=!}))!}
-- -- TmEqTm2 (BetaPi dA dB du da) = {!SubstTm du (tt , {!da!})!}

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


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

module TrustMe where

open import Common.Equality

postulate
  A : Set
  x : A

eq : x ≡ x
eq = primTrustMe

evaluates-to-refl : sym (sym eq) ≡ eq
evaluates-to-refl = refl

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Eta contraction didn't consider hiding when contracting,
-- leading to the following module not type checking.
module Issue259 where

postulate
  A    : Set
  B    : A → Set
  foo  : (∀ x → B x) → A
  q    : ∀ {x} → B x
  foo′ : (∀ {x} → B x) → A

bar : A
bar = foo (λ y → q {y})

Baz : B bar → Set → Set
Baz b C with C
Baz b C | _ = C

-- In fact you're not allowed to eta contract hidden lambdas at all.
bar′ : A
bar′ = foo′ (λ {y} → q {y})

Baz′ : B bar′ → Set → Set
Baz′ b C with C
Baz′ b C | _ = C

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue728 where

open import Common.MAlonzo using () renaming (main to mainDefault)

main = mainDefault


text:
-- Andreas, 2020-09-09, issue #4880
-- Make sure that duplicate hiding info is an error.

module _ (A B : Set) where

postulate
  _ : { { A } } → B

-- Expected: ERROR or WARNING
-- For instance:
-- {A} cannot appear by itself. It needs to be the argument to a
-- function expecting an implicit argument.
-- when scope checking {A}

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Level hiding (suc; zero)
open import Categories.Category
module Categories.Power {o ℓ e : Level} (C : Category o ℓ e) where

open import Function using () renaming (id to idf)
open import Data.Nat using (ℕ; _+_; zero; suc; _≤?_)
open import Data.Product using (_,_)
open import Data.Fin using (Fin; inject+; raise; zero; suc; #_)
open import Data.Sum using (_⊎_; inj₁; inj₂; map) renaming ([_,_] to ⟦_,_⟧; [_,_]′ to ⟦_,_⟧′)
open import Function using (flip) renaming (_∘_ to _∙_)
open import Relation.Nullary.Decidable using (True)
open import Data.Vec.N-ary using (N-ary)

open import Categories.Bifunctor using (Bifunctor)
open import Categories.Functor using (Functor; module Functor)

module C = Category C

Exp : (I : Set) → Category o ℓ e
Exp I = record
  { Obj = I → C.Obj
  ; _⇒_ = λ x y → (i : I) → C [ x i , y i ]
  ; _≡_ = λ f g → (i : I) → C [ f i ≡ g i ]
  ; _∘_ = λ f g i → C [ f i ∘ g i ]
  ; id = λ {x} i → C.id
  ; assoc = λ {A} {B} {C'} {D} {f} {g} {h} i → C.assoc
  ; identityˡ = λ {A} {B} {f} i → C.identityˡ
  ; identityʳ = λ {A} {B} {f} i → C.identityʳ
  ; equiv = record
    { refl = λ {x} i → C.Equiv.refl
    ; sym = λ f i → C.Equiv.sym (f i)
    ; trans = λ f g i → C.Equiv.trans (f i) (g i)
    }
  ; ∘-resp-≡ = λ f≡g h≡i x → C.∘-resp-≡ (f≡g x) (h≡i x)
  }

Power : (n : ℕ) → Category o ℓ e
Power n = Exp (Fin n)

Powerfunctor′ : (D : Category o ℓ e) (I : Set) → Set (e ⊔ ℓ ⊔ o)
Powerfunctor′ D I = Functor (Exp I) D

Powerfunctor : (D : Category o ℓ e) (n : ℕ) → Set (e ⊔ ℓ ⊔ o)
Powerfunctor D n = Powerfunctor′ D (Fin n)

Powerendo′ : (I : Set) → Set (e ⊔ ℓ ⊔ o)
Powerendo′ I = Powerfunctor′ C I

Powerendo : (n : ℕ) → Set (e ⊔ ℓ ⊔ o)
Powerendo n = Powerfunctor C n

Hyperendo : (n m : ℕ) → Set (e ⊔ ℓ ⊔ o)
Hyperendo n m = Functor (Power n) (Power m)

Hyperendo′ : (I J : Set) → Set (e ⊔ ℓ ⊔ o)
Hyperendo′ I J = Functor (Exp I) (Exp J)

_par_ : ∀ {I I′ J J′} (F : Hyperendo′ I I′) (G : Hyperendo′ J J′) → Hyperendo′ (I ⊎ J) (I′ ⊎ J′)
F par G = record
  { F₀ = λ xs → ⟦ F.F₀ (xs ∙ inj₁) , G.F₀ (xs ∙ inj₂) ⟧′
  ; F₁ = λ {A B} fs → ⟦ F.F₁ (fs ∙ inj₁) , G.F₁ (fs ∙ inj₂) ⟧
  ; identity = λ {A} → ⟦ F.identity , G.identity ⟧
  ; homomorphism = λ {A B C fs gs} → ⟦ F.homomorphism , G.homomorphism ⟧
  ; F-resp-≡ = λ {A B fs gs} fs≡gs → ⟦ F.F-resp-≡ (fs≡gs ∙ inj₁) , G.F-resp-≡ (fs≡gs ∙ inj₂) ⟧
  }
  where
  private module F = Functor F
  private module G = Functor G

flattenP : ∀ {D : Category o ℓ e} {n m} (F : Powerfunctor′ D (Fin n ⊎ Fin m)) → Powerfunctor′ D (Fin (n + m))
flattenP {n = n} {m = m} F = record
  { F₀ = λ As → F.F₀ (As ∙ pack)
  ; F₁ = λ {As Bs} fs → F.F₁ (fs ∙ pack)
  ; identity = λ {As} → F.identity
  ; homomorphism = λ {As Bs Cs fs gs} → F.homomorphism
  ; F-resp-≡ = λ {As Bs fs gs} fs≡gs → F.F-resp-≡ (fs≡gs ∙ pack)
  }
  where
  private module F = Functor F
  pack = ⟦ inject+ m , raise n ⟧′

flattenHʳ : ∀ {I} {n m} (F : Hyperendo′ I (Fin n ⊎ Fin m)) → Hyperendo′ I (Fin (n + m))
flattenHʳ {n = n} {m} F = record
  { F₀ = λ As → F.F₀ As ∙ chops n
  ; F₁ = λ {As Bs} fs → F.F₁ fs ∙ chops n
  ; identity = F.identity ∙ chops n
  ; homomorphism = F.homomorphism ∙ chops n
  ; F-resp-≡ = λ fs≡gs → F.F-resp-≡ fs≡gs ∙ chops n
  }
  where
  private module F = Functor F
  chops : (n : ℕ) → ∀ {m} (k : Fin (n + m)) → Fin n ⊎ Fin m
  chops 0 k = inj₂ k
  chops (suc n) zero = inj₁ zero
  chops (suc n) (suc k) = map suc idf (chops n k)

flattenH : ∀ {n m n′ m′} (F : Hyperendo′ (Fin n ⊎ Fin m) (Fin n′ ⊎ Fin m′)) → Hyperendo (n + m) (n′ + m′)
flattenH = flattenHʳ ∙ flattenP

_∥_ : ∀ {n n′ m m′} (F : Hyperendo n n′) (G : Hyperendo m m′) → Hyperendo (n + m) (n′ + m′)
F ∥ G = flattenH (F par G)

reduce′ : ∀ (H : Bifunctor C C C) {I J} (F : Powerendo′ I) (G : Powerendo′ J) → Powerendo′ (I ⊎ J)
reduce′ H {I} {J} F G = record
  { F₀ = my-F₀
  ; F₁ = my-F₁
  ; identity = λ {As} → my-identity {As}
  ; homomorphism = λ {As Bs Cs fs gs} → my-homomorphism {fs = fs} {gs}
  ; F-resp-≡ = λ fs → H.F-resp-≡ (F.F-resp-≡ (fs ∙ inj₁) , G.F-resp-≡ (fs ∙ inj₂))
  }
  where
  private module L = Category (Exp (I ⊎ J))
  private module F = Functor F
  private module G = Functor G
  private module H = Functor H
  open L using () renaming (_≡_ to _≡≡_; _∘_ to _∘∘_)
  open C using (_≡_; _∘_)
  my-F₀ = λ As → H.F₀ ((F.F₀ (As ∙ inj₁)) , (G.F₀ (As ∙ inj₂)))
  my-F₁ : ∀ {As Bs} → L._⇒_ As Bs → C [ my-F₀ As , my-F₀ Bs ]
  my-F₁ {As} {Bs} fs = H.F₁ (F.F₁ (fs ∙ inj₁) , G.F₁ (fs ∙ inj₂))
  .my-identity : ∀ {As} → my-F₁ (L.id {As}) ≡ C.id
  my-identity {As} = begin
                        H.F₁ (F.F₁ (λ i → C.id {As (inj₁ i)}) , G.F₁ (λ i → C.id {As (inj₂ i)}))
                      ↓⟨ H.F-resp-≡ (F.identity , G.identity) ⟩
                        H.F₁ (C.id , C.id)
                      ↓⟨ H.identity ⟩
                        C.id
                      ∎
    where
    open C.HomReasoning
  .my-homomorphism : ∀ {As Bs Cs} {fs : L._⇒_ As Bs} {gs : L._⇒_ Bs Cs} → my-F₁ (gs ∘∘ fs) ≡ (my-F₁ gs ∘ my-F₁ fs)
  my-homomorphism {fs = fs} {gs} =
    begin
      my-F₁ (gs ∘∘ fs)
    ↓⟨ H.F-resp-≡ (F.homomorphism , G.homomorphism) ⟩
      H.F₁ ((F.F₁ (gs ∙ inj₁) ∘ F.F₁ (fs ∙ inj₁)) , (G.F₁ (gs ∙ inj₂) ∘ G.F₁ (fs ∙ inj₂)))
    ↓⟨ H.homomorphism ⟩
      my-F₁ gs ∘ my-F₁ fs
    ∎
    where
    open C.HomReasoning

reduce : ∀ (H : Bifunctor C C C) {n m} (F : Powerendo n) (G : Powerendo m) → Powerendo (n + m)
reduce H F G = flattenP (reduce′ H F G)

flattenP-assocʳ : ∀ {n₁ n₂ n₃} (F : Powerendo′ (Fin n₁ ⊎ (Fin n₂ ⊎ Fin n₃))) → Powerendo ((n₁ + n₂) + n₃)
flattenP-assocʳ {n₁} {n₂} {n₃} F = record
  { F₀ = λ As → F.F₀ (As ∙ pack)
  ; F₁ = λ {As Bs} fs → F.F₁ (fs ∙ pack)
  ; identity = λ {As} → F.identity
  ; homomorphism = λ {As Bs Cs fs gs} → F.homomorphism
  ; F-resp-≡ = λ {As Bs fs gs} fs≡gs → F.F-resp-≡ (fs≡gs ∙ pack)
  }
  where
  module F = Functor F
  pack = ⟦ inject+ n₃ ∙ inject+ n₂ , ⟦ inject+ n₃ ∙ raise n₁ , raise (n₁ + n₂) ⟧′ ⟧′

reduce2ʳ : ∀ (G : Bifunctor C C C) {n₁ n₂ n₃} (F₁ : Powerendo n₁) (F₂ : Powerendo n₂) (F₃ : Powerendo n₃) → Powerendo ((n₁ + n₂) + n₃)
reduce2ʳ G F₁ F₂ F₃ = flattenP-assocʳ (reduce′ G F₁ (reduce′ G F₂ F₃))

overlaps : ∀ {D E} (H : Bifunctor D D E) {I} (F G : Powerfunctor′ D I) → Powerfunctor′ E I
overlaps {D} {E} H {I} F G = record
  { F₀ = my-F₀
  ; F₁ = my-F₁
  ; identity = λ {As} → my-identity {As}
  ; homomorphism = λ {As Bs Cs fs gs} → my-homomorphism {fs = fs} {gs}
  ; F-resp-≡ = λ fs → H.F-resp-≡ (F.F-resp-≡ fs , G.F-resp-≡ fs)
  }
  where
  private module L = Category (Exp I)
  private module F = Functor F
  private module G = Functor G
  private module H = Functor H
  private module D = Category D
  private module E = Category E
  open L using () renaming (_≡_ to _≡≡_; _∘_ to _∘∘_)
  open E using (_≡_; _∘_)
  open D using () renaming (_∘_ to _∘D_)
  my-F₀ = λ As → H.F₀ (F.F₀ As , G.F₀ As)
  my-F₁ : ∀ {As Bs} → (Exp I) [ As , Bs ] → E [ my-F₀ As , my-F₀ Bs ]
  my-F₁ {As} {Bs} fs = H.F₁ (F.F₁ fs , G.F₁ fs)
  .my-identity : ∀ {As} → my-F₁ (L.id {As}) ≡ E.id
  my-identity {As} = begin
                        H.F₁ (F.F₁ (λ i → C.id {As i}) , G.F₁ (λ i → C.id {As i}))
                      ↓⟨ H.F-resp-≡ (F.identity , G.identity) ⟩
                        H.F₁ (D.id , D.id)
                      ↓⟨ H.identity ⟩
                        E.id
                      ∎
    where
    open E.HomReasoning
  .my-homomorphism : ∀ {As Bs Cs} {fs : (Exp I) [ As , Bs ]} {gs : (Exp I) [ Bs , Cs ]} → my-F₁ (gs ∘∘ fs) ≡ (my-F₁ gs ∘ my-F₁ fs)
  my-homomorphism {fs = fs} {gs} =
    begin
      my-F₁ (gs ∘∘ fs)
    ↓⟨ H.F-resp-≡ (F.homomorphism , G.homomorphism) ⟩
      H.F₁ ((F.F₁ gs ∘D F.F₁ fs) , (G.F₁ gs ∘D G.F₁ fs))
    ↓⟨ H.homomorphism ⟩
      my-F₁ gs ∘ my-F₁ fs
    ∎
    where
    open E.HomReasoning

overlap2ʳ : ∀ (G : Bifunctor C C C) {n} (F₁ F₂ F₃ : Powerendo n) → Powerendo n
overlap2ʳ G F₁ F₂ F₃ = (overlaps {C} G F₁ (overlaps {C} G F₂ F₃))

select′ : ∀ {I} (i : I) → Powerendo′ I
select′ {I} i = record
  { F₀ = λ xs → xs i
  ; F₁ = λ fs → fs i
  ; identity = C.Equiv.refl
  ; homomorphism = C.Equiv.refl
  ; F-resp-≡ = λ eqs → eqs i
  }

select : ∀ m {n} {m<n : True (suc m ≤? n)} → Powerendo n
select m {n} {m<n} = select′ (#_ m {n} {m<n})

triv : (n : ℕ) → Hyperendo n n
triv n = record
  { F₀ = λ x → x
  ; F₁ = λ x → x
  ; identity = λ _ → C.Equiv.refl
  ; homomorphism = λ _ → C.Equiv.refl
  ; F-resp-≡ = λ x → x
  }

pad : ∀ (l r : ℕ) {n m} (F : Hyperendo n m) → Hyperendo ((l + n) + r) ((l + m) + r)
pad l r F = (triv l ∥ F) ∥ triv r

padˡ : ∀ (l : ℕ) {n m} (F : Hyperendo n m) → Hyperendo (l + n) (l + m)
padˡ l F = triv l ∥ F

padʳ : ∀ (r : ℕ) {n m} (F : Hyperendo n m) → Hyperendo (n + r) (m + r)
padʳ r F = F ∥ triv r

unary : (F : Functor C C) → Powerendo 1
unary F = record
  { F₀ = λ As → F.F₀ (As zero)
  ; F₁ = λ fs → F.F₁ (fs zero)
  ; identity = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≡ = λ fs≡gs → F.F-resp-≡ (fs≡gs zero)
  }
  where
  module F = Functor F

unaryH : (F : Functor C C) → Hyperendo 1 1
unaryH F = record
  { F₀ = λ As → F.F₀ ∙ As
  ; F₁ = λ fs → F.F₁ ∙ fs
  ; identity = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≡ = λ fs≡gs → F.F-resp-≡ ∙ fs≡gs
  }
  where
  module F = Functor F

nullary : (X : C.Obj) → Powerendo 0
nullary X = record
  { F₀ = λ _ → X
  ; F₁ = λ _ → C.id
  ; identity = C.Equiv.refl
  ; homomorphism = C.Equiv.sym C.identityˡ
  ; F-resp-≡ = λ _ → C.Equiv.refl
  }

nullaryH : (X : C.Obj) → Hyperendo 0 1
nullaryH X = record
  { F₀ = λ _ _ → X
  ; F₁ = λ _ _ → C.id
  ; identity = λ _ → C.Equiv.refl
  ; homomorphism = λ _ → C.Equiv.sym C.identityˡ
  ; F-resp-≡ = λ _ _ → C.Equiv.refl
  }

binary : (F : Bifunctor C C C) → Powerendo 2
binary F = record
  { F₀ = λ As → F.F₀ (As zero , As (suc zero))
  ; F₁ = λ fs → F.F₁ (fs zero , fs (suc zero))
  ; identity = F.identity
  ; homomorphism = F.homomorphism
  ; F-resp-≡ = λ fs≡gs → F.F-resp-≡ (fs≡gs zero , fs≡gs (suc zero))
  }
  where
  module F = Functor F

binaryH : (F : Bifunctor C C C) → Hyperendo 2 1
binaryH F = record
  { F₀ = λ As _ → F.F₀ (As zero , As (suc zero))
  ; F₁ = λ fs _ → F.F₁ (fs zero , fs (suc zero))
  ; identity = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≡ = λ fs≡gs _ → F.F-resp-≡ (fs≡gs zero , fs≡gs (suc zero))
  }
  where
  module F = Functor F

hyp : ∀ {n} (F : Powerendo n) → Hyperendo n 1
hyp F = record
  { F₀ = λ As _ → F.F₀ As
  ; F₁ = λ fs _ → F.F₁ fs
  ; identity = λ _ → F.identity
  ; homomorphism = λ _ → F.homomorphism
  ; F-resp-≡ = λ fs≡gs _ → F.F-resp-≡ fs≡gs
  }
  where
  module F = Functor F

private
  curryⁿ : ∀ n {a b} {A : Set a} {B : Set b} → ((Fin n → A) → B) → N-ary n A B
  curryⁿ zero f = f (λ ())
  curryⁿ (suc n) {A = A} f = λ x → curryⁿ n (f ∙ addon x)
    where
    addon : A → (Fin n → A) → Fin (suc n) → A
    addon x _ zero = x
    addon _ g (suc i) = g i

plex′ : ∀ {J I} → (J → Powerendo′ I) → Hyperendo′ I J
plex′ Fs = record
  { F₀ = flip (Functor.F₀ ∙ Fs)
  ; F₁ = flip (λ j → Functor.F₁ (Fs j))
  ; identity = λ j → Functor.identity (Fs j)
  ; homomorphism = λ j → Functor.homomorphism (Fs j)
  ; F-resp-≡ = flip (λ j → Functor.F-resp-≡ (Fs j))
  }

plex : ∀ {n} {I} → N-ary n (Powerendo′ I) (Hyperendo′ I (Fin n))
plex {n} = curryⁿ n plex′

widenˡ : ∀ (l : ℕ) {n} (F : Powerendo n) → Powerendo (l + n)
widenˡ l F = record
  { F₀ = λ As → F.F₀ (As ∙ pack)
  ; F₁ = λ {As Bs} fs → F.F₁ (fs ∙ pack)
  ; identity = λ {As} → F.identity
  ; homomorphism = λ {As Bs Cs fs gs} → F.homomorphism
  ; F-resp-≡ = λ {As Bs fs gs} fs≡gs → F.F-resp-≡ (fs≡gs ∙ pack)
  }
  where
  private module F = Functor F
  pack = raise l

widenʳ : ∀ (r : ℕ) {n} (F : Powerendo n) → Powerendo (n + r)
widenʳ r F = record
  { F₀ = λ As → F.F₀ (As ∙ pack)
  ; F₁ = λ {As Bs} fs → F.F₁ (fs ∙ pack)
  ; identity = λ {As} → F.identity
  ; homomorphism = λ {As Bs Cs fs gs} → F.homomorphism
  ; F-resp-≡ = λ {As Bs fs gs} fs≡gs → F.F-resp-≡ (fs≡gs ∙ pack)
  }
  where
  private module F = Functor F
  pack = inject+ r

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Caching evaluation
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term

import Parametric.Syntax.MType as MType
import Parametric.Syntax.MTerm as MTerm

import Parametric.Denotation.Value as Value
import Parametric.Denotation.Evaluation as Evaluation
import Parametric.Denotation.MValue as MValue
import Parametric.Denotation.CachingMValue as CachingMValue
import Parametric.Denotation.MEvaluation as MEvaluation

module Parametric.Denotation.CachingMEvaluation
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (⟦_⟧Const : Evaluation.Structure Const ⟦_⟧Base)
    (ValConst : MTerm.ValConstStructure Const)
    (CompConst : MTerm.CompConstStructure Const)
    (cbnToCompConst : MTerm.CbnToCompConstStructure Const CompConst)
    (cbvToCompConst : MTerm.CbvToCompConstStructure Const CompConst)
    -- I should really switch to records - can it get sillier than this? More
    -- precisely, this is the kind of thing ML functors are designed to replace.
    -- They have also subtyping --- not sure whether that's good or bad.
    (⟦_⟧ValBase : MEvaluation.ValStructure Const ⟦_⟧Base ValConst CompConst cbnToCompConst cbvToCompConst)
    (⟦_⟧CompBase : MEvaluation.CompStructure Const ⟦_⟧Base ValConst CompConst cbnToCompConst cbvToCompConst)
    (ΔBase : CachingMValue.Structure Base ⟦_⟧Base)
  where

open Type.Structure Base
open Term.Structure Base Const

open MType.Structure Base
open MTerm.Structure Const ValConst CompConst cbnToCompConst cbvToCompConst

open Value.Structure Base ⟦_⟧Base
open Evaluation.Structure Const ⟦_⟧Base ⟦_⟧Const
open MValue.Structure Base ⟦_⟧Base
open CachingMValue.Structure Base ⟦_⟧Base ΔBase
open MEvaluation.Structure Const ⟦_⟧Base ValConst CompConst cbnToCompConst cbvToCompConst ⟦_⟧ValBase ⟦_⟧CompBase

open import Base.Denotation.Notation

-- Extension Point: Evaluation of constants.
ValStructure : Set
ValStructure = ∀ {τ} → ValConst τ → ⟦ τ ⟧ValTypeHidCache

CompStructure : Set
CompStructure = ∀ {τ} → CompConst τ → ⟦ τ ⟧CompTypeHidCache

module Structure
       (⟦_⟧ValBaseTermCache  : ValStructure)
       (⟦_⟧CompBaseTermCache : CompStructure)
    where

  {-
  -- Prototype here the type-correctness of a simple non-standard semantics.
  -- This describes a simplified version of the transformation by Liu and
  -- Tanenbaum, PEPM 1995 - but for now, instead of producing object language
  -- terms, we produce host language terms to take advantage of the richer type
  -- system of the host language (in particular, here we need the unit type,
  -- product types and *existentials*).
  --
  -- As usual, we'll later switch to a real term transformation.
  -}
  open import Data.Product hiding (map)
  open import Data.Unit

  -- Defining a caching semantics for Term proves to be hard, requiring to
  -- insert and remove caches where we apply constants.

  -- Indeed, our plugin interface is not satisfactory for adding caching. CBPV can help us.

  -- The solution is to distinguish among different kinds of constants. Some are
  -- value constructors (and thus do not return caches), while others are
  -- computation constructors (and thus should return caches). For products, I
  -- believe we will only use positive/value products (i.e. pattern-match products),
  -- not negative/computation products (i.e. projection products).
  ⟦_⟧CompTermCache : ∀ {τ Γ} → Comp Γ τ → ⟦ Γ ⟧ValCtxHidCache → ⟦ τ ⟧CompTypeHidCache
  ⟦_⟧ValTermCache : ∀ {τ Γ} → Val Γ τ → ⟦ Γ ⟧ValCtxHidCache → ⟦ τ ⟧ValTypeHidCache
  ⟦_⟧ValsTermCache : ∀ {Γ Σ} → Vals Γ Σ → ⟦ Γ ⟧ValCtxHidCache → ⟦ Σ ⟧ValCtxHidCache

  open import Base.Denotation.Environment ValType ⟦_⟧ValTypeHidCache public
    using ()
    renaming (⟦_⟧Var to ⟦_⟧ValVarHidCache)

  -- This says that the environment does not contain caches... sounds wrong!
  -- Either we add extra variables for the caches, or we store computations in
  -- the environment (but that does not make sense), or we store caches in
  -- values, by acting not on F but on something else (U?).

  -- Copy of ⟦_⟧Vals
  ⟦ ∅ ⟧ValsTermCache ρ = ∅
  ⟦ vt • valtms ⟧ValsTermCache ρ = ⟦ vt ⟧ValTermCache ρ • ⟦ valtms ⟧ValsTermCache ρ

  -- I suspect the plan was to use extra variables; that's annoying to model in
  -- Agda but easier in implementations.

  ⟦ vVar   x ⟧ValTermCache ρ = ⟦ x ⟧ValVarHidCache ρ
  ⟦ vThunk x ⟧ValTermCache ρ = ⟦ x ⟧CompTermCache ρ
  -- No caching, because the arguments are values, so evaluating them does not
  -- produce intermediate results.
  ⟦ vConst c ⟧ValTermCache ρ = ⟦ c ⟧ValBaseTermCache

  -- The only caching is done by the interpretation of the constant (because the
  -- arguments are values so need no caching).
  ⟦_⟧CompTermCache (cConst c) ρ = ⟦ c ⟧CompBaseTermCache

  -- Also, where are introduction forms for pairs and sums among values? With
  -- them, we should see that we can interpret them without adding a cache.

  -- Thunks keep seeming noops.
  ⟦_⟧CompTermCache (cForce x) ρ = ⟦ x ⟧ValTermCache ρ

  -- The effect of F is a writer monad of cached values, where the monoid is
  -- (isomorphic to) the free monoid over (∃ τ . τ), but we push the
  -- existentials up when pairing things!

  -- That's what we're interpreting computations in. In fact, one could use
  -- monads directly, but that does not deal with arity satisfactorily.
  ⟦_⟧CompTermCache (cReturn v) ρ = vUnit , (⟦ v ⟧ValTermCache ρ , tt)

  -- A function can invoke, in tail position, either a `cReturn` directly, or
  -- invoke another function. In the latter case, we need to ensure that the
  -- return value of the other function is not forwarded directly, but that
  -- further intermediate results from the current function are also recorded.
  --
  -- At one time, `f1 into cReturn` did this correctly, but `f1` didn't, while
  -- instead, they should be equivalent. In other words, we want `_into_` to
  -- satisfy the monadic laws for bind.

  {-
  -- Here we'd have a problem with the original `_into_` constructor from CBPV, because it does
  -- not require converting expressions to the "CBPV A-normal form".
  --
  -- If we tried supporting it, we could try to write something like:

  ⟦_⟧CompTermCache (v₁ into v₂) ρ =
  -- Sequence commands and combine their caches.
  {-
    let (_ , (r₁ , c₁)) = ⟦ v₁ ⟧CompTermCache ρ
        (_ , (r₂ , c₂)) = ⟦ v₂ ⟧CompTermCache (r₁ • ρ)
    in , (r₂ , (c₁ ,′ c₂))
  -}

  -- However, the code above does not work, because we only guarantee that v₂ is
  -- a computation, not that it's an F-computation - v₂ could also be function
  -- type or a computation product.

  -- Instead, we use a restricted CBPV, where these two possibilities are forbidden.
  -- If you want to save something between different lambdas, you need to add an
  -- F U to reflect that. (Double-check the papers which show how to encode
  -- arity using CBPV, it seems that they should find the same problem ---
  -- XXX they don't).
  -}

  -- But if we alter _into_ as described above, composing the caches works!
  -- However, we should not forget we also need to save the new intermediate
  -- result, that is the one produced by the first part of the let.
  ⟦_⟧CompTermCache (_into_ {σ} {τ} v₁ v₂) ρ =
    let (τ₁ , (r₁ , c₁)) = ⟦ v₁ ⟧CompTermCache ρ
        (τ₂ , (r₂ , c₂)) = ⟦ v₂ ⟧CompTermCache (r₁ • ρ)
    in  (τ₁ v× τ₂ v× σ) , (r₂ ,′ (c₁ ,′ c₂  ,′ r₁))

  -- Note the compositionality and luck: we don't need to do anything at the
  -- cReturn time, we just need the nested into to do their job, because as I
  -- said intermediate results are a writer monad.
  --
  -- Q: But then, do we still need to do all the other stuff? IOW, do we still
  -- need to forbid (λ x . y <- f args; g args') and replace it with (λ x . y <-
  -- f args; z <- g args'; z)?
  --
  -- A: One thing we still need is using the monadic version of into for the
  -- same reasons - which makes sense, since it has the type of monadic bind.
  --
  -- Maybe not: if we use a monad, which respects left and right identity, the
  -- two above forms are equivalent. But what about associativity? We don't have
  -- associativity with nested tuples in the middle. That's why the monad uses
  -- lists! We can also use nested tuple, as long as in the into case we don't
  -- do (a, b) but append a b (ahem, where?), which decomposes the first list
  -- and prepends it to the second. To this end, we need to know the type of the
  -- first element, or to ensure it's always a pair. XXX: We should just reuse
  -- HList.

  -- In abstractions, we should start collecting all variables...

  -- Here, unlike in ⟦_⟧TermCache, we don't need to invent an empty cache,
  -- that's moved into the handling of cReturn. This makes *the* difference for
  -- nested lambdas, where we don't need to create caches multiple times!

  ⟦_⟧CompTermCache (cAbs v) ρ = λ x → ⟦ v ⟧CompTermCache (x • ρ)

  -- Here we see that we are in a sort of A-normal form, because the argument is
  -- a value (not quite ANF though, since values can be thunks - that is,
  -- computations which haven't been run yet, I guess. Do we have an use for
  -- that? That allows passing lambdas as arguments directly - which is fine,
  -- because producing a closure indeed does not have intermediate results!).
  ⟦_⟧CompTermCache (cApp t v) ρ = ⟦ t ⟧CompTermCache ρ (⟦ v ⟧ValTermCache ρ)

  ⟦_⟧TermCacheCBV : ∀ {τ Γ} → Term Γ τ → ⟦ fromCBVCtx Γ ⟧ValCtxHidCache → ⟦ cbvToCompType τ ⟧CompTypeHidCache
  ⟦ t ⟧TermCacheCBV = ⟦ fromCBV t ⟧CompTermCache

  module _ (ι : Base) where
    Γ : ValContext
    Γ = ∅
    σ = B ι
    τ = B ι
    f : Comp Γ (σ ⇛ F τ)
    f = cAbs (cReturn (vVar vThis))

    bar : ⟦ σ ⇛ F τ ⟧CompTypeHidCache
    bar = ⟦ f ⟧CompTermCache ∅

    open import Relation.Binary.PropositionalEquality
    bar≡ : bar ≡ (λ x → vUnit , x , tt)
    bar≡ = refl

    dbar : ⟦ σ ⇛ F τ ⟧ΔCompType
    dbar = λ dx → vUnit , λ c₀ → (dx , c₀)

    barbaz : ⟦ base ι ⟧Type → ⟦ ΔBase ι ⟧Type → ⟦ base ι ⟧Type × ⟦ ΔBase ι ⟧Type
    barbaz x dx =
      let
          (τ₁ , y , c₁) = bar x
          (τ₂ , dbar′) = dbar dx
          (dy , c₂) = dbar′ c₁
      in y , dy
    module _ (f : ⟦ σ ⇛ F τ ⟧CompTypeHidCache) (df : ⟦ σ ⇛ F τ ⟧ΔCompType)
      (proof : ∀ x dx → proj₁ (f x) ≡ proj₁ (df dx)) where

      -- fdf₁ : ⟦ base ι ⟧Type → ⟦ ΔBase ι ⟧Type → ⟦ base ι ⟧Type × ⟦ ΔBase ι ⟧Type
      -- fdf₁ x dx =
      --   let
      --     (τ₁ , y , c₁) = f x
      --     (τ₂ , dbar′) = df dx
      --     --(dy , c₂) = dbar′ c₁ -- fails, as it should be expected!
      --   in y , dy

      fdf : ⟦ base ι ⟧Type → ⟦ ΔBase ι ⟧Type → ⟦ base ι ⟧Type × ⟦ ΔBase ι ⟧Type
      fdf x dx with proof x dx
      ... | p =
        let
          (τ₁ , y , c₁) = f x
          (τ₂ , dbar′) = df dx
          (dy , c₂) = dbar′ (subst ⟦_⟧ValTypeHidCache p c₁) --
        in y , dy

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
--
-- The functions in this module assume some (unenforced) invariants.
-- If you cannot guarantee that your data respects these invariants,
-- you should instead use Text.Tabular.List.
------------------------------------------------------------------------

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

module Text.Tabular.Base where

open import Data.Bool.Base using (if_then_else_)
open import Data.Char.Base using (Char)
open import Data.List.Base as List
  using (List; []; _∷_; _?∷_; _++_; _∷ʳ?_; null; map; intersperse)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe)
open import Data.Nat.Base
open import Data.String.Base as String
  using (String; fromChar; unlines; replicate; length)
open import Function.Base
open import Agda.Builtin.Equality

open String
  using ( Alignment
        ; Left
        ; Center
        ; Right
        ) public

record TabularLine : Set where
  field
    left  : Maybe String
    cont  : Maybe Char
    sep   : String
    right : Maybe String
open TabularLine

record TabularConfig : Set where
  field
    top : Maybe TabularLine
    sep : Maybe TabularLine
    row : TabularLine
    bot : Maybe TabularLine
open TabularConfig

unicode : TabularConfig
unicode .top = just λ where
  .left  → just "┌"
  .cont  → just '─'
  .sep   → "┬"
  .right → just "┐"
unicode .sep = just λ where
  .left  → just "├"
  .cont  → just '─'
  .sep   → "┼"
  .right → just "┤"
unicode .row = λ where
  .left  → just "│"
  .cont  → nothing
  .sep   → "│"
  .right → just "│"
unicode .bot = just λ where
  .left  → just "└"
  .cont  → just '─'
  .sep   → "┴"
  .right → just "┘"

ascii : TabularConfig
ascii .top = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"
ascii .sep = just λ where
  .left  → just "|"
  .cont  → just '-'
  .sep   → "+"
  .right → just "|"
ascii .row = λ where
  .left  → just "|"
  .cont  → nothing
  .sep   → "|"
  .right → just "|"
ascii .bot = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"

compact : TabularConfig → TabularConfig
compact c = record c { sep = nothing }

private
  dropBorder : TabularLine → TabularLine
  dropBorder l = record l { left = nothing; right = nothing }

noBorder : TabularConfig → TabularConfig
noBorder c .top = nothing
noBorder c .sep = Maybe.map dropBorder (c .sep)
noBorder c .row = dropBorder (c .row)
noBorder c .bot = nothing

private
  space : TabularLine → TabularLine
  space l = let pad = maybe fromChar " " (l .cont) in λ where
    .left  → Maybe.map (String._++ pad) (l .left)
    .cont  → l .cont
    .sep   → pad String.++ l .sep String.++ pad
    .right → Maybe.map (pad String.++_) (l .right)

addSpace : TabularConfig → TabularConfig
addSpace c .top = Maybe.map space (c .top)
addSpace c .sep = Maybe.map space (c .sep)
addSpace c .row = space (c .row)
addSpace c .bot = Maybe.map space (c .bot)

whitespace : TabularConfig
whitespace .top = nothing
whitespace .sep = nothing
whitespace .row = λ where
  .left  → nothing
  .cont  → nothing
  .sep   → " "
  .right → nothing
whitespace .bot = nothing

-- /!\ Invariants:
-- * the table is presented as a list of rows
-- * header has the same length as each one of the rows
--   i.e. we have a rectangular table
-- * all of the strings in a given column have the same length

unsafeDisplay : TabularConfig → List (List String) → List String
unsafeDisplay _ []              = []
unsafeDisplay c (header ∷ rows) =
  map String.concat $ th ++ (trs ∷ʳ? lbot) where

  cellsOf : Maybe Char → List String → List String
  cellsOf nothing  = id
  cellsOf (just c) = map (λ cell → replicate (length cell) c)

  lineOf : TabularLine → List String → List String
  lineOf l xs = l .left
            ?∷  intersperse (l .sep) (cellsOf (l .cont) xs)
            ∷ʳ? l .right

  mlineOf : Maybe TabularLine → List String → Maybe (List String)
  mlineOf l xs = Maybe.map (λ l → lineOf l xs) l

  ltop : Maybe (List String)
  lsep : Maybe (List String)
  tr   : List String → List String
  lbot : Maybe (List String)

  ltop = mlineOf (c. top) header
  lsep = mlineOf (c. sep) header
  tr   = lineOf (c. row)
  lbot = mlineOf (c. bot) header

  th  = ltop ?∷ tr header ∷ []
  trs = if null rows then id else (maybe _∷_ id lsep)
      $ maybe intersperse id lsep
      $ map tr rows


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

open import HoTT
open import homotopy.elims.Lemmas

module homotopy.elims.SuspSmash {i j k} {X : Ptd i} {Y : Ptd j}
  {P : Susp (X ∧ Y) → Type k}
  (north* : P north) (south* : P south)
  (smin* : (x : de⊙ X) (y : de⊙ Y) → north* == south* [ P ↓ merid (smin x y) ])
  where

private
  smbase*-template : ∀ {s} (p : smin (pt X) (pt Y) == s)
    → north* == south* [ P ↓ merid s ]
  smbase*-template p = transport (λ κ → north* == south* [ P ↓ merid κ ])
    p (smin* (pt X) (pt Y))

  smbasel* = smbase*-template (smgluel (pt X))
  smbaser* = smbase*-template (smgluer (pt Y))

  -- note that [smin*] is adjusted.
  coh* : (s : X ∧ Y) → north* == south* [ P ↓ merid s ]
  coh* = Smash-elim
    (λ x y → fst (fill-l x) ◃ fst (fill-r y) ◃ fst fill-base ◃ smin* x y)
    smbasel* smbaser*
    (λ x → ↓↓-from-squareover $
           ap (λ p → fst (fill-l x) ◃ p ◃ fst fill-base ◃ smin* x (pt Y)) fill-r-β
      ∙h↓⊡ ap (fst (fill-l x) ◃_) (idp◃ _)
      ∙h↓⊡ snd (fill-l x))
    (λ y → ↓↓-from-squareover $
           ap (λ p → p ◃ fst (fill-r y) ◃ fst fill-base ◃ smin* (pt X) y) fill-l-β
      ∙h↓⊡ idp◃ _
      ∙h↓⊡ snd (fill-r y))
    where
    fill-template : ∀ {s₁ s₂} (p : s₁ == s₂)
      (α : north* == south* [ P ↓ merid s₁ ])
      (β : north* == south* [ P ↓ merid s₂ ])
      → Σ (north* == north*)
          (λ q → SquareOver P (natural-square merid p)
                   (q ◃ α)
                   (↓-ap-in _ _ (apd (λ _ → north*) p))
                   (↓-ap-in _ _ (apd (λ _ → south*) p))
                   β)
    fill-template p α β = fill-upper-left _ _ _ _ _

    fill-base = fill-template (smgluel (pt X)) (smin* (pt X) (pt Y)) smbasel*
    fill-l = λ x → fill-template (smgluel x) (fst fill-base ◃ smin* x (pt Y)) smbasel*
    fill-l-β : fst (fill-l (pt X)) == idp
    fill-l-β = ! $
      fill-upper-left-unique _ _ _ _ _ idp (idp◃ _ ∙h↓⊡ snd fill-base)

    fill-r = λ y → fill-template (smgluer y) (fst fill-base ◃ smin* (pt X) y) smbaser*
    fill-r-β : fst (fill-r (pt Y)) == idp
    fill-r-β = ! $
      fill-upper-left-unique _ _ _ _ _ idp (idp◃ _ ∙h↓⊡ snd fill-base)
      ∙ ap (λ sp → fst (fill-template (snd sp)
                                      (fst fill-base ◃ smin* (pt X) (pt Y))
                                      (smbase*-template (snd sp))))
           (contr-has-all-paths {{pathfrom-is-contr (smin (pt X) (pt Y))}}
                                (smbasel , smgluel (pt X))
                                (smbaser , smgluer (pt Y)))

SuspSmash-elim : Π (Susp (X ∧ Y)) P
SuspSmash-elim = Susp-elim north* south* coh*

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --prop --show-irrelevant #-}

postulate
  P : Prop
  p : P
  A : P → Set
  f : {x : P} → A x

test : A p
test = f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-11-06, issue #2840 reported by wenkokke

Id : (F : Set → Set) → Set → Set
Id F = F

data D (A : Set) : Set where
  c : Id _ A

-- WAS: internal error in positivity checker

-- EXPECTED: success, or
-- Failed to solve the following constraints:
--   [4] _F_2 A A = D A : Set
-- when checking the constructor c in the declaration of D


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory
open import cohomology.CofiberSequence

module cohomology.LongExactSequence {i} (CT : CohomologyTheory i)
  (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

open CohomologyTheory CT

long-exact-diag : ExactDiag _ _
long-exact-diag =
  C n (⊙Susp (⊙Cof f))  ⟨ CF-hom n (⊙susp-fmap (⊙cfcod f)) ⟩→
  C n (⊙Susp Y)         ⟨ CF-hom n (⊙susp-fmap f)          ⟩→
  C n (⊙Susp X)         ⟨ CF-hom n ⊙ext-glue               ⟩→
  C n (⊙Cof f)          ⟨ CF-hom n (⊙cfcod f)              ⟩→
  C n Y                 ⟨ CF-hom n f                       ⟩→
  C n X                 ⊣|

long-exact-cofiber : ExactSeq long-exact-diag
long-exact-cofiber = transport
  (λ {(_ , g , h , k) → ExactSeq $
    _ ⟨ CF-hom n k ⟩→ _ ⟨ CF-hom n h ⟩→ _ ⟨ CF-hom n g ⟩→
    _ ⟨ CF-hom n (⊙cfcod f) ⟩→ _ ⟨ CF-hom n f ⟩→ _ ⊣|})
  (cofiber-sequence f)
  (exact-build
    (_ ⟨ CF-hom n (⊙cfcod⁴ f) ⟩→ _ ⟨ CF-hom n (⊙cfcod³ f) ⟩→
     _ ⟨ CF-hom n (⊙cfcod² f) ⟩→ _ ⟨ CF-hom n (⊙cfcod f) ⟩→
     _ ⟨ CF-hom n f ⟩→ _ ⊣|)
    (C-exact n (⊙cfcod³ f)) (C-exact n (⊙cfcod² f))
    (C-exact n (⊙cfcod f)) (C-exact n f))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module UnSizedIO.IOObject where

open import Data.Product

open import UnSizedIO.Base
open import UnSizedIO.Object

-- An IO object is like a simple object,
-- but the method returns IO applied to the result type of a simple object
-- which means the method returns an IO program which when terminating
-- returns the result of the simple object

module _  (ioi  : IOInterface)  (let C  = Command ioi)  (let R   = Response ioi)
          (oi   : Interface)   (let M  = Method oi)    (let Rt  = Result oi)
  where

  record IOObject : Set where
    coinductive
    field
      method : (m : M) → IO ioi (Rt m × IOObject)

open IOObject public

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --copatterns #-}

open import Common.Size
open import Common.Prelude
open import Common.Product renaming (proj₁ to fst; proj₂ to snd)

record Stream (i : Size) (A : Set) : Set where
  coinductive
  field force : ∀{j : Size< i} → A × Stream j A
open Stream

head : ∀{i A} → Stream (↑ i) A →  A
head s = fst (force s)

tail : ∀{i A} → Stream (↑ i) A → Stream i A
tail s = snd (force s)

smap : ∀{i A B} (f : A → B) → Stream i A → Stream i B
force (smap f s) with force s
... | a , as = f a , smap f as

scanl : ∀{i A B} (f : B → A → B) (b : B) (s : Stream i A) → Stream i B
force (scanl f b s) with force s
... | a , as = b , scanl f (f b a) as

_!_ : ∀{A} (s : Stream _ A) (n : Nat) → A
s ! zero  = head s
s ! suc n = tail s ! n

_!!_ : ∀{A} (s : Stream _ A) (n : Nat) → A
s !! n with force s
_ !! zero  | a , as = a
_ !! suc n | a , as = as !! n

nats : ∀{i} → Stream i Nat
force nats = 0 , smap suc nats

sums : Stream _ Nat
sums = scanl (_+_) 0 (tail nats)

main : IO Unit
main = printNat (sums ! 100)
-- Expected output, due to Gauss: 5050


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

module Space where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; suc)
  renaming (_+_ to _ℕ+_; _*_ to _ℕ*_; _⊔_ to _ℕ⊔_)
open import Data.Nat.Properties
open import Data.Integer as ℤ using (ℤ; +_; -[1+_]; ∣_∣; _+_; _⊔_; -_)
open import Data.Rational
  using (ℚ)
  renaming (1/_ to recip)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Maybe
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Binary.PropositionalEquality
  renaming ([_] to R[_])
  using (_≡_; refl; sym; trans; cong; inspect)
open import Data.Unit using (⊤; tt)

open import Singleton
open import PiFrac

------------------------------------------------------------------------------
-- Space denotational semantics

-- for each type, we calculate its memory requirements which are two
-- numbers (m , z). The number m represents the amount of space needed
-- to store values of the type. The number z represents the effect of
-- the value on space when it is interpreted. Ex. a gc process needs m
-- bits to be stored but when run it releases z bits.

-- Number of points in type
card : (t : 𝕌) → ℕ
card 𝟘 = 0
card 𝟙 = 1
card (t₁ +ᵤ t₂) = card t₁ ℕ+ card t₂
card (t₁ ×ᵤ t₂) = card t₁ ℕ* card t₂
card ● t [ v ] = 1
card 𝟙/● t [ v ] = 1

-- If number of points is zero then it is impossible to find a value
-- of the type
0empty : {t : 𝕌} → card t ≡ 0 → (v : ⟦ t ⟧) → ⊥
0empty {𝟘} _ ()
0empty {𝟙} () tt
0empty {t₁ +ᵤ t₂} s (inj₁ v₁)
  with card t₁ | card t₂ | inspect card t₁
0empty {t₁ +ᵤ t₂} refl (inj₁ v₁) | ℕ.zero | ℕ.zero | R[ s₁ ] =
  0empty {t₁} s₁ v₁
0empty {t₁ +ᵤ t₂} s (inj₂ v₂)
  with card t₁ | card t₂ | inspect card t₂
0empty {t₁ +ᵤ t₂} refl (inj₂ v₂) | ℕ.zero | ℕ.zero | R[ s₂ ] =
  0empty {t₂} s₂ v₂
0empty {t₁ ×ᵤ t₂} s (v₁ , v₂)
  with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
0empty {t₁ ×ᵤ t₂} refl (v₁ , v₂) | ℕ.zero | _ | R[ s₁ ] | _ =
  0empty {t₁} s₁ v₁
0empty {t₁ ×ᵤ t₂} s (v₁ , v₂) | ℕ.suc n₁ | ℕ.zero | R[ s₁ ] | R[ s₂ ] =
  0empty {t₂} s₂ v₂
0empty {● t [ v ]} () (.v , refl)
0empty {𝟙/● t [ v ]} () f

-- Space effects

-- For a pointed type, even though we only have one value, that value
-- could be large and we need just as much space to store it as we
-- would need for any value of the given type. For a fractional type,
-- the effect is to de-allocate the space above.

space : (t : 𝕌) → {¬t≡0 : ¬ card t ≡ 0} → ℤ
space 𝟘 {0ne} = ⊥-elim (0ne refl)
space 𝟙 = + 0
space (t₁ +ᵤ t₂) {pne} with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
... | 0 | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (pne refl)
... | 0 | suc n | R[ s₁ ] | R[ s₂ ] =
  space t₂ {λ t2≡0 → ⊥-elim (pne (trans (sym s₂) t2≡0))}
... | suc m | 0 | R[ s₁ ] | R[ s₂ ] =
  space t₁
    {λ t1≡0 →
      ⊥-elim (pne (trans (sym (trans s₁ (sym (+-identityʳ (suc m))))) t1≡0))}
... | suc m | suc n | R[ s₁ ] | R[ s₂ ] =
  + 1 + (space t₁ {λ t1≡0 → ⊥-elim (1+n≢0 (trans (sym s₁) t1≡0))} ⊔
         space t₂ {λ t2≡0 → ⊥-elim ((1+n≢0 (trans (sym s₂) t2≡0)))})
space (t₁ ×ᵤ t₂) {pne} with card t₁ | card t₂ | inspect card t₁ | inspect card t₂
... | 0 | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (pne refl)
... | 0 | suc n | R[ s₁ ] | R[ s₂ ] = ⊥-elim (pne refl)
... | suc m | 0 | R[ s₁ ] | R[ s₂ ] = ⊥-elim (pne (*-zeroʳ (suc m)))
... | suc m | suc n | R[ s₁ ] | R[ s₂ ] =
  space t₁ {λ t1≡0 → ⊥-elim (1+n≢0 (trans (sym s₁) t1≡0))} +
  space t₂ {λ t2≡0 → ⊥-elim (1+n≢0 (trans (sym s₂) t2≡0))}
space ● t [ v ]   = space t {λ t≡0 → 0empty t≡0 v}
space 𝟙/● t [ v ] = - space t {λ t≡0 → 0empty t≡0 v}

-- TODO

-- Every combinator preserves space effects

card= : (t₁ t₂ : 𝕌) (C : t₁ ⟷ t₂) → (card t₁ ≡ card t₂)
card= .(𝟘 +ᵤ t₂) t₂ unite₊l  = refl
card= t₁ .(𝟘 +ᵤ t₁) uniti₊l  = refl
card= .(t₂ +ᵤ 𝟘) t₂ unite₊r  rewrite +-identityʳ (card t₂) = refl
card= t₁ .(t₁ +ᵤ 𝟘) uniti₊r  rewrite +-identityʳ (card t₁) = refl
card= (t₁ +ᵤ t₂) _ swap₊  rewrite +-comm (card t₁) (card t₂) = refl
card= (t₁ +ᵤ t₂ +ᵤ t₃) _ assocl₊  rewrite +-assoc (card t₁) (card t₂) (card t₃) = refl
card= ((t₁ +ᵤ t₂) +ᵤ t₃) _ assocr₊  rewrite +-assoc (card t₁) (card t₂) (card t₃) = refl
card= (𝟙 ×ᵤ t₂) t₂ unite⋆l  rewrite +-identityʳ (card t₂) = refl
card= t₁ (𝟙 ×ᵤ t₁) uniti⋆l  rewrite +-identityʳ (card t₁) = refl
card= (t₂ ×ᵤ 𝟙) t₂ unite⋆r  rewrite *-identityʳ (card t₂) = refl
card= t₁ (t₁ ×ᵤ 𝟙) uniti⋆r  rewrite *-identityʳ (card t₁) = refl
card= (t₁ ×ᵤ t₂) _ swap⋆  rewrite *-comm (card t₁) (card t₂) = refl
card= (t₁ ×ᵤ t₂ ×ᵤ t₃) _ assocl⋆  rewrite *-assoc (card t₁) (card t₂) (card t₃) = refl
card= ((t₁ ×ᵤ t₂) ×ᵤ t₃) _ assocr⋆  rewrite *-assoc (card t₁) (card t₂) (card t₃) = refl
card= .(𝟘 ×ᵤ _) .𝟘 absorbr  = refl
card= (t ×ᵤ 𝟘) .𝟘 absorbl  rewrite *-zeroʳ (card t) = refl
card= .𝟘 (t ×ᵤ 𝟘) factorzr  rewrite *-zeroʳ (card t) = refl
card= .𝟘 .(𝟘 ×ᵤ _) factorzl  = refl
card= ((t₁ +ᵤ t₂) ×ᵤ t₃) _ dist  rewrite *-distribʳ-+ (card t₃) (card t₁) (card t₂) = refl
card= _ ((t₁ +ᵤ t₂) ×ᵤ t₃) factor  rewrite *-distribʳ-+ (card t₃) (card t₁) (card t₂) = refl
card= (t₃ ×ᵤ (t₁ +ᵤ t₂)) _ distl  rewrite *-distribˡ-+ (card t₃) (card t₁) (card t₂) = refl
card= _ (t₃ ×ᵤ (t₁ +ᵤ t₂)) factorl  rewrite *-distribˡ-+ (card t₃) (card t₁) (card t₂) = refl
card= t₁ .t₁ id⟷  = refl
card= t₁ t₂ (c₁ ⊚ c₂)  rewrite card= _ _ c₁ | card= _ _ c₂ = refl
card= (t₁ +ᵤ t₂) (t₃ +ᵤ t₄) (c₁ ⊕ c₂) rewrite card= _ _ c₁ | card= _ _ c₂ = refl
card= (t₁ ×ᵤ t₂) (t₃ ×ᵤ t₄) (c₁ ⊗ c₂) rewrite card= _ _ c₁ | card= _ _ c₂ = refl
card= .(● _ [ _ ]) .(● _ [ eval c _ ]) (lift c)  = refl
card= .(● _ ×ᵤ _ [ _ , _ ]) .(● _ [ _ ] ×ᵤ ● _ [ _ ]) tensorl  = refl
card= .(● _ [ _ ] ×ᵤ ● _ [ _ ]) .(● _ ×ᵤ _ [ _ , _ ]) tensorr  = refl
card= .(● _ +ᵤ _ [ inj₁ _ ]) .(● _ [ _ ]) plusll  = refl
card= .(● _ [ _ ]) .(● _ +ᵤ _ [ inj₁ _ ]) pluslr = refl
card= .(● _ +ᵤ _ [ inj₂ _ ]) .(● _ [ _ ]) plusrl  = refl
card= .(● _ [ _ ]) .(● _ +ᵤ _ [ inj₂ _ ]) plusrr = refl
card= .(𝟙/● _ ×ᵤ _ [ _ , _ ]) .(𝟙/● _ [ _ ] ×ᵤ 𝟙/● _ [ _ ]) fracl  = refl
card= .(𝟙/● _ [ _ ] ×ᵤ 𝟙/● _ [ _ ]) .(𝟙/● _ ×ᵤ _ [ _ , _ ]) fracr  = refl
card= .𝟙 .(● _ [ v ] ×ᵤ 𝟙/● _ [ v ]) (η v)  = refl
card= .(● _ [ v ] ×ᵤ 𝟙/● _ [ v ]) .𝟙 (ε v)  = refl
card= .(● _ [ _ ]) .(● _ [ _ ]) (== c x)  = refl
card= .(● (● t [ v ]) [ w ]) .(● t [ v ]) (ll {t} {v} {w}) = refl

space= : (t₁ t₂ : 𝕌) → (c : t₁ ⟷ t₂) → Set
space= t₁ t₂ c with card t₁ ≟ 0
space= t₁ t₂ c | yes _ = ⊤
space= t₁ t₂ c | no  nz₁ = space t₁ {nz₁} ≡ space t₂ {λ nz₂ → nz₁ (trans (card= _ _ c) nz₂)}

space≡ : (t₁ t₂ : 𝕌) → (c : t₁ ⟷ t₂) → space= t₁ t₂ c
space≡ t₁ t₂ c with card t₁ ≟ 0
space≡ t₁ t₂ c | yes _ = tt
space≡ t₁ t₂ c | no nz₁ = {!!}

-- Groupoid interpretation ???? Groupoid for pointed 1/A is point and
-- (size A) loops on point labeled (= a1), (= a2), (= a3), etc.

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
_∘_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set₁} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

postulate
  R : {A : Set₁} → A → A → Set₁

_≡_ : {A : Set₁} → A → A → Set₁
_≡_ = R

data D (A : Set) : Set where
  c : A → D A

postulate
  cong  : {A B : Set₁} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
  refl  : {A : Set₁} {x : A} → x ≡ x
  A     : Set
  P     : D A → Set
  p     : (F : A → Set) → (P ∘ c) ≡ F → (P ∘ c) ≡ F
  eq    : P ≡ P

_ : p (P ∘ c) (cong (_∘ c) eq) ≡ p (P ∘ c) (cong (_∘ c) eq)
_ = cong (λ eq → p _ eq) (cong (cong (_∘ c)) refl)


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types --guardedness #-}

open import Data.Product
open import Data.Vec
open import Data.Unit
open import Codata.Colist
open import Agda.Builtin.Equality
open import Size
open import Data.Nat
open import Data.Fin
open import Codata.Thunk
open import Relation.Unary using (_⊆_)
open import Examples.Colists.Auxiliary.Colist_member

open import is-lib.InfSys

module Examples.Colists.allPos where

  U = Colist ℕ ∞

  data allPosRN : Set where
    allp-Λ allp-t : allPosRN

  allP-Λ-r : FinMetaRule U
  allP-Λ-r .Ctx = ⊤
  allP-Λ-r .comp c =
    [] ,
    -----------------
    []

  allP-t-r : FinMetaRule U
  allP-t-r .Ctx = Σ[ (x , _) ∈ ℕ × Thunk (Colist ℕ) ∞ ] x Data.Nat.> 0
  allP-t-r .comp ((x , xs) , _) =
    xs .force ∷ [] ,
    -----------------
    x ∷ xs

  allPosIS : IS U
  allPosIS .Names = allPosRN
  allPosIS .rules allp-Λ = from allP-Λ-r
  allPosIS .rules allp-t = from allP-t-r

  allPos : U → Set
  allPos = CoInd⟦ allPosIS ⟧

  allPosSpec : U → Set
  allPosSpec xs = ∀{x} → x ∈ xs → x Data.Nat.> 0

  allPosSound : allPos ⊆ allPosSpec
  allPosSound {x ∷ xs} ap mem with ap .CoInd⟦_⟧.unfold
  allPosSound {x ∷ xs} ap here | allp-t , ((.x , .xs) , x>0) , refl , prem = x>0
  allPosSound {x ∷ xs} ap (there mem) | allp-t , ((.x , .xs) , _) , refl , prem = allPosSound (prem zero) mem

  allPosSpecCons : ∀{xs} → allPosSpec xs → ISF[ allPosIS ] allPosSpec xs
  allPosSpecCons {[]} _ = allp-Λ , (tt , (refl , λ ()))
  allPosSpecCons {(x ∷ xs)} Sxs = allp-t , (((x , xs) , Sxs here) , (refl , λ {Fin.zero → λ mem → Sxs (there mem)}))

  allPosComplete : allPosSpec ⊆ allPos
  allPosComplete = coind[ allPosIS ] allPosSpec allPosSpecCons

  {- allPos as Container -}

  open import Data.Empty using (⊥)
  open import Data.Container.Indexed
  open import is-lib.InfSys.Container U
  open ISCont

  allPosCont : ISCont
  allPosCont .Command [] = ⊤
  allPosCont .Command (x ∷ xs) = x Data.Nat.> 0
  allPosCont .Response {[]} tt = ⊥
  allPosCont .Response {_ ∷ _} _ = Fin 1
  allPosCont .next {_ ∷ xs} _ zero = xs .force

  allPosC : U → Set
  allPosC = ISCont.CoInd⟦ allPosCont ⟧

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
module Cats.Bifunctor where

open import Data.Product using (_,_)
open import Level using (_⊔_)
open import Relation.Binary using (IsEquivalence ; _Preserves₂_⟶_⟶_)

open import Cats.Category
open import Cats.Category.Cat using (_∘_ ; ∘-resp ; _≈_ ; equiv)
open import Cats.Category.Cat.Facts.Product using (Swap ; hasBinaryProducts)
open import Cats.Category.Fun using (Fun ; Trans ; ≈-intro ; ≈-elim)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Category.Product.Binary.Facts using (iso-intro)
open import Cats.Functor using (Functor)
open import Cats.Trans.Iso using (NatIso)
open import Cats.Util.Simp using (simp!)

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Fun.Facts as Fun

open Functor
open Trans
open Iso.Build._≅_

module _ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″} where

  Bifunctor
    : Category lo la l≈
    → Category lo′ la′ l≈′
    → Category lo″ la″ l≈″
    → Set (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′ ⊔ lo″ ⊔ la″ ⊔ l≈″)
  Bifunctor C D E = Functor (C × D) E

  module _
    {C : Category lo la l≈}
    {D : Category lo′ la′ l≈′}
    {E : Category lo″ la″ l≈″}
    where

    private
      module C = Category C
      module D = Category D
      module E = Category E

    biobj : Bifunctor C D E → C.Obj → D.Obj → E.Obj
    biobj F c d = fobj F (c , d)

    bimap
      : (F : Bifunctor C D E)
      → ∀ {A B A′ B′}
      → (A C.⇒ B)
      → (A′ D.⇒ B′)
      → biobj F A A′ E.⇒ biobj F B B′
    bimap F f g = fmap F (f , g)

    Bifunctor→Functor₁ : Bifunctor C D E → C.Obj → Functor D E
    Bifunctor→Functor₁ F x = record
        { fobj = λ d → fobj F (x , d)
        ; fmap = λ f → fmap F (C.id , f)
        ; fmap-resp = λ x≈y → fmap-resp F (C.≈.refl , x≈y)
        ; fmap-id = fmap-id F
        ; fmap-∘ = λ where
            {f = f} {g} →
              begin
                fmap F (C.id , f) E.∘ fmap F (C.id , g)
              ≈⟨ fmap-∘ F ⟩
                fmap F (C.id C.∘ C.id , f D.∘ g)
              ≈⟨ fmap-resp F (C.id-l , D.≈.refl) ⟩
                fmap F (C.id , f D.∘ g)
              ∎
        }
      where
        open E.≈-Reasoning

    Bifunctor→Functor₁-resp : ∀ {F G x y}
      → F ≈ G
      → x C.≅ y
      → Bifunctor→Functor₁ F x ≈ Bifunctor→Functor₁ G y
    Bifunctor→Functor₁-resp {F} {G} {x} {y}
      record { iso = Fx≅Gx ; forth-natural = fnat } x≅y
        = record
        { iso = λ {z} →
            let open E.≅-Reasoning in
            begin
              fobj F (x , z)
            ≈⟨ Fx≅Gx ⟩
              fobj G (x , z)
            ≈⟨ fobj-resp G (iso-intro x≅y D.≅.refl) ⟩
              fobj G (y , z)
            ∎
        ; forth-natural = λ {c} {d} {f} →
            let open E.≈-Reasoning in
            triangle (fmap G (forth x≅y , f) E.∘ forth Fx≅Gx)
            ( begin
                ((E.id E.∘ fmap G (forth x≅y , D.id)) E.∘ forth Fx≅Gx) E.∘ fmap F (C.id , f)
              ≈⟨ simp! E ⟩
                fmap G (forth x≅y , D.id) E.∘ forth Fx≅Gx E.∘ fmap F (C.id , f)
              ≈⟨ E.∘-resp-r fnat ⟩
                fmap G (forth x≅y , D.id) E.∘ (fmap G (C.id , f) E.∘ forth Fx≅Gx)
              ≈⟨ simp! E ⟩
                (fmap G (forth x≅y , D.id) E.∘ fmap G (C.id , f)) E.∘ forth Fx≅Gx
              ≈⟨ E.∘-resp-l (fmap-∘ G) ⟩
                fmap G (forth x≅y C.∘ C.id , D.id D.∘ f) E.∘ forth Fx≅Gx
              ≈⟨ E.∘-resp-l (fmap-resp G (C.id-r , D.id-l)) ⟩
                fmap G (forth x≅y , f) E.∘ forth Fx≅Gx
              ∎
            )
            ( begin
                fmap G (C.id , f) E.∘ (E.id E.∘ fmap G (forth x≅y , D.id)) E.∘ forth Fx≅Gx
              ≈⟨ E.∘-resp-r (E.∘-resp-l E.id-l) ⟩
                fmap G (C.id , f) E.∘ fmap G (forth x≅y , D.id) E.∘ forth Fx≅Gx
              ≈⟨ simp! E ⟩
                (fmap G (C.id , f) E.∘ fmap G (forth x≅y , D.id)) E.∘ forth Fx≅Gx
              ≈⟨ E.∘-resp-l (fmap-∘ G) ⟩
                fmap G (C.id C.∘ forth x≅y , f D.∘ D.id) E.∘ forth Fx≅Gx
              ≈⟨ E.∘-resp-l (fmap-resp G (C.id-l , D.id-r)) ⟩
                fmap G (forth x≅y , f) E.∘ forth Fx≅Gx
              ∎
            )
        }

    transposeBifunctor₁ : Bifunctor C D E → Functor C (Fun D E)
    transposeBifunctor₁ F = record
        { fobj = Bifunctor→Functor₁ F
        ; fmap = λ {a} {b} f → record
            { component = λ d → fmap F (f , D.id)
            ; natural = λ {a′} {b′} {g} →
                begin
                  fmap F (f , D.id) E.∘ fmap (Bifunctor→Functor₁ F a) g
                ≈⟨ fmap-∘ F ⟩
                  fmap F (f C.∘ C.id , D.id D.∘ g)
                ≈⟨ fmap-resp F
                    ( (C.≈.trans C.id-r (C.≈.sym C.id-l))
                    , D.≈.trans D.id-l (D.≈.sym D.id-r) ) ⟩
                  fmap F (C.id C.∘ f , g D.∘ D.id)
                ≈⟨ E.≈.sym (fmap-∘ F) ⟩
                  fmap (Bifunctor→Functor₁ F b) g E.∘ fmap F (f , D.id)
                ∎
            }
        ; fmap-resp = λ x≈y → ≈-intro (fmap-resp F (x≈y , D.≈.refl))
        ; fmap-id = ≈-intro (fmap-id F)
        ; fmap-∘ = λ where
            {f = f} {g} → ≈-intro (
              begin
                fmap F (f , D.id) E.∘ fmap F (g , D.id)
              ≈⟨ fmap-∘ F ⟩
                fmap F (f C.∘ g , D.id D.∘ D.id)
              ≈⟨ fmap-resp F (C.≈.refl , D.id-l) ⟩
                fmap F (f C.∘ g , D.id)
              ∎)
        }
      where
        open E.≈-Reasoning

    transposeBifunctor₁-resp : ∀ {F G}
      → F ≈ G
      → transposeBifunctor₁ F ≈ transposeBifunctor₁ G
    transposeBifunctor₁-resp {F} {G} F≈G = record
        { iso = Fun.≈→≅ (Bifunctor→Functor₁-resp F≈G C.≅.refl)
        ; forth-natural = λ {c} {d} {f} → ≈-intro (
            let open E.≈-Reasoning in
            triangle (fmap G (f , D.id) E.∘ forth (iso F≈G))
            ( begin
                ((E.id E.∘ fmap G (C.id , D.id)) E.∘ forth (iso F≈G)) E.∘ fmap F (f , D.id)
              ≈⟨ E.∘-resp-l (E.≈.trans (E.∘-resp-l (E.≈.trans E.id-l (fmap-id G))) E.id-l) ⟩
                forth (iso F≈G) E.∘ fmap F (f , D.id)
              ≈⟨ forth-natural F≈G ⟩
                (fmap G (f , D.id) E.∘ forth (iso F≈G))
              ∎
            )
            ( begin
                fmap G (f , D.id) E.∘ (E.id E.∘ fmap G (C.id , D.id)) E.∘ forth (iso F≈G)
              ≈⟨ E.∘-resp-r (E.≈.trans (E.∘-resp-l (E.≈.trans E.id-l (fmap-id G))) E.id-l) ⟩
                fmap G (f , D.id) E.∘ forth (iso F≈G)
              ∎
            ))
        }
      where
        open E.≈-Reasoning
        open NatIso using (iso ; forth-natural)

module _
  {lo la l≈} {C : Category lo la l≈}
  {lo′ la′ l≈′} {D : Category lo′ la′ l≈′}
  {lo″ la″ l≈″} {E : Category lo″ la″ l≈″}
  where

  private
    module C = Category C
    module D = Category D
    module E = Category E

  Bifunctor→Functor₂ : Bifunctor C D E → D.Obj → Functor C E
  Bifunctor→Functor₂ F x = Bifunctor→Functor₁ (F ∘ Swap) x

  Bifunctor→Functor₂-resp : ∀ {F G x y}
    → F ≈ G
    → x D.≅ y
    → Bifunctor→Functor₂ F x ≈ Bifunctor→Functor₂ G y
  Bifunctor→Functor₂-resp {F} {G} F≈G x≅y
      = Bifunctor→Functor₁-resp {F = F ∘ Swap} {G = G ∘ Swap} (∘-resp F≈G refl) x≅y
    where
      open IsEquivalence equiv

  transposeBifunctor₂ : Bifunctor C D E → Functor D (Fun C E)
  transposeBifunctor₂ F = transposeBifunctor₁ (F ∘ Swap)

  transposeBifunctor₂-resp : ∀ {F G}
    → F ≈ G → transposeBifunctor₂ F ≈ transposeBifunctor₂ G
  transposeBifunctor₂-resp {F} {G} F≈G
      = transposeBifunctor₁-resp {F = F ∘ Swap} {G = G ∘ Swap} (∘-resp F≈G refl)
    where
      open IsEquivalence equiv

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------
-- Banker's queues (following Okasaki)
------------------------------------------------------------------------

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

open import Equality

module Queue.Bankers {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Bijection eq using (_↔_)
open import Erased.Without-box-cong eq as Erased hiding (map)
open import Function-universe eq hiding (id; _∘_)
open import List eq as L hiding (map)
open import Nat eq
open import Surjection eq using (_↠_)
open import Tactic.By.Parametrised eq

private
  variable
    a ℓ ℓ₁ ℓ₂ : Level
    A B       : Type a
    p q x     : A
    f         : A → B
    b         : Bool
    xs        : List A

------------------------------------------------------------------------
-- Queues

-- Queues.
--
-- Note that the invariant is erased.

record Queue (A : Type a) : Type a where
  field
    front rear               : List A
    length-front length-rear : ℕ
    @0 length-invariant      : length-rear ≤ length-front
    @0 length-front≡         : length-front ≡ length front
    @0 length-rear≡          : length-rear  ≡ length rear

open Queue public

------------------------------------------------------------------------
-- Conversion functions

-- Converts queues to lists.

to-List : Queue A → List A
to-List q = q .front ++ reverse (q .rear)

-- Converts lists to queues.

from-List : List A → Queue A
from-List xs = record
  { front            = xs
  ; rear             = []
  ; length-front     = length xs
  ; length-rear      = 0
  ; length-invariant = zero≤ _
  ; length-front≡    = refl _
  ; length-rear≡     = refl _
  }

-- The function from-List is a right inverse of to-List.

to-List-from-List : to-List (from-List xs) ≡ xs
to-List-from-List {xs = xs} =
  xs ++ []  ≡⟨ ++-right-identity _ ⟩∎
  xs        ∎

------------------------------------------------------------------------
-- Queues with broken invariants

private

  -- Queues where the invariant may have been broken (slightly).

  record Almost-queue (A : Type a) : Type a where
    field
      front rear               : List A
      length-front length-rear : ℕ
      @0 length-invariant      : length-rear ≤ suc length-front
      @0 length-front≡         : length-front ≡ length front
      @0 length-rear≡          : length-rear  ≡ length rear

  open Almost-queue

  -- Some conversion functions.

  from-Almost-queue : Almost-queue A → List A
  from-Almost-queue q = q .front ++ reverse (q .rear)

  to-Almost-queue : Queue A → Almost-queue A
  to-Almost-queue q = record
    { front            = q .front
    ; rear             = q .rear
    ; length-front     = q .length-front
    ; length-rear      = q .length-rear
    ; length-front≡    = q .length-front≡
    ; length-rear≡     = q .length-rear≡
    ; length-invariant = ≤-step (q .length-invariant)
    }

  -- Restores the invariant by rotating the queue, if necessary.

  rotate′ :
    (q : Almost-queue A) (b : Bool) →
    @0 T b ↔ suc (q .length-front) ≡ q .length-rear →
    Queue A
  rotate′ q true _ = record
    { front            = q .front ++ reverse (q .rear)
    ; rear             = []
    ; length-front     = q .length-front + q .length-rear
    ; length-rear      = 0
    ; length-invariant = zero≤ _
    ; length-rear≡     = refl _
    ; length-front≡    =
        ⟨ q .length-front ⟩ + q .length-rear                ≡⟨ ⟨by⟩ (q .length-front≡) ⟩
        length (q .front) + ⟨ q .length-rear ⟩              ≡⟨ ⟨by⟩ (q .length-rear≡) ⟩
        length (q .front) + ⟨ length (q .rear) ⟩            ≡⟨ ⟨by⟩ (length-reverse (q .rear)) ⟩
        ⟨ length (q .front) + length (reverse (q .rear)) ⟩  ≡⟨ ⟨by⟩ (length-++ (q .front)) ⟩∎
        length (q .front ++ reverse (q .rear))              ∎
    }
  rotate′ q false 1+f≢r = record
    { front            = q .front
    ; rear             = q .rear
    ; length-front     = q .length-front
    ; length-rear      = q .length-rear
    ; length-front≡    = q .length-front≡
    ; length-rear≡     = q .length-rear≡
    ; length-invariant = case ≤→<⊎≡ (q .length-invariant) of λ @0 where
        (inj₁ 1+r≤1+f) → suc≤suc⁻¹ 1+r≤1+f
        (inj₂ r≡1+f)   → ⊥-elim (_↔_.from 1+f≢r (sym r≡1+f))
    }

  rotate : Almost-queue A → Queue A
  rotate q =
    rotate′ q (suc (q .length-front) == q .length-rear) T[==]↔≡

  to-List-rotate′ :
    ∀ b {p} → to-List (rotate′ q b p) ≡ from-Almost-queue q
  to-List-rotate′         false = refl _
  to-List-rotate′ {q = q} true  =
    (q .front ++ reverse (q .rear)) ++ []  ≡⟨ ++-right-identity _ ⟩∎
    q .front ++ reverse (q .rear)          ∎

  to-List-rotate :
    (q : Almost-queue A) → to-List (rotate q) ≡ from-Almost-queue q
  to-List-rotate q =
    to-List-rotate′ (suc (q .length-front) == q .length-rear)

------------------------------------------------------------------------
-- Queue operations

-- Enqueues an element.

enqueue : A → Queue A → Queue A
enqueue x q =
  rotate (record (to-Almost-queue q)
    { rear             = x ∷ q .rear
    ; length-rear      = 1 + q .length-rear
    ; length-rear≡     = cong suc (q .length-rear≡)
    ; length-invariant = suc≤suc (q .length-invariant)
    })

to-List-enqueue : ∀ q → to-List (enqueue x q) ≡ to-List q ++ x ∷ []
to-List-enqueue {x = x} q =
  to-List (enqueue x q)                      ≡⟨ to-List-rotate (record
                                                  { length-invariant = suc≤suc (q .length-invariant)
                                                  }) ⟩
  q .front ++ ⟨ reverse (x ∷ q .rear) ⟩      ≡⟨ ⟨by⟩ (reverse-∷ (q .rear)) ⟩
  q .front ++ (reverse (q .rear) ++ x ∷ [])  ≡⟨ ++-associative (q .front) _ _ ⟩∎
  (q .front ++ reverse (q .rear)) ++ x ∷ []  ∎

-- Dequeues an element, if possible.

dequeue : Queue A → Maybe (A × Queue A)
dequeue (record { front = [] }) = nothing

dequeue q@(record { front        = x ∷ front
                  ; length-front = suc length-front
                  }) =
  just (x , rotate (record (to-Almost-queue q)
    { front            = front
    ; length-front     = length-front
    ; length-invariant = q .length-invariant
    ; length-front≡    = cancel-suc (q .length-front≡)
    }))

dequeue {A = A}
        q@(record { front        = x ∷ front
                  ; length-front = zero
                  }) =                $⟨ [ q .length-front≡ ] ⟩
  Erased (zero ≡ suc (length front))  ↝⟨ Erased.map 0≢+ ⟩
  Erased ⊥                            ↔⟨ Erased-⊥↔⊥ ⟩
  ⊥                                   ↝⟨ ⊥-elim ⟩□
  Maybe (A × Queue A)                 □

to-List-dequeue :
  (q : Queue A) →
  ⊎-map id (Σ-map id to-List) (dequeue q) ≡
  _↔_.to List↔Maybe[×List] (to-List q)
to-List-dequeue (record { front = []; rear = [] }) = refl _

to-List-dequeue q@(record { front = []; rear = _ ∷ _ }) =
                                             $⟨ [ q .length-invariant ] ⟩
  Erased (q .length-rear ≤ q .length-front)  ↝⟨ Erased.map (subst (_ ≤_) (q .length-front≡)) ⟩
  Erased (q .length-rear ≤ 0)                ↝⟨ Erased.map (subst (_≤ _) (q .length-rear≡)) ⟩
  Erased (suc _ ≤ 0)                         ↝⟨ Erased.map (≮0 _) ⟩
  Erased ⊥                                   ↔⟨ Erased-⊥↔⊥ ⟩
  ⊥                                          ↝⟨ ⊥-elim ⟩□
  _                                          □

to-List-dequeue q@(record { front        = x ∷ front
                          ; length-front = suc length-front
                          }) =
  cong (just ∘ (x ,_))
    (to-List-rotate (record { length-invariant = q .length-invariant }))

to-List-dequeue q@(record { front        = x ∷ front
                          ; length-front = zero
                  }) =                $⟨ [ q .length-front≡ ] ⟩
  Erased (zero ≡ suc (length front))  ↝⟨ Erased.map 0≢+ ⟩
  Erased ⊥                            ↔⟨ Erased-⊥↔⊥ ⟩
  ⊥                                   ↝⟨ ⊥-elim ⟩□
  _                                   □

-- The "inverse" of the dequeue operation.

dequeue⁻¹ : Maybe (A × Queue A) → Queue A
dequeue⁻¹ nothing        = from-List []
dequeue⁻¹ (just (x , q)) = record q
  { front            = x ∷ q .front
  ; length-front     = suc (q .length-front)
  ; length-invariant = ≤-step (q .length-invariant)
  ; length-front≡    = cong suc (q .length-front≡)
  }

to-List-dequeue⁻¹ :
  (x : Maybe (A × Queue A)) →
  to-List (dequeue⁻¹ x) ≡
  _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id to-List) x)
to-List-dequeue⁻¹ nothing  = refl _
to-List-dequeue⁻¹ (just _) = refl _

-- A map function.

map : (A → B) → Queue A → Queue B
map f q = record
  { front            = L.map f (q .front)
  ; rear             = L.map f (q .rear)
  ; length-front     = q .length-front
  ; length-rear      = q .length-rear
  ; length-invariant = q .length-invariant
  ; length-front≡    =
      q .length-front              ≡⟨ q .length-front≡ ⟩
      ⟨ length (q .front) ⟩        ≡⟨ ⟨by⟩ (length∘map _ (q .front)) ⟩∎
      length (L.map f (q .front))  ∎
  ; length-rear≡     =
      q .length-rear              ≡⟨ q .length-rear≡ ⟩
      ⟨ length (q .rear) ⟩        ≡⟨ ⟨by⟩ (length∘map _ (q .rear)) ⟩∎
      length (L.map f (q .rear))  ∎
  }

to-List-map : ∀ q → to-List (map f q) ≡ L.map f (to-List q)
to-List-map {f = f} q =
  L.map f (q .front) ++ ⟨ reverse (L.map f (q .rear)) ⟩  ≡⟨ ⟨by⟩ (map-reverse (q .rear)) ⟩
  L.map f (q .front) ++ L.map f (reverse (q .rear))      ≡⟨ sym $ map-++ _ (q .front) _ ⟩∎
  L.map f (q .front ++ reverse (q .rear))                ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Unit

data World : Set where
  ww : World

test : Term → TC ⊤
test hole
  = unify (con (quote ww) []) hole

HVet : Set₁
HVet = {@(tactic test) w : World} → Set

a : {HQ : HVet} → HQ → ⊤
a = _


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

module JamesAll where

import JamesTwoMaps
import JamesFirstComposite
import JamesSecondComposite
import JamesContractibility

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
A : Set
A = ?
B : Set
B = ?


text:
open import Level
open import Ordinals
module BAlgbra {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OrdUtil
import OD
import ODUtil
import ODC

open import Relation.Nullary
open import Relation.Binary
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Core
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )

open inOrdinal O
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

open OD O
open OD.OD
open ODAxiom odAxiom
open HOD

open _∧_
open _∨_
open Bool

--_∩_ : ( A B : HOD  ) → HOD
--A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
--    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }

_∪_ : ( A B : HOD  ) → HOD
A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)

_＼_ : ( A B : HOD  ) → HOD
A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }

∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
    lemma1 {x} lt = lemma3 lt where
        lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) )
        lemma4 {y} z with proj1 z
        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) )
        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) )
        lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
        lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
    lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
        ⟪ case1 refl , d→∋ A A∋x ⟫ )
    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B
        ⟪ case2 refl , d→∋ B B∋x ⟫ )

∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
    lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
    lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫

dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
    lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
    lemma1 {x} lt with proj2 lt
    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫
    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫
    lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫
    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫

dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
    lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
    lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
    lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
    lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
    lemma2 {x} lt with proj1 lt | proj2 lt
    lemma2 {x} lt | case1 cp | _ = case1 cp
    lemma2 {x} lt | _ | case1 cp = case1 cp
    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫

record IsBooleanAlgebra ( L : Set n)
       ( b1 : L )
       ( b0 : L )
       ( -_ : L → L  )
       ( _+_ : L → L → L )
       ( _x_ : L → L → L ) : Set (suc n) where
   field
       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
       x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
       +-sym : {a b : L } → a + b ≡ b + a
       -sym : {a b : L } → a x b  ≡ b x a
       +-aab : {a b : L } → a + ( a x b ) ≡ a
       x-aab : {a b : L } → a x ( a + b ) ≡ a
       +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
       x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
       a+0 : {a : L } → a + b0 ≡ a
       ax1 : {a : L } → a x b1 ≡ a
       a+-a1 : {a : L } → a + ( - a ) ≡ b1
       ax-a0 : {a : L } → a x ( - a ) ≡ b0

record BooleanAlgebra ( L : Set n) : Set (suc n) where
   field
       b1 : L
       b0 : L
       -_ : L → L
       _+_ : L → L → L
       _x_ : L → L → L
       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


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

open import HoTT
open import homotopy.CircleHSpace
open import homotopy.LoopSpaceCircle
import homotopy.Pi2HSusp as Pi2HSusp
open import homotopy.IterSuspensionStable

-- This summerizes all [πₙ Sⁿ]
module homotopy.PinSn where

  πS-SphereS-iso-ℤ : ∀ n → πS n (⊙Sphere (S n)) ≃ᴳ ℤ-group
  πS-SphereS-iso-ℤ 0 =
    πS 0 ⊙S¹
      ≃ᴳ⟨ unTrunc-iso ΩS¹-group-structure ⟩
    Ω^S-group 0 ⊙S¹
      ≃ᴳ⟨ ΩS¹-iso-ℤ ⟩
    ℤ-group
      ≃ᴳ∎
  πS-SphereS-iso-ℤ 1 =
    πS 1 ⊙S²
      ≃ᴳ⟨ Pi2HSusp.π₂-Susp ⊙S¹-hSpace ⟩
    πS 0 ⊙S¹
      ≃ᴳ⟨ πS-SphereS-iso-ℤ O ⟩
    ℤ-group
      ≃ᴳ∎
  πS-SphereS-iso-ℤ (S (S n)) =
    πS (S (S n)) (⊙Sphere (S (S (S n))))
      ≃ᴳ⟨ Susp^StableSucc.stable
           (S n) (S n) (≤-ap-S $ ≤-ap-S $ *2-increasing n)
           (⊙Sphere (S (S n))) {{Sphere-conn (S (S n))}} ⟩
    πS (S n) (⊙Sphere (S (S n)))
      ≃ᴳ⟨ πS-SphereS-iso-ℤ (S n) ⟩
    ℤ-group
      ≃ᴳ∎


text:
-- Minimal implicational modal logic, vector-based de Bruijn approach, initial encoding

module Vi.BoxMp where

open import Lib using (Nat; suc; _+_; Fin; fin; Vec; []; _,_; proj; VMem; mem)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty
  BOX  : Ty       -> Ty

-- Context and truth/validity judgements

Cx : Nat -> Set
Cx n = Vec Ty n

isTrue : forall {tn} -> Ty -> Fin tn -> Cx tn -> Set
isTrue a i tc = VMem a i tc

isValid : forall {vn} -> Ty -> Fin vn -> Cx vn -> Set
isValid a i vc = VMem a i vc

-- Terms

module BoxMp where
  infixl 1 _$_
  infixr 0 lam=>_
  data Tm {vn tn} (vc : Cx vn) (tc : Cx tn) : Ty -> Set where
    var     : forall {a i} -> isTrue a i tc                   -> Tm vc tc a
    lam=>_  : forall {a b} -> Tm vc (tc , a) b                -> Tm vc tc (a => b)
    _$_     : forall {a b} -> Tm vc tc (a => b) -> Tm vc tc a -> Tm vc tc b
    var#    : forall {a i} -> isValid a i vc                  -> Tm vc tc a
    box     : forall {a}   -> Tm vc [] a                      -> Tm vc tc (BOX a)
    unbox'' : forall {a b} -> Tm vc tc (BOX a)  -> Tm (vc , a) tc b -> Tm vc tc b

  syntax unbox'' x' x = unbox x' => x

  v : forall {vn tn} {vc : Cx vn} (k : Nat) {tc : Cx (suc (k + tn))} -> Tm vc tc (proj tc (fin k))
  v i = var (mem i)

  v# : forall {vn tn} (k : Nat) {vc : Cx (suc (k + vn))} {tc : Cx tn} -> Tm vc tc (proj vc (fin k))
  v# i = var# (mem i)

  Thm : Ty -> Set
  Thm a = forall {vn tn} {vc : Cx vn} {tc : Cx tn} -> Tm vc tc a
open BoxMp public

-- Example theorems

rNec : forall {a} -> Thm a -> Thm (BOX a)
rNec x =
  box x

aK : forall {a b} -> Thm (BOX (a => b) => BOX a => BOX b)
aK =
  lam=>
    lam=>
      (unbox v 1 =>
        unbox v 0 =>
          box (v# 1 $ v# 0))

aT : forall {a} -> Thm (BOX a => a)
aT =
  lam=>
    (unbox v 0 => v# 0)

a4 : forall {a} -> Thm (BOX a => BOX (BOX a))
a4 =
  lam=>
    (unbox v 0 => box (box (v# 0)))

t1 : forall {a} -> Thm (a => BOX (a => a))
t1 =
  lam=> box (lam=> (v 0))

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.ReflexiveTransitive module directly
------------------------------------------------------------------------

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

module Data.Star where

open import Relation.Binary.Construct.Closure.ReflexiveTransitive public

{-# WARNING_ON_IMPORT
"Data.Star was deprecated in v0.16.
Use Relation.Binary.Construct.Closure.ReflexiveTransitive instead."
#-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Lex.Core directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Lex.Core where

open import Data.List.Relation.Binary.Lex.Core public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Lex.Core was deprecated in v1.0.
Use Data.List.Relation.Binary.Lex.Core instead."
#-}


text:
module Issue2487-1 where

postulate get-out-of-jail : {A : Set} -> A


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

module overloading.level where

open import sum
open import equality.core
open import overloading.bundle
open import function.isomorphism
open import hott.level.core
open import sets.unit

open Bundle

bundle-structure-iso : ∀ {i j}{Base : Set i}
                       (Struct : Base → Set j)
                     → Σ Base Struct ≅ Bundle Struct
bundle-structure-iso Struct = record
  { to = λ { (X , s) → bundle X s }
  ; from = λ { (bundle X s) → X , s }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl }

bundle-equality-iso : ∀ {i j}{Base : Set i}
                      (Struct : Base → Set j)
                    → ((B : Base) → h 1 (Struct B))
                    → {X Y : Bundle Struct}
                    → (parent X ≡ parent Y)
                    ≅ (X ≡ Y)
bundle-equality-iso Struct hS {X}{Y} = begin
    parent X ≡ parent Y
  ≅⟨ sym≅ ×-right-unit ⟩
    ((parent X ≡ parent Y) × ⊤)
  ≅⟨ Σ-ap-iso refl≅ (λ p → sym≅ (contr-⊤-iso (hS _ _ _))) ⟩
    ( Σ (parent X ≡ parent Y) λ p
    → (subst Struct p (struct X) ≡ struct Y) )
  ≅⟨ Σ-split-iso ⟩
    (parent X , struct X) ≡ (parent Y , struct Y)
  ≅⟨ iso≡ (bundle-structure-iso Struct) ⟩
    X ≡ Y
  ∎
  where open ≅-Reasoning

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types