Frex.Free

Definitions and constructions involving free models

Reexports

import public Frex.Free.Definition
import public Frex.Free.Construction
import public Data.Fun.Nary

Definitions

extensionLemma : (h : mod1 ~> mod2) -> (s ~~> mod2 .Model) .rel ((h .H) .H . mod1 .Env) (mod2 .Env): Visibility: public export
freeSolve : mod1 ~> mod2 -> (eq : (Term (pres .signature) (U s), Term (pres .signature) (U s))) -> (mod1 .Model) .rel ((mod1 .Model) .Sem (fst eq) ((mod1 .Env) .H)) ((mod1 .Model) .Sem (snd eq) ((mod1 .Env) .H)) -> (mod2 .Model) .rel ((mod2 .Model) .Sem (fst eq) ((mod2 .Env) .H)) ((mod2 .Model) .Sem (snd eq) ((mod2 .Env) .H)): Visibility: public export
solveVect : (free : Free pres (irrelevantCast (Fin n))) -> (env : Vect n (U a)) -> (eq : (Term (pres .signature) (Fin n), Term (pres .signature) (Fin n))) -> ((free .Data) .Model) .rel (free .Sem (fst eq) (((free .Data) .Env) .H)) (free .Sem (snd eq) (((free .Data) .Env) .H)) => a .rel (a .Sem (fst eq) (flip index env)) (a .Sem (snd eq) (flip index env)): Visibility: public export
solve : (n : Nat) -> (free : Free pres (cast (Fin n))) -> PI n Hidden (U a) (\env => (eq : (Term (pres .signature) (Fin n), Term (pres .signature) (Fin n))) -> ((free .Data) .Model) .rel (free .Sem (fst eq) (((free .Data) .Env) .H)) (free .Sem (snd eq) (((free .Data) .Env) .H)) => a .rel (a .Sem (fst eq) (flip index env)) (a .Sem (snd eq) (flip index env))): Visibility: public export
prove : (free : Free pres (cast (Fin n))) -> (eq : (Term (pres .signature) (Fin n), Term (pres .signature) (Fin n))) -> {auto prf : ((free .Data) .Model) .rel (free .Sem (fst eq) (((free .Data) .Env) .H)) (free .Sem (snd eq) (((free .Data) .Env) .H))} -> ((free' .Data) .Model) .rel (((free' .Data) .Model) .Sem (fst eq) (((free' .Data) .Env) .H)) (((free' .Data) .Model) .Sem (snd eq) (((free' .Data) .Env) .H)): Visibility: public export
.simplify : (freea : (free : Free pres x ** Model pres)) -> Term (pres .signature) (U x) -> x ~> cast (snd freea) -> U (snd freea): Visibility: public export
simplifyGeneral : (free : Free pres x) -> (env : x ~> cast a) -> (t : Term (pres .signature) (U x)) -> a .rel (a .Sem t (env .H)) ((free ** a) .simplify t env): Visibility: public export
simplifyVect : (free : Free pres (irrelevantCast (Fin n))) -> (env : Vect n (U a)) -> (t : Term (pres .signature) (Fin n)) -> a .rel (a .Sem t (flip index env)) ((free ** a) .simplify t (mate (flip index env))): Visibility: public export
simplify : (n : Nat) -> (free : Free pres (cast (Fin n))) -> PI n Hidden (U a) (\env => (t : Term (pres .signature) (Fin n)) -> a .rel (a .Sem t (flip index env)) ((free ** a) .simplify t (mate (flip index env)))): Visibility: public export